Certificate for #25722 ⟨a, b | aa=a, bbbb=abba⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] abba=bbbb

Axiom: bbbb=abba.

Flip LHS and RHS.

Defines rule #2.

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

[3] abbbb=bbbb

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

a a abba

Critical pair: abbbb=abba.

Reduce RHS:

[2](abba)
⇒ bbbb

Defines rule #4.

[4] bbbba=bbbb

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

abb a aa

Critical pair: abba=bbbba.

Reduce LHS:

[2](abba)
⇒ bbbb

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] bbbbbbbb=bbbbbb

Overlap of [4] bbbba=bbbb with [2] abba=bbbb:

bbbb a abba

Critical pair: bbbbbbbb=bbbbbba.

Reduce RHS:

[4]bb(bbbba)
⇒ bbbbbb

Defines rule #5.