Certificate for #2452 ⟨a, b, c | aab=b, caab=1⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #2.

Referenced by [2].

[2] cb=1

Axiom: caab=1.

Reduce LHS:

[1]c(aab)
⇒ cb

Defines rule #1.