Certificate for #22787 ⟨a, b | aaa=1, abaab=bbb⟩

Back:⟨a, b | aaa=1, abaab=bbb⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #4.

Referenced by [3], [6].

[2] abaab=bbb

Axiom: abaab=bbb.

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

[3] baab=aabbb

Overlap of [1] aaa=1 with [2] abaab=bbb:

aa a abaab

Critical pair: aabbb=baab.

Flip LHS and RHS.

Defines rule #3.

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

[4] ababbb=aabbbbbbb

Overlap of [2] abaab=bbb with [2] abaab=bbb:

aba ab abaab

Critical pair: ababbb=bbbaab.

Reduce RHS:

[3]bb(baab)
[3]⇒ b(baab)bb
[3]⇒ (baab)bbbb
⇒ aabbbbbbb

Referenced by [6].

[5] babbb=abbbbbbb

Overlap of [3] baab=aabbb with [2] abaab=bbb:

ba ab abaab

Critical pair: babbb=aabbbaab.

Reduce RHS:

[3]aabb(baab)
[3]⇒ aab(baab)bb
[2]⇒ a(abaab)bbbb
⇒ abbbbbbb

Defines rule #2.

Referenced by [6].

[6] bbbbbbbbbbbbbbb=bbbbbbbb

Overlap of [3] baab=aabbb with [5] babbb=abbbbbbb:

baa b babbb

Critical pair: baaabbbbbbb=aabbbabbb.

Reduce LHS:

[1]b(aaa)bbbbbbb
⇒ bbbbbbbb

Reduce RHS:

[5]aabb(babbb)
[5]⇒ aab(babbb)bbbb
[4]⇒ a(ababbb)bbbbbbbb
[1]⇒ (aaa)bbbbbbbbbbbbbbb
⇒ bbbbbbbbbbbbbbb

Flip LHS and RHS.

Defines rule #1.