Certificate for #5766 ⟨a, b, c | aa=b, cbc=ac⟩

Completion settings:

• Auxiliary generators:
  1. d = bc
• Reduction order:
  • Left-to-right recursive path with deg(d) = 0; deg(c) = deg(b) = 1, c < b; deg(a) = 2

Axiom: aa=b.

Defines rule #7.

Referenced by [5], [6].

Axiom: cbc=ac.

Flip LHS and RHS.

Referenced by [4].

Axiom: bc=d.

Defines rule #3.

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

Simplify [2] ac=cbc.

Reduce RHS:

Defines rule #5.

Referenced by [6], [7].

Overlap of [1] aa=b with [1] aa=b:

Critical pair: ab=ba.

Flip LHS and RHS.

Defines rule #6.

Overlap of [1] aa=b with [4] ac=cd:

Critical pair: acd=bc.

Reduce LHS:

Reduce RHS:

Defines rule #1.

Referenced by [7], [8].

Overlap of [4] ac=cd with [6] cdd=d:

Critical pair: ad=cddd.

Reduce RHS:

Defines rule #4.

Overlap of [3] bc=d with [6] cdd=d:

Critical pair: bd=ddd.

Defines rule #2.