Certificate for #3416 ⟨a, b, c | ba=ab, aac=b⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(c) = deg(a) = 0, c < a; deg(b) = 1

Axiom: ba=ab.

Flip LHS and RHS.

Referenced by [3].

Axiom: aac=b.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

Simplify [1] ab=ba.

Reduce RHS:

[2]	(b)a
	⇒ aaca

Referenced by [4].

a b b

Critical pair: aaac=aaca.

Defines rule #1.