Certificate for #20226 ⟨a, b | aba=a, abbb=bba⟩

Back:⟨a, b | aba=a, abbb=bba⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #4.

Referenced by [3], [4].

[2] bba=abbb

Axiom: abbb=bba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] aabbbbbb=abbb

Overlap of [2] bba=abbb with [1] aba=a:

bb a aba

Critical pair: bba=abbbba.

Reduce LHS:

[2](bba)
⇒ abbb

Reduce RHS:

[2]abb(bba)
[2]⇒ a(bba)bbb
⇒ aabbbbbb

Flip LHS and RHS.

Referenced by [4], [5].

[4] abbbbbb=abbb

Overlap of [3] aabbbbbb=abbb with [2] bba=abbb:

aabbbbb b bba

Critical pair: aabbbbbabbb=abbbba.

Reduce LHS:

[2]aabbb(bba)bbb
[2]⇒ aab(bba)bbbbbb
[1]⇒ a(aba)bbbbbbbbb
[3]⇒ (aabbbbbb)bbb
⇒ abbbbbb

Reduce RHS:

[2]abb(bba)
[2]⇒ a(bba)bbb
[3]⇒ (aabbbbbb)
⇒ abbb

Defines rule #1.

Referenced by [5].

[5] aabbb=abbb

Overlap of [3] aabbbbbb=abbb with [4] abbbbbb=abbb:

a abbbbbb abbbbbb

Critical pair: aabbb=abbb.

Defines rule #3.