PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
lpower
alt
1
2
2
1
2
2
1.
Alph:
Type
2.
L:
Alph*
3.
n:
4.
0 < n
5.
(L
n-1) = if n-1=
0
nil else L @ (L
n-1-1) fi
6.
n = 0
7.
n-1 = 0
8.
(L
n-1) = (L @ (L
n-1-1))
(L
n) = (L @ (L
n-1-1) @ L)
By:
RWH (RevLemmaC
Thm*
as,bs,cs:T*. ((as @ bs) @ cs) = (as @ (bs @ cs))) 0
Generated subgoal:
1
(L
n) = ((L @ (L
n-1-1)) @ L)
About:
(L
n) = ((L @ (Ln-1-1)) @ L)
n-1) = if n-1=
0
nil else L @ (Ln-1-1) fi
n = 0n-1 = 0n-1) = (L @ (Ln-1-1)) (Ln) = (L @ (Ln-1-1) @ L)
as,bs,cs:T*. ((as @ bs) @ cs) = (as @ (bs @ cs)))
0 (Ln) = ((L @ (Ln-1-1)) @ L)
