PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
1
2
1
2
1
1
1
1
1
1.
n:
2.
b:
3.
0
b < (n
0)
0 = b
(n
0)
By:
RWH (RecUnfoldC `exp`) 3
Generated subgoal:
1
3.
0
b < if 0=
0
1 else n
(n
0-1) fi
0 = b
(n
0)
About:
b < if 0=
0
1 else n
(n
0-1) fi
0 = b 
(n0)
b < (n0) 0 = b (n0) b < if 0=0 1 else n(n0-1) fi 0 = b (n0)
