Certificate for #9155 ⟨a, b | aa=a, abba=bbb⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] abba=bbb

Axiom: abba=bbb.

Defines rule #2.

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

[3] abbb=bbb

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

a a abba

Critical pair: abbb=abba.

Reduce RHS:

[2](abba)
⇒ bbb

Defines rule #3.

Referenced by [5].

[4] bbba=bbb

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

abb a aa

Critical pair: abba=bbba.

Reduce LHS:

[2](abba)
⇒ bbb

Flip LHS and RHS.

Defines rule #4.

[5] bbbbbb=bbbbb

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

abb a abbb

Critical pair: abbbbb=bbbbbb.

Reduce LHS:

[3](abbb)bb
⇒ bbbbb

Flip LHS and RHS.

Defines rule #5.