PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
2
1
2
2
1
2
1
1
2
1
1
1
1
2
1
1
1
1
1
1
1.
n:
2.
m:
3.
0 < m
4.
f:
(
(m-1)
n)
(n
m-1)
5.
n = 0
6.
f1:
n
(n
m-1)
(n
m)
7.
b:
(n
m)
8.
a:
n
(n
m-1)
9.
f1(a) = b
(n
(n
m-1))
10.
a@0:
(m-1)
n
11.
f(a@0) = 2of(a)
(
z.if z=
m-1
1of(a) else a@0(z) fi)
m
n
By:
Analyze
Generated subgoal:
1
12.
z:
m
if z=
m-1
1of(a) else a@0(z) fi
n
About:
m
if z=
m-1
1of(a) else a@0(z) fi 
n
(m-1)
n)(n
m-1)
n = 0n
(nm-1)(nm)(nm)n(nm-1) (n
(nm-1))(m-1)n (
z.if z=m-1 1of(a) else a@0(z) fi) mnm if z=m-1 1of(a) else a@0(z) fi n
