Certificate for #1623 ⟨a, b, c | aab=ab, caa=1⟩

Back:⟨a, b, c | aab=ab, caa=1⟩

Completion settings:

[1] aab=ab

Axiom: aab=ab.

Referenced by [3], [4].

[2] caa=1

Axiom: caa=1.

Defines rule #3.

Referenced by [3], [4].

[3] cab=b

Overlap of [2] caa=1 with [1] aab=ab:

c aa aab

Critical pair: cab=b.

Referenced by [5].

[4] ab=b

Overlap of [2] caa=1 with [1] aab=ab:

ca a aab

Critical pair: caab=ab.

Reduce LHS:

[2](caa)b
⇒ b

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] cb=b

Simplify [3] cab=b.

Reduce LHS:

[4]c(ab)
⇒ cb

Defines rule #2.