Certificate for #22847 ⟨a, b | aaa=1, babbb=abb⟩

Back:⟨a, b | aaa=1, babbb=abb⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

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

[2] babbb=abb

Axiom: babbb=abb.

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

[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=aabb

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

bab babb babbb

Critical pair: bababb=ababbb.

Reduce RHS:

[2]a(babbb)
⇒ aabb

Referenced by [5], [8].

[5] aababb=bbb

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

bab babb babbabb

Critical pair: babababb=ababbabb.

Reduce LHS:

[4]ba(bababb)
[1]⇒ b(aaa)bb
⇒ bbb

Reduce RHS:

[3]a(babbabb)
⇒ aababb

Flip LHS and RHS.

Referenced by [6], [7].

[6] babb=abbb

Overlap of [1] aaa=1 with [5] aababb=bbb:

a aa aababb

Critical pair: abbb=babb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[7] bbbb=bb

Overlap of [5] aababb=bbb with [2] babbb=abb:

aa babb babbb

Critical pair: aaabb=bbbb.

Reduce LHS:

[1](aaa)bb
⇒ bb

Flip LHS and RHS.

Defines rule #3.

Referenced by [9].

[8] baabbb=aabb

Simplify [4] bababb=aabb.

Reduce LHS:

[6]ba(babb)
⇒ baabbb

Referenced by [9].

[9] baabb=aabbb

Overlap of [8] baabbb=aabb with [7] bbbb=bb:

baa bbb bbbb

Critical pair: baabb=aabbb.

Defines rule #4.