Thm* e:
, L,M:
*. ||e:L @ M|| = ||e:L||+||e:M||
counter_append
Thm* S:ActionSet(T), s:S.car, tl1,tl2:T*. (S:tl1 @ tl2
s) = (S:tl1
(S:tl2
s))
action_append
Thm* 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 @ (b
k)) @ c
s) = (S:A
s))))
pump_theorem
Thm* L:Alph*, n:
. (L
n) = if n=
0
nil else L @ (L
n-1) fi lpower_alt
Thm* S:ActionSet(Alph), s:S.car, L1,L2,L:Alph*.
(S:L1
s) = (S:L2
s)
(S:L @ L1
s) = (S:L @ L2
s)
maction_lemma
In prior sections: list 1 list 3 autom