Certificate for #2710 ⟨a, b | abbab=ababa⟩

Back:⟨a, b | abbab=ababa⟩

Completion settings:

[1] abbab=ababa

Axiom: abbab=ababa.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

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

[3] abbab=cca

Simplify [1] abbab=ababa.

Reduce RHS:

[2](ab)aba
[2]⇒ c(ab)a
⇒ cca

Referenced by [4].

[4] cca=cbc

Overlap of [3] abbab=cca with [2] ab=c:

abbab ab

Critical pair: cbab=cca.

Reduce LHS:

[2]cb(ab)
⇒ cbc

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] cbcb=ccc

Overlap of [4] cca=cbc with [2] ab=c:

cc a ab

Critical pair: ccc=cbcb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] ccccb=cbccc

Overlap of [5] cbcb=ccc with [5] cbcb=ccc:

cb cb cbcb

Critical pair: cbccc=ccccb.

Flip LHS and RHS.

Defines rule #4.