Certificate for #3812 ⟨a, b | abbabaaaab=a⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(b) = deg(d) = deg(c) = deg(e) = 0, b < d < c < e; deg(f) = deg(a) = 1, f < a
• Auxiliary generators:
  1. ab=c
  2. ac=d
  3. ad=e
  4. ebcaea=f

Axiom: abbabaaaab=a.

Referenced by [6].

Axiom: ab=c.

Referenced by [6], [8], [13], [25].

Axiom: ac=d.

Referenced by [6], [7], [8], [9], [14], [26], [28], [29], [30].

Axiom: ad=e.

Referenced by [6], [9], [10], [11], [12], [15], [27].

Axiom: ebcaea=f.

Referenced by [13], [14], [15], [16].

Overlap of [1] abbabaaaab=a with [2] ab=c:

Critical pair: cbabaaaab=a.

Reduce LHS:

Referenced by [7], [17].

Overlap of [3] ac=d with [6] cbcae=a:

Critical pair: aa=dbcae.

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

Overlap of [7] aa=dbcae with [2] ab=c:

Critical pair: ac=dbcaeb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [7] aa=dbcae with [3] ac=d:

Critical pair: ad=dbcaec.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12], [18].

Overlap of [7] aa=dbcae with [7] aa=dbcae:

Critical pair: adbcae=dbcaea.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [4] ad=e with [8] dbcaeb=d:

Critical pair: ad=ebcaeb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [4] ad=e with [9] dbcaec=e:

Critical pair: ae=ebcaec.

Flip LHS and RHS.

Referenced by [13], [22].

Overlap of [5] ebcaea=f with [2] ab=c:

Critical pair: ebcaec=fb.

Reduce LHS:

Referenced by [14], [15], [16], [17], [24].

Overlap of [5] ebcaea=f with [3] ac=d:

Critical pair: ebcaed=fc.

Reduce LHS:

Referenced by [31], [43], [46].

Overlap of [5] ebcaea=f with [4] ad=e:

Critical pair: ebcaee=fd.

Reduce LHS:

Referenced by [47].

Overlap of [5] ebcaea=f with [13] ae=fb:

Critical pair: ebcfba=f.

Referenced by [32].

Overlap of [6] cbcae=a with [13] ae=fb:

Critical pair: cbcfb=a.

Flip LHS and RHS.

Defines rule #21.

Referenced by [18], [19], [20], [21], [22], [23], [24], [25], [26], [27], [28], [29], [30], [32].

Overlap of [9] dbcaec=e with [17] a=cbcfb:

Critical pair: dbccbcfbec=e.

Referenced by [20].

Simplify [10] dbcaea=ebcae.

Reduce RHS:

Referenced by [20].

Overlap of [19] dbcaea=ebccbcfbe with [17] a=cbcfb:

Critical pair: dbccbcfbea=ebccbcfbe.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21], [23].

Overlap of [11] ebcaeb=e with [17] a=cbcfb:

Critical pair: ebccbcfbeb=e.

Reduce LHS:

Defines rule #11.

Referenced by [34].

Simplify [12] ebcaec=ae.

Reduce RHS:

Referenced by [23].

Overlap of [22] ebcaec=cbcfbe with [17] a=cbcfb:

Critical pair: ebccbcfbec=cbcfbe.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24], [29], [38].

Overlap of [13] ae=fb with [17] a=cbcfb:

Critical pair: cbcfbe=fb.

Reduce LHS:

Defines rule #17.

Referenced by [29], [32], [38], [40].

Overlap of [2] ab=c with [17] a=cbcfb:

Critical pair: cbcfbb=c.

Defines rule #10.

Referenced by [28], [35].

Overlap of [3] ac=d with [17] a=cbcfb:

Critical pair: cbcfbc=d.

Defines rule #16.

Referenced by [28], [30], [39].

Overlap of [4] ad=e with [17] a=cbcfb:

Critical pair: cbcfbd=e.

Defines rule #13.

Referenced by [29], [30], [31], [43].

Overlap of [3] ac=d with [25] cbcfbb=c:

Critical pair: ac=dbcfbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [36].

Overlap of [3] ac=d with [27] cbcfbd=e:

Critical pair: ae=dbcfbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [43], [44].

Overlap of [3] ac=d with [26] cbcfbc=d:

Critical pair: ad=dbcfbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [31], [37], [45].

Overlap of [30] dbcfbc=e with [27] cbcfbd=e:

Critical pair: dbcfbe=ebcfbd.

Reduce RHS:

Referenced by [48].

Simplify [16] ebcfba=f.

Reduce LHS:

Defines rule #25.

Referenced by [33], [34], [35], [36], [37], [39], [40], [41], [42], [44].

Overlap of [32] fbbcfb=f with [32] fbbcfb=f:

Critical pair: fbbcf=fbcfb.

Flip LHS and RHS.

Defines rule #24.

Overlap of [21] ebcfbb=e with [32] fbbcfb=f:

Critical pair: ebcf=ecfb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [40], [42], [45].

Overlap of [25] cbcfbb=c with [32] fbbcfb=f:

Critical pair: cbcf=ccfb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [39].

Overlap of [28] dbcfbb=d with [32] fbbcfb=f:

Critical pair: dbcf=dcfb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [37].

Overlap of [36] dcfb=dbcf with [32] fbbcfb=f:

Critical pair: dcf=dbcfbcfb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Simplify [23] cbcfbe=ebcfbc.

Reduce RHS:

Defines rule #19.

Overlap of [35] ccfb=cbcf with [32] fbbcfb=f:

Critical pair: ccf=cbcfbcfb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [34] ecfb=ebcf with [32] fbbcfb=f:

Critical pair: ecf=ebcfbcfb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [41], [42], [43], [44].

Overlap of [32] fbbcfb=f with [40] fbfb=ecf:

Critical pair: fbbcecf=ffb.

Flip LHS and RHS.

Defines rule #22.

Overlap of [40] fbfb=ecf with [32] fbbcfb=f:

Critical pair: fbf=ecfbcfb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [45].

Overlap of [27] cbcfbd=e with [29] dbcfbd=fb:

Critical pair: cbcfbfb=ebcfbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [45], [46], [48].

Overlap of [29] dbcfbd=fb with [29] dbcfbd=fb:

Critical pair: dbcfbfb=fbbcfbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [45], [47].

Overlap of [44] fd=dbcecf with [30] dbcfbc=e:

Critical pair: fe=dbcecfbcfbc.

Reduce RHS:

Defines rule #8.

Simplify [14] ebcfbd=fc.

Reduce RHS:

Defines rule #14.

Simplify [15] ebcfbe=fd.

Reduce RHS:

Defines rule #20.

Simplify [31] dbcfbe=fc.

Reduce RHS:

Defines rule #18.