Certificate for #1949 ⟨a, b, c | abc=ab, ccb=1⟩

Completion settings:

[1] abc=ab

Axiom: abc=ab.

Defines rule #2.

Referenced by [3].

[2] ccb=1

Axiom: ccb=1.

Defines rule #3.

Referenced by [3].

[3] abb=ab

Overlap of [1] abc=ab with [2] ccb=1:

ab c ccb

Critical pair: ab=abcb.

Reduce RHS:

[1](abc)b
⇒ abb

Flip LHS and RHS.

Defines rule #1.