PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
2
1
2
2
1
1
1.
n:
2.
m:
3.
0 < m
4.
f:
(
(m-1)
n)
(n
m-1)
5.
Bij(
(m-1)
n;
(n
m-1); f)
6.
n = 0
7.
f1:
n
(n
m-1)
(n
(n
m-1))
8.
Bij(
n
(n
m-1);
(n
(n
m-1)); f1)
n
(n
m-1) = (n
m)
By:
RW (AddrC [3] (RecUnfoldTopC `exp`)) 0
Generated subgoal:
1
n
(n
m-1) = if m=
0
1 else n
(n
m-1) fi
About:
n
(n
m-1) = if m=
0
1 else n(nm-1) fi
(m-1)
n)(nm-1)(m-1)n; (nm-1); f)
n = 0n
(nm-1)(n(nm-1))n(nm-1); (n(nm-1)); f1) n(nm-1) = (nm) n(nm-1) = if m=0 1 else n(nm-1) fi
