Certificate for #12043 ⟨a, b | abab=aa, bbbbb=1⟩

Back:⟨a, b | abab=aa, bbbbb=1⟩

Completion settings:

[1] abab=aa

Axiom: abab=aa.

Referenced by [3], [4].

[2] bbbbb=1

Axiom: bbbbb=1.

Defines rule #1.

Referenced by [4], [6], [7].

[3] abaa=aaab

Overlap of [1] abab=aa with [1] abab=aa:

ab ab abab

Critical pair: abaa=aaab.

Referenced by [5].

[4] aba=aabbbb

Overlap of [1] abab=aa with [2] bbbbb=1:

aba b bbbbb

Critical pair: aba=aabbbb.

Defines rule #2.

Referenced by [5], [6], [7].

[5] aabbbba=aaab

Simplify [3] abaa=aaab.

Reduce LHS:

[4](aba)a
⇒ aabbbba

Defines rule #3.

Referenced by [6], [7].

[6] aaaabbba=aaaaabb

Overlap of [5] aabbbba=aaab with [5] aabbbba=aaab:

aabbbb a aabbbba

Critical pair: aabbbbaaab=aaababbbba.

Reduce LHS:

[5](aabbbba)aab
[4]⇒ aa(aba)ab
[5]⇒ aa(aabbbba)b
⇒ aaaaabb

Reduce RHS:

[4]aa(aba)bbbba
[2]⇒ aaaa(bbbbb)bbba
⇒ aaaabbba

Flip LHS and RHS.

Defines rule #5.

[7] aaabba=aaaabbb

Overlap of [5] aabbbba=aaab with [4] aba=aabbbb:

aabbbb a aba

Critical pair: aabbbbaabbbb=aaabba.

Reduce LHS:

[5](aabbbba)abbbb
[4]⇒ aa(aba)bbbb
[2]⇒ aaaa(bbbbb)bbb
⇒ aaaabbb

Flip LHS and RHS.

Defines rule #4.