Certificate for #10711 ⟨a, b | aaab=aba, bbbb=1⟩

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

Completion settings:

[1] aba=aaab

Axiom: aaab=aba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[2] bbbb=1

Axiom: bbbb=1.

Defines rule #5.

Referenced by [5].

[3] aaabba=aaaaaaabb

Overlap of [1] aba=aaab with [1] aba=aaab:

ab a aba

Critical pair: abaaab=aaabba.

Reduce LHS:

[1](aba)aab
[1]⇒ aa(aba)ab
[1]⇒ aaaa(aba)b
⇒ aaaaaaabb

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] aaaaaaabbba=aaaaaaaaaaaaaaabbb

Overlap of [1] aba=aaab with [3] aaabba=aaaaaaabb:

ab a aaabba

Critical pair: abaaaaaaabb=aaabaabba.

Reduce LHS:

[1](aba)aaaaaabb
[1]⇒ aa(aba)aaaaabb
[1]⇒ aaaa(aba)aaaabb
[1]⇒ aaaaaa(aba)aaabb
[1]⇒ aaaaaaaa(aba)aabb
[1]⇒ aaaaaaaaaa(aba)abb
[1]⇒ aaaaaaaaaaaa(aba)bb
⇒ aaaaaaaaaaaaaaabbb

Reduce RHS:

[1]aa(aba)abba
[1]⇒ aaaa(aba)bba
⇒ aaaaaaabbba

Flip LHS and RHS.

Defines rule #4.

[5] aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa=aaaaaaaaaaaaaaaa

Overlap of [3] aaabba=aaaaaaabb with [3] aaabba=aaaaaaabb:

aaabb a aaabba

Critical pair: aaabbaaaaaaabb=aaaaaaabbaabba.

Reduce LHS:

[3](aaabba)aaaaaabb
[3]⇒ aaaa(aaabba)aaaaabb
[3]⇒ aaaaaaaa(aaabba)aaaabb
[3]⇒ aaaaaaaaaaaa(aaabba)aaabb
[3]⇒ aaaaaaaaaaaaaaaa(aaabba)aabb
[3]⇒ aaaaaaaaaaaaaaaaaaaa(aaabba)abb
[3]⇒ aaaaaaaaaaaaaaaaaaaaaaaa(aaabba)bb
[2]⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa(bbbb)
⇒ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa

Reduce RHS:

[3]aaaa(aaabba)abba
[3]⇒ aaaaaaaa(aaabba)bba
[2]⇒ aaaaaaaaaaaaaaa(bbbb)a
⇒ aaaaaaaaaaaaaaaa

Defines rule #1.