import string
import random

test_cases = 100

juan = []
chars=string.ascii_uppercase
for _ in range(test_cases):
	rand = ''.join(random.choice(chars) for _ in range(5))
	juan.append(rand)
	print("let j = D.insert \"" + rand + "\" S.empty j;; ")

for i in range(test_cases):
	print("D.rep_ok (D.remove \"" + juan[i] + "\" j);; ")