Certificate for #5009 ⟨a, b | aba=bb, aabbb=1⟩

Back:⟨a, b | aba=bb, aabbb=1⟩

Completion settings:

[1] aba=bb

Axiom: aba=bb.

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

[2] aabbb=1

Axiom: aabbb=1.

Referenced by [4], [6], [8], [9].

[3] bbba=abbb

Overlap of [1] aba=bb with [1] aba=bb:

ab a aba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Referenced by [6], [7].

[4] bbabbb=ab

Overlap of [1] aba=bb with [2] aabbb=1:

ab a aabbb

Critical pair: ab=bbabbb.

Flip LHS and RHS.

Referenced by [5].

[5] bbabbab=aab

Overlap of [4] bbabbb=ab with [4] bbabbb=ab:

bbabb b bbabbb

Critical pair: bbabbab=abbabbb.

Reduce RHS:

[4]a(bbabbb)
⇒ aab

Referenced by [7].

[6] ba=abbbbb

Overlap of [2] aabbb=1 with [3] bbba=abbb:

aab bb bbba

Critical pair: aababbb=ba.

Reduce LHS:

[1]a(aba)bbb
⇒ abbbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[7] aab=bbbbbbbbbb

Simplify [5] bbabbab=aab.

Reduce LHS:

[6]b(ba)bbab
[3]⇒ babbbb(bbba)b
[3]⇒ bab(bbba)bbbb
[1]⇒ b(aba)bbbbbbb
⇒ bbbbbbbbbb

Flip LHS and RHS.

Referenced by [8].

[8] bbbbbbbbbbbb=1

Overlap of [2] aabbb=1 with [7] aab=bbbbbbbbbb:

aabbb aab

Critical pair: bbbbbbbbbbbb=1.

Defines rule #1.

Referenced by [9].

[9] aa=bbbbbbbbb

Overlap of [2] aabbb=1 with [8] bbbbbbbbbbbb=1:

aa bbb bbbbbbbbbbbb

Critical pair: aa=bbbbbbbbb.

Defines rule #3.