Certificate for #2326 ⟨a, b | ababaab=bab⟩

Back:⟨a, b | ababaab=bab⟩

Completion settings:

[1] ababaab=bab

Axiom: ababaab=bab.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #3.

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

[3] ababaab=bc

Simplify [1] ababaab=bab.

Reduce RHS:

[2]b(ab)
⇒ bc

Referenced by [4].

[4] bc=ccac

Overlap of [3] ababaab=bc with [2] ab=c:

ababaab ab

Critical pair: cabaab=bc.

Reduce LHS:

[2]c(ab)aab
[2]⇒ cca(ab)
⇒ ccac

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] accac=cc

Overlap of [2] ab=c with [4] bc=ccac:

a b bc

Critical pair: accac=cc.

Defines rule #1.

Referenced by [6].

[6] acccc=cccac

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

acc ac accac

Critical pair: acccc=cccac.

Defines rule #2.