Certificate for #22290 ⟨a, b | aaa=1, abbbbb=ba⟩

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

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #3.

Referenced by [3].

[2] ba=abbbbb

Axiom: abbbbb=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb=b

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

b a aaa

Critical pair: b=abbbbbaa.

Reduce RHS:

[2]abbbb(ba)a
[2]⇒ abbb(ba)bbbbba
[2]⇒ abb(ba)bbbbbbbbbba
[2]⇒ ab(ba)bbbbbbbbbbbbbbba
[2]⇒ a(ba)bbbbbbbbbbbbbbbbbbbba
[2]⇒ aabbbbbbbbbbbbbbbbbbbbbbbb(ba)
[2]⇒ aabbbbbbbbbbbbbbbbbbbbbbb(ba)bbbbb
[2]⇒ aabbbbbbbbbbbbbbbbbbbbbb(ba)bbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabbb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aabb(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aab(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[2]⇒ aa(ba)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
[1]⇒ (aaa)bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb
⇒ bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb

Flip LHS and RHS.

Defines rule #1.