PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
2
1
1
1
2
1
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.
b:
8.
0
b < (n
m)
a:(
m
n). (
z.z(0))(a) = b
(n
m)
By:
Assert ((n
m) = 0)
Generated subgoals:
1
(n
m) = 0
2
9.
(n
m) = 0
a:(
m
n). (
z.z(0))(a) = b
(n
m)
About:
(n
m) = 0m) = 0 
a:(
m
n). (
z.z(0))(a) = b 
(nm)
(m-1)n)(nm-1)(m-1)n; (nm-1); f)
b < (nm) a:(mn). (z.z(0))(a) = b (nm)m) = 0) (nm) = 0m) = 0 a:(mn). (z.z(0))(a) = b (nm)
