PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
2
1
2
2
1
2
1
1
2
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.
b:
(n
m)
b
(n
(n
m-1))
By:
Inst
Thm*
n,k:
. 0 < k
(n
k) = n
(n
k-1) [n;m]
Generated subgoal:
1
9.
(n
m) = n
(n
m-1)
b
(n
(n
m-1))
About:
m) = n
(nm-1)
b 
(n(nm-1))
(m-1)
n)(nm-1)(m-1)n; (nm-1); f)
n = 0n
(nm-1)(nm)(nm) b (n(nm-1))
n,k:. 0 < k 
(nk) = n(nk-1)
[n;m]m) = n(nm-1) b (n(nm-1))
