Certificate for #15200 ⟨a, b | aab=ba, bbbbbb=1⟩

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

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] bbbbbb=1

Axiom: bbbbbb=1.

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=a

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

bbbbb b ba

Critical pair: bbbbbaab=a.

Reduce LHS:

[1]bbbb(ba)ab
[1]⇒ bbb(ba)abab
[1]⇒ bb(ba)ababab
[1]⇒ b(ba)abababab
[1]⇒ (ba)ababababab
[1]⇒ aa(ba)babababab
[1]⇒ aaaab(ba)bababab
[1]⇒ aaaa(ba)abbababab
[1]⇒ aaaaaa(ba)bbababab
[1]⇒ aaaaaaaabb(ba)babab
[1]⇒ aaaaaaaab(ba)abbabab
[1]⇒ aaaaaaaa(ba)ababbabab
[1]⇒ aaaaaaaaaa(ba)babbabab
[1]⇒ aaaaaaaaaaaab(ba)bbabab
[1]⇒ aaaaaaaaaaaa(ba)abbbabab
[1]⇒ aaaaaaaaaaaaaa(ba)bbbabab
[1]⇒ aaaaaaaaaaaaaaaabbb(ba)bab
[1]⇒ aaaaaaaaaaaaaaaabb(ba)abbab
[1]⇒ aaaaaaaaaaaaaaaab(ba)ababbab
[1]⇒ aaaaaaaaaaaaaaaa(ba)abababbab
[1]⇒ aaaaaaaaaaaaaaaaaa(ba)bababbab
[1]⇒ aaaaaaaaaaaaaaaaaaaab(ba)babbab
[1]⇒ aaaaaaaaaaaaaaaaaaaa(ba)abbabbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaa(ba)bbabbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaabb(ba)bbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaab(ba)abbbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaa(ba)ababbbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaa(ba)babbbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)bbbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abbbbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bbbbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabbbb(ba)b
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabbb(ba)abb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabb(ba)ababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)abababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)ababababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)babababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)bababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abbababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bbababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabb(ba)babb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)abbabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)ababbabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)babbabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)bbabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abbbabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bbbabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabbb(ba)bb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabb(ba)abbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)ababbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abababbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bababbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)babbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abbabbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bbabbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabb(ba)bbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)abbbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)ababbbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)babbbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)bbbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abbbbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bbbbb
[2]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(bbbbbb)
⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Defines rule #1.