Certificate for #19253 ⟨a, b | aaa=a, aabab=bb⟩

Back:⟨a, b | aaa=a, aabab=bb⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [3], [4].

[2] aabab=bb

Axiom: aabab=bb.

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

[3] abab=abb

Overlap of [1] aaa=a with [2] aabab=bb:

a aa aabab

Critical pair: abb=abab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[4] aabb=bb

Overlap of [1] aaa=a with [2] aabab=bb:

aa a aabab

Critical pair: aabb=aabab.

Reduce RHS:

[2](aabab)
⇒ bb

Defines rule #2.

[5] bbab=bbb

Overlap of [2] aabab=bb with [3] abab=abb:

aab ab abab

Critical pair: aababb=bbab.

Reduce LHS:

[2](aabab)b
⇒ bbb

Flip LHS and RHS.

Defines rule #4.