PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
counter
lpower
1
2
1.
e:
2.
L:
*
3.
n:
4.
0 < n
5.
||e:(L
n-1)|| = (n-1)
||e:L||
||e:(L
n)|| = n
||e:L||
By:
RW (RecUnfoldC `lpower`) 0
Generated subgoal:
1
||e:if n=
0
nil else (L
n-1) @ L fi|| = n
||e:L||
About:
||e:if n=
0
nil else (L
n-1) @ L fi|| = n
||e:L|| 
*n-1)|| = (n-1)||e:L|| ||e:(Ln)|| = n||e:L|| ||e:if n=0 nil else (Ln-1) @ L fi|| = n||e:L|| 
