On the Combination of Congruence Closure and Completion - Artificial Intelligence and Symbolic Computation - page 109

V1 V2 V1 V2

f E g f R g

c1 c2 c1 c2

c1 > c2

V1 V1

S i S

i

R R

V2 V3 V2 V3

f f

V2 V2

c2 c2

R R

g R h g R h

V1 V3 V1 V3

c1 c3

c3 c1

c2 > c3

f f

V1 V1

c1 c1

R R

g R h g R h

V2 V3 V2 V3

c2 c3

c3 c2

c1 > c3

Fig. 1. Orient , SR , RRout and RRin graph transformation rules