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