Certificate for #19809 ⟨a, b | aaa=a, abab=abb⟩

Back:⟨a, b | aaa=a, abab=abb⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #3.

Referenced by [6].

[2] abab=abb

Axiom: abab=abb.

Referenced by [4].

[3] ab=c

Axiom: ab=c.

Defines rule #1.

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

[4] abab=cb

Simplify [2] abab=abb.

Reduce RHS:

[3](ab)b
⇒ cb

Referenced by [5].

[5] cb=cc

Overlap of [4] abab=cb with [3] ab=c:

abab ab

Critical pair: cab=cb.

Reduce LHS:

[3]c(ab)
⇒ cc

Flip LHS and RHS.

Defines rule #2.

[6] aac=c

Overlap of [1] aaa=a with [3] ab=c:

aa a ab

Critical pair: aac=ab.

Reduce RHS:

[3](ab)
⇒ c

Defines rule #4.