PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
one
one
corr
tran
1
1
1
2
1
1
1.
A:
Type
2.
B:
Type
3.
C:
Type
4.
f1:
A
B
5.
g1:
B
A
6.
g1 o f1 = Id
7.
f1 o g1 = Id
8.
f:
B
C
9.
g:
C
B
10.
g o f = Id
11.
f o g = Id
12.
x:
C
f(g(x)) = x
By:
RWH add_composeC 0
Generated subgoal:
1
(f o g)(x) = x
About:
(f o g)(x) = x
B
