PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
1
2
1
1
1
2
1
2
1
1
1
1.
n:
2.
f:
n
n
3.
a1:
n
4.
a2:
n
5.
f(a1) = f(a2)
6.
a1 = a2
7.
b:
(n+1)
8.
b = n
(n+1)
9.
a:
n
10.
f(a) = b
n
11.
a = a2
if a2=
a1
n else f(a1) fi = b
(n+1)
By:
SplitOnConclITE
Generated subgoals:
1
12.
a2 = a1
n = b
(n+1)
2
12.
a2 = a1
f(a1) = b
(n+1)
About:
n = b 
(n+1)
a2 = a1 f(a1) = b (n+1)n
nnna1 = a2(n+1)b = n (n+1)n n if a2=
a1
n else f(a1) fi = b (n+1) n = b (n+1)a2 = a1 f(a1) = b (n+1)
