Certificate for #2047 ⟨a, b | abaabbba=ba⟩

Back:⟨a, b | abaabbba=ba⟩

Completion settings:

[1] abaabbba=ba

Axiom: abaabbba=ba.

Referenced by [3].

[2] abaabbb=c

Axiom: abaabbb=c.

Referenced by [3], [4].

[3] ba=ca

Overlap of [1] abaabbba=ba with [2] abaabbb=c:

abaabbba abaabbb

Critical pair: ca=ba.

Flip LHS and RHS.

Defines rule #1.

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

[4] acaabbb=c

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

a baabbb ba

Critical pair: acaabbb=c.

Defines rule #3.

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

[5] bc=cc

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

b a acaabbb

Critical pair: bc=cacaabbb.

Reduce RHS:

[4]c(acaabbb)
⇒ cc

Defines rule #2.

Referenced by [6], [7].

[6] acaaccca=ca

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

acaabb b ba

Critical pair: acaabbca=ca.

Reduce LHS:

[5]acaab(bc)a
[5]⇒ acaa(bc)ca
⇒ acaaccca

Defines rule #4.

[7] acaacccc=cc

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

acaabb b bc

Critical pair: acaabbcc=cc.

Reduce LHS:

[5]acaab(bc)c
[5]⇒ acaa(bc)cc
⇒ acaacccc

Defines rule #5.