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