Certificate for #25721 ⟨a, b | aa=a, bbbb=abab⟩

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

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abab=bbbb

Axiom: bbbb=abab.

Flip LHS and RHS.

Defines rule #2.

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

[3] abbbb=bbbb

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

a a abab

Critical pair: abbbb=abab.

Reduce RHS:

[2](abab)
⇒ bbbb

Defines rule #3.

Referenced by [4], [5].

[4] bbbbab=bbbbb

Overlap of [2] abab=bbbb with [2] abab=bbbb:

ab ab abab

Critical pair: abbbbb=bbbbab.

Reduce LHS:

[3](abbbb)b
⇒ bbbbb

Flip LHS and RHS.

Defines rule #4.

[5] bbbbbbb=bbbbb

Overlap of [2] abab=bbbb with [3] abbbb=bbbb:

ab ab abbbb

Critical pair: abbbbb=bbbbbbb.

Reduce LHS:

[3](abbbb)b
⇒ bbbbb

Flip LHS and RHS.

Defines rule #5.