Selected Objects

def	action_set	ActionSet(T) == car:TypeTcarcar
def	aset_car	a.car == 1of(a)
def	aset_act	a.act == 2of(a)
def	factorial	(rec) (n)! == if n=0 1 else n(n-1)! fi
THM	ex1_of_factorial	(0)! = 1
def	multi_action	(rec) multi_action(l; s; ASet) == if null(l) s else ASet.act(hd(rev(l)),multi_action(ASet.act; rev(tl(rev(l))); s)) fi
def	maction	(rec) (S:Ls) == if null(L) s else S.act(hd(L),(S:tl(L)s)) fi
THM	maction_lemma	S:ActionSet(Alph), s:S.car, L1,L2,L:Alph*. (S:L1s) = (S:L2s) (S:L @ L1s) = (S:L @ L2s)
def	lpower	(rec) (Ln) == if n=0 nil else (Ln-1) @ L fi
THM	lpower_alt	L:Alph*, n:. (Ln) = if n=0 nil else L @ (Ln-1) fi
THM	pump_theorem	S:ActionSet(Alph), N:, s:S.car. #(S.car)=N (A:Alph*. N < ||A|| (a,b,c:Alph*. 0 < ||b|| & A = ((a @ b) @ c) & (k:. (S:(a @ (bk)) @ cs) = (S:As))))
THM	pump_thm_cor	n:, Alph:Type, S:ActionSet(Alph), s,f:S.car. #(S.car)=n (l:Alph*. (S:ls) = f) (l:Alph*. ||l||n & (S:ls) = f)
THM	action_append	S:ActionSet(T), s:S.car, tl1,tl2:T*. (S:tl1 @ tl2s) = (S:tl1(S:tl2s))
def	n0n1	n0n1(n) == ([0]n) @ ([1]n)
def	el_counter	(rec) ||e:L|| == if null(L)0 ;e=hd(L)1+||e:tl(L)|| else ||e:tl(L)|| fi
THM	counter_of_nil	e:. ||e:nil|| = 0
THM	counter_append	e:, L,M:*. ||e:L @ M|| = ||e:L||+||e:M||
THM	counter_lpower	e:, L:*, n:. ||e:(Ln)|| = n||e:L||
THM	n0n1_irregular	S:ActionSet(), s,q:S.car. (n:. #(S.car)=n ) & (k:. (S:n0n1(k)s) = q) (L:*. (S:Ls) = q & (k:. L = n0n1(k)))