PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
1
2
2
1
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
a1 = a2
By:
FwdThru
Thm*
Q:(A
B
Prop). (
x:A.
y:B. Q(x,y))
(
f:(A
B).
x:A. Q(x,f(x))) [9]
Generated subgoal:
1
10.
f:(
(n+1)
n).
b:
(n+1). h(f(b)) = b
a1 = a2
About:
f:(
(n+1)
n). 
b:(n+1). h(f(b)) = b
a1 = a2nnn; n; f)nn
a1 = a2n(n+1)b:(n+1). a:n. h(a) = b a1 = a2Q:(ABProp). (x:A. y:B. Q(x,y)) 
(f:(AB). x:A. Q(x,f(x)))
[9]f:((n+1)n). b:(n+1). h(f(b)) = b a1 = a2
