Certificate for #12474 ⟨a, b | aabb=ba, abbb=a⟩

Back:⟨a, b | aabb=ba, abbb=a⟩

Completion settings:

[1] aabb=ba

Axiom: aabb=ba.

Referenced by [3].

[2] abbb=a

Axiom: abbb=a.

Defines rule #1.

Referenced by [3], [7], [8], [9], [10].

[3] aa=bab

Overlap of [1] aabb=ba with [2] abbb=a:

a abb abbb

Critical pair: aa=bab.

Defines rule #3.

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

[4] baba=abab

Overlap of [3] aa=bab with [3] aa=bab:

a a aa

Critical pair: abab=baba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [7].

[5] ababba=bbabbab

Overlap of [4] baba=abab with [4] baba=abab:

ba ba baba

Critical pair: baabab=ababba.

Reduce LHS:

[3]b(aa)bab
⇒ bbabbab

Flip LHS and RHS.

Defines rule #6.

Referenced by [6], [7].

[6] babbabba=abbabbab

Overlap of [3] aa=bab with [5] ababba=bbabbab:

a a ababba

Critical pair: abbabbab=babbabba.

Flip LHS and RHS.

Defines rule #7.

[7] bbbabbab=abbab

Overlap of [4] baba=abab with [5] ababba=bbabbab:

b aba ababba

Critical pair: bbbabbab=ababbba.

Reduce RHS:

[2]ab(abbb)a
[3]⇒ ab(aa)
⇒ abbab

Referenced by [8].

[8] bbbabba=abba

Overlap of [7] bbbabbab=abbab with [2] abbb=a:

bbbabb ab abbb

Critical pair: bbbabba=abbabbb.

Reduce RHS:

[2]abb(abbb)
⇒ abba

Defines rule #5.

Referenced by [9].

[9] bbbbabb=babb

Overlap of [8] bbbabba=abba with [3] aa=bab:

bbbabb a aa

Critical pair: bbbabbbab=abbaa.

Reduce LHS:

[2]bbb(abbb)ab
[3]⇒ bbb(aa)b
⇒ bbbbabb

Reduce RHS:

[3]abb(aa)
[2]⇒ (abbb)ab
[3]⇒ (aa)b
⇒ babb

Referenced by [10].

[10] bbbba=ba

Overlap of [9] bbbbabb=babb with [2] abbb=a:

bbbb abb abbb

Critical pair: bbbba=babbb.

Reduce RHS:

[2]b(abbb)
⇒ ba

Defines rule #2.