Certificate for #1922 ⟨a, b, c | abc=aa, cab=1⟩

Back:⟨a, b, c | abc=aa, cab=1⟩

Completion settings:

[1] aa=abc

Axiom: abc=aa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[2] cab=1

Axiom: cab=1.

Referenced by [4], [5].

[3] abca=abcbc

Overlap of [1] aa=abc with [1] aa=abc:

a a aa

Critical pair: aabc=abca.

Reduce LHS:

[1](aa)bc
⇒ abcbc

Flip LHS and RHS.

Referenced by [4].

[4] ca=cbc

Overlap of [2] cab=1 with [3] abca=abcbc:

c ab abca

Critical pair: cabcbc=ca.

Reduce LHS:

[2](cab)cbc
⇒ cbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] cbcb=1

Overlap of [2] cab=1 with [4] ca=cbc:

cab ca

Critical pair: cbcb=1.

Defines rule #1.