PrintForm
Definitions
action
sets
Sections
AutomataTheory
Doc
At:
lpower
alt
1
2
2
1
1
1
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.
n = 0
((L
n-1) @ L) = L
By:
RecCaseSplit `lpower`
Generated subgoals:
1
9.
n-1 = 0
L = L
2
9.
n-1 = 0
(((L
n-1-1) @ L) @ L) = L
About:
L = L
n-1 = 0 (((L
n-1-1) @ L) @ L) = L
n-1) = if n-1=
0
nil else L @ (Ln-1-1) fin = 0n = 0 ((Ln-1) @ L) = L L = Ln-1 = 0 (((Ln-1-1) @ L) @ L) = L
