PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
surj
is
inj
gen
1
1
1
1
2
1
1
1
1
1
1
1
1
1
1
1
1.
A:
Type
2.
B:
Type
3.
f:
A
B
4.
f1:
A
B
5.
g:
B
A
6.
g o f1 = Id
7.
f1 o g = Id
8.
n:
9.
f2:
n
B
10.
g1:
B
n
11.
g1 o f2 = Id
12.
f2 o g1 = Id
13.
Surj(A; B; f)
14.
a1:
A
15.
a2:
A
16.
f(a1) = f(a2)
g1(f(g(f1(a1)))) = g1(f(g(f1(a2))))
By:
RW (LowerC add_composeC) 0
Generated subgoal:
1
g1(f((g o f1)(a1))) = g1(f((g o f1)(a2)))
About:
g1(f((g o f1)(a1))) = g1(f((g o f1)(a2)))
B
