Certificate for #24660 ⟨a, b | aa=a, ababab=bb⟩

Back:⟨a, b | aa=a, ababab=bb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] ababab=bb

Axiom: ababab=bb.

Defines rule #5.

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

[3] abb=bb

Overlap of [1] aa=a with [2] ababab=bb:

a a ababab

Critical pair: abb=ababab.

Reduce RHS:

[2](ababab)
⇒ bb

Defines rule #2.

Referenced by [4], [5].

[4] bbab=bbb

Overlap of [2] ababab=bb with [2] ababab=bb:

ab abab ababab

Critical pair: abbb=bbab.

Reduce LHS:

[3](abb)b
⇒ bbb

Flip LHS and RHS.

Defines rule #3.

[5] bbbb=bbb

Overlap of [2] ababab=bb with [3] abb=bb:

abab ab abb

Critical pair: ababbb=bbb.

Reduce LHS:

[3]ab(abb)b
[3]⇒ (abb)bb
⇒ bbbb

Defines rule #4.