Certificate for #2083 ⟨a, b | abbabbba=ba⟩

Back:⟨a, b | abbabbba=ba⟩

Completion settings:

[1] abbabbba=ba

Axiom: abbabbba=ba.

Referenced by [3].

[2] abbabbb=c

Axiom: abbabbb=c.

Referenced by [3], [4].

[3] ba=ca

Overlap of [1] abbabbba=ba with [2] abbabbb=c:

abbabbba abbabbb

Critical pair: ca=ba.

Flip LHS and RHS.

Defines rule #1.

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

[4] abcabbb=c

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

ab babbb ba

Critical pair: abcabbb=c.

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

[5] bc=cc

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

b a abcabbb

Critical pair: bc=cabcabbb.

Reduce RHS:

[4]c(abcabbb)
⇒ cc

Defines rule #2.

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

[6] accaccca=ca

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

abcabb b ba

Critical pair: abcabbca=ca.

Reduce LHS:

[5]a(bc)abbca
[5]⇒ accab(bc)a
[5]⇒ acca(bc)ca
⇒ accaccca

Defines rule #4.

[7] accacccc=cc

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

abcabb b bc

Critical pair: abcabbcc=cc.

Reduce LHS:

[5]a(bc)abbcc
[5]⇒ accab(bc)c
[5]⇒ acca(bc)cc
⇒ accacccc

Defines rule #5.

[8] accabbb=c

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

a bcabbb bc

Critical pair: accabbb=c.

Defines rule #3.