Certificate for #25243 ⟨a, b | aa=a, babbb=abb⟩

Back:⟨a, b | aa=a, babbb=abb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [4], [5].

[2] babbb=abb

Axiom: babbb=abb.

Referenced by [3], [4], [7], [8].

[3] babbabb=ababb

Overlap of [2] babbb=abb with [2] babbb=abb:

babb b babbb

Critical pair: babbabb=abbabbb.

Reduce RHS:

[2]ab(babbb)
⇒ ababb

Referenced by [4], [5].

[4] bababb=abb

Overlap of [3] babbabb=ababb with [2] babbb=abb:

bab babb babbb

Critical pair: bababb=ababbb.

Reduce RHS:

[2]a(babbb)
[1]⇒ (aa)bb
⇒ abb

Referenced by [5], [6].

[5] ababb=babb

Overlap of [3] babbabb=ababb with [3] babbabb=ababb:

bab babb babbabb

Critical pair: babababb=ababbabb.

Reduce LHS:

[4]ba(bababb)
[1]⇒ b(aa)bb
⇒ babb

Reduce RHS:

[3]a(babbabb)
[1]⇒ (aa)babb
⇒ ababb

Flip LHS and RHS.

Referenced by [6].

[6] bbabb=abb

Simplify [4] bababb=abb.

Reduce LHS:

[5]b(ababb)
⇒ bbabb

Referenced by [7].

[7] babb=abbb

Overlap of [6] bbabb=abb with [2] babbb=abb:

b babb babbb

Critical pair: babb=abbb.

Defines rule #2.

Referenced by [8].

[8] abbbb=abb

Overlap of [2] babbb=abb with [7] babb=abbb:

babbb babb

Critical pair: abbbb=abb.

Defines rule #3.