Certificate for #7802 ⟨a, b | aaa=1, abbbb=ba⟩

Back:⟨a, b | aaa=1, abbbb=ba⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #3.

Referenced by [3].

[2] ba=abbbb

Axiom: abbbb=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=b

Overlap of [2] ba=abbbb with [1] aaa=1:

b a aaa

Critical pair: b=abbbbaa.

Reduce RHS:

[2]abbb(ba)a
[2]⇒ abb(ba)bbbba
[2]⇒ ab(ba)bbbbbbbba
[2]⇒ a(ba)bbbbbbbbbbbba
[2]⇒ aabbbbbbbbbbbbbbb(ba)
[2]⇒ aabbbbbbbbbbbbbb(ba)bbbb
[2]⇒ aabbbbbbbbbbbbb(ba)bbbbbbbb
[2]⇒ aabbbbbbbbbbbb(ba)bbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbb(ba)bbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aab(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aa(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[1]⇒ (aaa)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
⇒ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Flip LHS and RHS.

Defines rule #1.