At:
graph-isomorphic transitivity111
1.
G: Graph
2.
H: Graph
3.
K: Graph
4.
v1: Vertices(G)Vertices(H)
5.
e1: Edges(G)Edges(H)
6.
Bij(Vertices(G); Vertices(H); v1)
7.
Bij(Edges(G); Edges(H); e1)
8.
(v1,v1) o Incidence(G) = Incidence(H) o e1
9.
vmap: Vertices(H)Vertices(K)
10.
emap: Edges(H)Edges(K)
11.
Bij(Vertices(H); Vertices(K); vmap)
12.
Bij(Edges(H); Edges(K); emap)
13.
(vmap,vmap) o Incidence(H) = Incidence(K) o emap
(vmap o v1,vmap o v1) o Incidence(G) = Incidence(K) o emap o e1
By:
RWO
Thm*f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD
0
THEN
RevHypSubst -1 0
THEN
RWO "comp2_comp_assoc < " 0
THEN
RevHypSubst -6 0
THEN
RWO
Thm*h:(A'A1A2), g1:(A1B), g2:(A2C), f1:(BB'), f2:(CC'). (f1,f2) o (g1,g2) o h = (f1 o g1,f2 o g2) o h
0
Generated subgoals:
Vertices(H)
(vmap o v1,vmap o v1) o Incidence(G) = Incidence(K) o emap o e1
f:(A
A
A2), g1:(A1