Certificate for #3269 ⟨a, b, c | bb=ac, aacb=1⟩

Completion settings:

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

Axiom: bb=ac.

Referenced by [3], [4].

Axiom: aacb=1.

Referenced by [4], [6].

Overlap of [1] bb=ac with [1] bb=ac:

Critical pair: bac=acb.

Referenced by [5].

Overlap of [2] aacb=1 with [1] bb=ac:

Critical pair: aacac=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

Simplify [3] bac=acb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [6].

Overlap of [2] aacb=1 with [4] b=aacac:

Critical pair: aacaacac=1.

Reduce LHS:

Defines rule #2.