Certificate for #416 ⟨a, b, c | abc=b, caa=1⟩

Completion settings:

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

Axiom: abc=b.

Referenced by [5].

Axiom: caa=1.

Defines rule #9.

Referenced by [7], [8], [9], [10].

Axiom: ab=d.

Defines rule #7.

Referenced by [5], [6], [7].

Axiom: ad=e.

Defines rule #8.

Referenced by [6], [7], [8], [17], [18].

Overlap of [1] abc=b with [3] ab=d:

Critical pair: dc=b.

Defines rule #2.

Referenced by [6], [9], [11], [14], [15].

Overlap of [4] ad=e with [5] dc=b:

Critical pair: ab=ec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [10], [12], [13], [16].

Overlap of [2] caa=1 with [3] ab=d:

Critical pair: cad=b.

Reduce LHS:

Defines rule #5.

Referenced by [11], [12], [13].

Overlap of [2] caa=1 with [4] ad=e:

Critical pair: cae=d.

Defines rule #10.

Referenced by [15], [16].

Overlap of [5] dc=b with [2] caa=1:

Critical pair: d=baa.

Flip LHS and RHS.

Defines rule #12.

Overlap of [6] ec=d with [2] caa=1:

Critical pair: e=daa.

Flip LHS and RHS.

Defines rule #14.

Referenced by [17].

Overlap of [5] dc=b with [7] ce=b:

Critical pair: db=be.

Defines rule #6.

Overlap of [6] ec=d with [7] ce=b:

Critical pair: eb=de.

Defines rule #11.

Overlap of [7] ce=b with [6] ec=d:

Critical pair: cd=bc.

Defines rule #3.

Referenced by [14].

Overlap of [13] cd=bc with [5] dc=b:

Critical pair: cb=bcc.

Defines rule #1.

Overlap of [5] dc=b with [8] cae=d:

Critical pair: dd=bae.

Flip LHS and RHS.

Defines rule #13.

Overlap of [6] ec=d with [8] cae=d:

Critical pair: ed=dae.

Flip LHS and RHS.

Defines rule #15.

Referenced by [18].

Overlap of [4] ad=e with [10] daa=e:

Critical pair: ae=eaa.

Flip LHS and RHS.

Defines rule #16.

Overlap of [4] ad=e with [16] dae=ed:

Critical pair: aed=eae.

Flip LHS and RHS.

Defines rule #17.