Certificate for #4917 ⟨a, b | aab=ba, bbbbb=1⟩

Back:⟨a, b | aab=ba, bbbbb=1⟩

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] bbbbb=1

Axiom: bbbbb=1.

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=a

Overlap of [2] bbbbb=1 with [1] ba=aab:

bbbb b ba

Critical pair: bbbbaab=a.

Reduce LHS:

[1]bbb(ba)ab
[1]⇒ bb(ba)abab
[1]⇒ b(ba)ababab
[1]⇒ (ba)abababab
[1]⇒ aa(ba)bababab
[1]⇒ aaaab(ba)babab
[1]⇒ aaaa(ba)abbabab
[1]⇒ aaaaaa(ba)bbabab
[1]⇒ aaaaaaaabb(ba)bab
[1]⇒ aaaaaaaab(ba)abbab
[1]⇒ aaaaaaaa(ba)ababbab
[1]⇒ aaaaaaaaaa(ba)babbab
[1]⇒ aaaaaaaaaaaab(ba)bbab
[1]⇒ aaaaaaaaaaaa(ba)abbbab
[1]⇒ aaaaaaaaaaaaaa(ba)bbbab
[1]⇒ aaaaaaaaaaaaaaaabbb(ba)b
[1]⇒ aaaaaaaaaaaaaaaabb(ba)abb
[1]⇒ aaaaaaaaaaaaaaaab(ba)ababb
[1]⇒ aaaaaaaaaaaaaaaa(ba)abababb
[1]⇒ aaaaaaaaaaaaaaaaaa(ba)bababb
[1]⇒ aaaaaaaaaaaaaaaaaaaab(ba)babb
[1]⇒ aaaaaaaaaaaaaaaaaaaa(ba)abbabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaa(ba)bbabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaabb(ba)bb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaab(ba)abbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaa(ba)ababbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaa(ba)babbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)bbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abbbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bbbb
[2]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(bbbbb)
⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Defines rule #1.