PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
2
1
2
2
1
2
1
1
1
1
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.
f1:
n
(n
m-1)
(n
m)
8.
a1,a2:(
n
(n
m-1)). f1(a1) = f1(a2)
(n
(n
m-1))
a1 = a2
9.
a1:
m
n
10.
a2:
m
n
11.
f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > )
f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > )
(n
(n
m-1))
By:
RWH (LemmaC
Thm*
n,k:
. 0 < k
(n
k) = n
(n
k-1)) 11
Generated subgoals:
None
About:
(m-1)
n)(n
m-1)(m-1)n; (nm-1); f)
n = 0n
(nm-1)(nm)
a1,a2:(n(nm-1)). f1(a1) = f1(a2) 
(n
(nm-1)) 
a1 = a2mnmn
f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > ) (n(nm-1))n,k:. 0 < k (nk) = n(nk-1))
11
