Certificate for #3818 ⟨a, b | aaab=ba, bbbb=1⟩

Back:⟨a, b | aaab=ba, bbbb=1⟩

Completion settings:

[1] ba=aaab

Axiom: aaab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[2] bbbb=1

Axiom: bbbb=1.

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=a

Overlap of [2] bbbb=1 with [1] ba=aaab:

bbb b ba

Critical pair: bbbaaab=a.

Reduce LHS:

[1]bb(ba)aab
[1]⇒ b(ba)aabaab
[1]⇒ (ba)aabaabaab
[1]⇒ aaa(ba)abaabaab
[1]⇒ aaaaaa(ba)baabaab
[1]⇒ aaaaaaaaab(ba)abaab
[1]⇒ aaaaaaaaa(ba)aababaab
[1]⇒ aaaaaaaaaaaa(ba)ababaab
[1]⇒ aaaaaaaaaaaaaaa(ba)babaab
[1]⇒ aaaaaaaaaaaaaaaaaab(ba)baab
[1]⇒ aaaaaaaaaaaaaaaaaa(ba)aabbaab
[1]⇒ aaaaaaaaaaaaaaaaaaaaa(ba)abbaab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaa(ba)bbaab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaabb(ba)ab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)aabab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)aabaabab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abaabab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)baabab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)abab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)aababab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)ababab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)babab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)bab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)aabbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bbab
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabb(ba)b
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)aabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)aabaabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abaabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)baabb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)abb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)aababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)ababb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)babb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaab(ba)bb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)aabbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)abbb
[1]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(ba)bbb
[2]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(bbbb)
⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Defines rule #1.