PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
2
1
2
2
1
2
1
1
1
1
1
1
2
1
1
2
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.
a1,a2:(
n
(n
m-1)). f1(a1) = f1(a2)
(n
(n
m-1))
a1 = a2
8.
a1:
m
n
9.
a2:
m
n
10.
f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > )
11.
a1(m-1) = a2(m-1)
12.
f(a1) = f(a2)
13.
x:
m
14.
x = m-1
m
15.
a1 = a2
(m-1)
n
a1(x) = a2(x)
By:
Assert (x
(m-1))
Generated subgoals:
1
x
(m-1)
2
16.
x
(m-1)
a1(x) = a2(x)
About:
x 
(m-1) (m-1) a1(x) = a2(x)
(m-1)
n)(n
m-1)
n = 0n
(nm-1)(nm)
a1,a2:(n(nm-1)). f1(a1) = f1(a2) (n
(nm-1)) 
a1 = a2mnmnmx = m-1 m (m-1)n a1(x) = a2(x) (m-1)) x (m-1) (m-1) a1(x) = a2(x)
