Certificate for #5209 ⟨a, b | aabbaab=aaba⟩

Back:⟨a, b | aabbaab=aaba⟩

Completion settings:

[1] aabbaab=aaba

Axiom: aabbaab=aaba.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Defines rule #4.

Referenced by [3], [4], [5].

[3] aabbaab=ca

Simplify [1] aabbaab=aaba.

Reduce RHS:

[2](aab)a
⇒ ca

Referenced by [4].

[4] ca=cbc

Overlap of [3] aabbaab=ca with [2] aab=c:

aabbaab aab

Critical pair: cbaab=ca.

Reduce LHS:

[2]cb(aab)
⇒ cbc

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] cbcbcb=cc

Overlap of [4] ca=cbc with [2] aab=c:

c a aab

Critical pair: cc=cbcab.

Reduce RHS:

[4]cb(ca)b
⇒ cbcbcb

Flip LHS and RHS.

Defines rule #2.

Referenced by [6].

[6] cccb=cbcc

Overlap of [5] cbcbcb=cc with [5] cbcbcb=cc:

cb cbcb cbcbcb

Critical pair: cbcc=cccb.

Flip LHS and RHS.

Defines rule #1.