PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
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
a1,a2:(
m
n). (
z.z(0))(a1) = (
z.z(0))(a2)
(n
m)
a1 = a2
By:
Reduce 0
Generated subgoal:
1
a1,a2:(
m
n). a1(0) = a2(0)
(n
m)
a1 = a2
About:
a1,a2:(
m
n). a1(0) = a2(0) 
(n
m) 
a1 = a2
(m-1)n)(nm-1)(m-1)n; (nm-1); f) a1,a2:(mn). (
z.z(0))(a1) = (z.z(0))(a2) (nm) a1 = a2 a1,a2:(mn). a1(0) = a2(0) (nm) a1 = a2
