Certificate for #10273 ⟨a, b | aa=1, ababa=bbb⟩

Back:⟨a, b | aa=1, ababa=bbb⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

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

[2] ababa=bbb

Axiom: ababa=bbb.

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

[3] baba=abbb

Overlap of [1] aa=1 with [2] ababa=bbb:

a a ababa

Critical pair: abbb=baba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6].

[4] bbba=abab

Overlap of [2] ababa=bbb with [1] aa=1:

abab a aa

Critical pair: abab=bbba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] bbabbb=ababba

Overlap of [4] bbba=abab with [3] baba=abbb:

bb ba baba

Critical pair: bbabbb=ababba.

Defines rule #4.

Referenced by [6].

[6] babbbbbbb=ababbabba

Overlap of [5] bbabbb=ababba with [4] bbba=abab:

bbabb b bbba

Critical pair: bbabbabab=ababbabba.

Reduce LHS:

[3]bbab(baba)b
[3]⇒ b(baba)bbbb
⇒ babbbbbbb

Defines rule #5.

Referenced by [7].

[7] bbbbbbbbbb=abbabbabba

Overlap of [2] ababa=bbb with [6] babbbbbbb=ababbabba:

aba ba babbbbbbb

Critical pair: abaababbabba=bbbbbbbbbb.

Reduce LHS:

[1]ab(aa)babbabba
⇒ abbabbabba

Flip LHS and RHS.

Defines rule #6.

Referenced by [8].

[8] babbabbabba=abbabbabbab

Overlap of [7] bbbbbbbbbb=abbabbabba with [7] bbbbbbbbbb=abbabbabba:

b bbbbbbbbb bbbbbbbbbb

Critical pair: babbabbabba=abbabbabbab.

Defines rule #7.