PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
1
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
Surj(
n;
(n+1);
x.if a2=
x
n else f(x) fi)
By:
Unfold `surject` 0
THEN
UnivCD
Generated subgoal:
1
8.
b:
(n+1)
a:
n. (
x.if a2=
x
n else f(x) fi)(a) = b
About:
(n+1)
a:n. (
x.if a2=
x
n else f(x) fi)(a) = bn
nn; n; f)nn
a1 = a2 Surj(n; (n+1); x.if a2=x n else f(x) fi)(n+1) a:n. (x.if a2=x n else f(x) fi)(a) = b
