Certificate for #1810 ⟨a, b | abbababba=b⟩

Back:⟨a, b | abbababba=b⟩

Completion settings:

[1] abbababba=b

Axiom: abbababba=b.

Referenced by [3].

[2] abba=c

Axiom: abba=c.

Defines rule #2.

Referenced by [3], [5].

[3] cbc=b

Overlap of [1] abbababba=b with [2] abba=c:

abbababba abba

Critical pair: cbabba=b.

Reduce LHS:

[2]cb(abba)
⇒ cbc

Defines rule #1.

Referenced by [4], [6].

[4] cbb=bbc

Overlap of [3] cbc=b with [3] cbc=b:

cb c cbc

Critical pair: cbb=bbc.

Defines rule #4.

Referenced by [5].

[5] abbc=bbca

Overlap of [2] abba=c with [2] abba=c:

abb a abba

Critical pair: abbc=cbba.

Reduce RHS:

[4](cbb)a
⇒ bbca

Defines rule #3.

Referenced by [6].

[6] abbb=bbcabc

Overlap of [5] abbc=bbca with [3] cbc=b:

abb c cbc

Critical pair: abbb=bbcabc.

Defines rule #5.