Certificate for #2794 ⟨a, b, c | abc=b, caaa=1⟩

Completion settings:

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

Axiom: abc=b.

Referenced by [6].

Axiom: caaa=1.

Defines rule #24.

Referenced by [9], [10], [11], [12], [13], [14].

Axiom: ab=d.

Defines rule #11.

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

Axiom: ad=e.

Defines rule #12.

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

Axiom: ae=f.

Defines rule #13.

Referenced by [8], [9], [10], [11], [24], [28], [29].

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

Critical pair: dc=b.

Defines rule #2.

Referenced by [7], [12], [15], [20], [23], [25].

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

Critical pair: ab=ec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [8], [13], [16], [19], [21], [26].

Overlap of [5] ae=f with [7] ec=d:

Critical pair: ad=fc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [14], [17], [18], [22], [27].

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

Critical pair: caad=b.

Reduce LHS:

Defines rule #7.

Referenced by [15], [16], [17], [18].

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

Critical pair: caae=d.

Reduce LHS:

Defines rule #14.

Referenced by [20], [21], [22].

Overlap of [2] caaa=1 with [5] ae=f:

Critical pair: caaf=e.

Defines rule #19.

Referenced by [25], [26], [27].

Overlap of [6] dc=b with [2] caaa=1:

Critical pair: d=baaa.

Flip LHS and RHS.

Defines rule #25.

Overlap of [7] ec=d with [2] caaa=1:

Critical pair: e=daaa.

Flip LHS and RHS.

Defines rule #26.

Overlap of [8] fc=e with [2] caaa=1:

Critical pair: f=eaaa.

Flip LHS and RHS.

Defines rule #27.

Referenced by [28].

Overlap of [6] dc=b with [9] cf=b:

Critical pair: db=bf.

Defines rule #8.

Overlap of [7] ec=d with [9] cf=b:

Critical pair: eb=df.

Defines rule #9.

Overlap of [8] fc=e with [9] cf=b:

Critical pair: fb=ef.

Defines rule #10.

Overlap of [9] cf=b with [8] fc=e:

Critical pair: ce=bc.

Defines rule #5.

Referenced by [19].

Overlap of [18] ce=bc with [7] ec=d:

Critical pair: cd=bcc.

Defines rule #3.

Referenced by [23].

Overlap of [6] dc=b with [10] caf=d:

Critical pair: dd=baf.

Flip LHS and RHS.

Defines rule #15.

Overlap of [7] ec=d with [10] caf=d:

Critical pair: ed=daf.

Flip LHS and RHS.

Defines rule #16.

Overlap of [8] fc=e with [10] caf=d:

Critical pair: fd=eaf.

Flip LHS and RHS.

Defines rule #17.

Referenced by [24].

Overlap of [19] cd=bcc with [6] dc=b:

Critical pair: cb=bccc.

Defines rule #1.

Overlap of [5] ae=f with [22] eaf=fd:

Critical pair: afd=faf.

Flip LHS and RHS.

Defines rule #18.

Overlap of [6] dc=b with [11] caaf=e:

Critical pair: de=baaf.

Flip LHS and RHS.

Defines rule #20.

Overlap of [7] ec=d with [11] caaf=e:

Critical pair: ee=daaf.

Flip LHS and RHS.

Defines rule #21.

Overlap of [8] fc=e with [11] caaf=e:

Critical pair: fe=eaaf.

Flip LHS and RHS.

Defines rule #22.

Referenced by [29].

Overlap of [5] ae=f with [14] eaaa=f:

Critical pair: af=faaa.

Flip LHS and RHS.

Defines rule #28.

Overlap of [5] ae=f with [27] eaaf=fe:

Critical pair: afe=faaf.

Flip LHS and RHS.

Defines rule #23.