Certificate for #2069 ⟨a, b | ababbbba=ba⟩

Back:⟨a, b | ababbbba=ba⟩

Completion settings:

[1] ababbbba=ba

Axiom: ababbbba=ba.

Referenced by [3].

[2] ababbbb=c

Axiom: ababbbb=c.

Referenced by [3], [4].

[3] ba=ca

Overlap of [1] ababbbba=ba with [2] ababbbb=c:

ababbbba ababbbb

Critical pair: ca=ba.

Flip LHS and RHS.

Defines rule #1.

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

[4] acabbbb=c

Overlap of [2] ababbbb=c with [3] ba=ca:

a babbbb ba

Critical pair: acabbbb=c.

Defines rule #3.

Referenced by [5], [6], [7].

[5] bc=cc

Overlap of [3] ba=ca with [4] acabbbb=c:

b a acabbbb

Critical pair: bc=cacabbbb.

Reduce RHS:

[4]c(acabbbb)
⇒ cc

Defines rule #2.

Referenced by [6], [7].

[6] acacccca=ca

Overlap of [4] acabbbb=c with [3] ba=ca:

acabbb b ba

Critical pair: acabbbca=ca.

Reduce LHS:

[5]acabb(bc)a
[5]⇒ acab(bc)ca
[5]⇒ aca(bc)cca
⇒ acacccca

Defines rule #4.

[7] acaccccc=cc

Overlap of [4] acabbbb=c with [5] bc=cc:

acabbb b bc

Critical pair: acabbbcc=cc.

Reduce LHS:

[5]acabb(bc)c
[5]⇒ acab(bc)cc
[5]⇒ aca(bc)ccc
⇒ acaccccc

Defines rule #5.