PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
1
2
2
1
1
1
1
2
1
1.
n:
2.
f:
n
n
3.
Surj(
n;
n; f)
4.
a1:
n
5.
a2:
n
6.
f(a1) = f(a2)
7.
a1 = a2
8.
h:
n
(n+1)
9.
b:
(n+1).
a:
n. h(a) = b
10.
f1:
(n+1)
n
11.
b:
(n+1). h(f1(b)) = b
12.
n = 0
13.
i:
(n+1), j:
i. f1(i) = f1(j)
a1 = a2
By:
Analyze 13
THEN
Analyze 14
Generated subgoal:
1
13.
i:
(n+1)
14.
j:
i
15.
f1(i) = f1(j)
a1 = a2
About:
(n+1)i
a1 = a2n
nn; n; f)nn
a1 = a2n(n+1)
b:(n+1). 
a:n. h(a) = b(n+1)nb:(n+1). h(f1(b)) = bn = 0i:(n+1), j:i. f1(i) = f1(j) a1 = a2(n+1)i a1 = a2
