action
sets
Sections
AutomataTheory
Doc
Def
i=
j == if i=j
true
; false
fi
Thm*
L:Alph*, n:
. (L
n) = if n=
0
nil else L @ (L
n-1) fi lpower_alt
In prior sections:
bool
1
L:Alph*, n:
. (L
n) = if n=
0
nil else L @ (Ln-1) fi lpower_alt
j == if i=j true ; false fi
L:Alph*, n:. (Ln) = if n=0 nil else L @ (Ln-1) fi lpower_alt