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

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] ababa=bbb

Axiom: ababa=bbb.

Defines rule #4.

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

[3] abbb=bbb

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

a a ababa

Critical pair: abbb=ababa.

Reduce RHS:

[2](ababa)
⇒ bbb

Defines rule #2.

Referenced by [5].

[4] bbba=bbb

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

abab a aa

Critical pair: ababa=bbba.

Reduce LHS:

[2](ababa)
⇒ bbb

Flip LHS and RHS.

Defines rule #3.

[5] bbbbbb=bbbbb

Overlap of [2] ababa=bbb with [3] abbb=bbb:

abab a abbb

Critical pair: ababbbb=bbbbbb.

Reduce LHS:

[3]ab(abbb)b
[3]⇒ (abbb)bb
⇒ bbbbb

Flip LHS and RHS.

Defines rule #5.