PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
1
2
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
a1 = a2
By:
Assert (
h:(
n
(n+1)). Surj(
n;
(n+1); h))
Generated subgoals:
1
h:(
n
(n+1)). Surj(
n;
(n+1); h)
2
8.
h:(
n
(n+1)). Surj(
n;
(n+1); h)
a1 = a2
About:
h:(
n
(n+1)). Surj(n; (n+1); h)h:(n(n+1)). Surj(n; (n+1); h) a1 = a2nnn; n; f)nn
a1 = a2 a1 = a2h:(n(n+1)). Surj(n; (n+1); h)) h:(n(n+1)). Surj(n; (n+1); h)h:(n(n+1)). Surj(n; (n+1); h) a1 = a2
