PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
wf
n:
, l:
n*. en(l)
By:
UnivCD
THEN
ListInd 2
THEN
RecUnfold `en` 0
THEN
Reduce 0
Generated subgoals:
1
1.
n:
2.
l:
n*
0
2
1.
n:
2.
l:
n*
3.
u:
n
4.
v:
n*
5.
en(v)
u+en(v)
n
About:
n*
0 
n*nn* u+en(v)
n 
n:, l:n*. en(l) n* 0 n*nn* u+en(v)n 
