Certificate for #4527 ⟨a, b | aaababba=baa⟩

Completion settings:

• Auxiliary generators:
  1. c = bb
  2. d = aabac
• Reduction order:
  • Right-to-left recursive path with deg(a) = deg(d) = 0, a < d; deg(c) = deg(b) = 1, c < b

Axiom: aaababba=baa.

Referenced by [4].

Axiom: bb=c.

Defines rule #33.

Referenced by [4], [5], [6], [10].

Axiom: aabac=d.

Defines rule #21.

Referenced by [4], [7], [8], [9], [11], [13], [14], [27], [30], [33].

Overlap of [1] aaababba=baa with [2] bb=c:

Critical pair: aaabaca=baa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [6], [8], [9], [11], [13], [15], [18], [19], [22], [25], [26], [30], [31], [32], [33], [34], [35], [37], [39], [40], [45], [47], [48].

Overlap of [2] bb=c with [2] bb=c:

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #29.

Referenced by [7], [17], [20], [36].

Overlap of [2] bb=c with [4] baa=ada:

Critical pair: bada=caa.

Referenced by [12].

Overlap of [3] aabac=d with [5] cb=bc:

Critical pair: aababc=db.

Defines rule #45.

Referenced by [21].

Overlap of [4] baa=ada with [3] aabac=d:

Critical pair: bd=adabac.

Flip LHS and RHS.

Defines rule #22.

Referenced by [15], [16], [17], [18], [19], [20], [28], [31], [34], [47].

Overlap of [4] baa=ada with [3] aabac=d:

Critical pair: bad=adaabac.

Reduce RHS:

Defines rule #12.

Referenced by [10], [12].

Overlap of [2] bb=c with [9] bad=add:

Critical pair: badd=cad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [11], [19], [20], [24], [26], [36], [38], [42].

Overlap of [3] aabac=d with [10] cad=addd:

Critical pair: aabaaddd=dad.

Reduce LHS:

Defines rule #2.

Referenced by [43].

Simplify [6] bada=caa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [13], [14], [16], [18], [21], [23], [25], [41], [46].

Overlap of [3] aabac=d with [12] caa=adda:

Critical pair: aabaadda=daa.

Reduce LHS:

Defines rule #1.

Referenced by [44].

Overlap of [12] caa=adda with [3] aabac=d:

Critical pair: cd=addabac.

Flip LHS and RHS.

Defines rule #23.

Referenced by [22], [23], [24], [25], [26], [29], [32], [35], [43], [48].

Overlap of [4] baa=ada with [8] adabac=bd:

Critical pair: babd=adadabac.

Reduce RHS:

Defines rule #34.

Overlap of [12] caa=adda with [8] adabac=bd:

Critical pair: cabd=addadabac.

Reduce RHS:

Defines rule #30.

Referenced by [33], [34], [35].

Overlap of [8] adabac=bd with [5] cb=bc:

Critical pair: adababc=bdb.

Defines rule #46.

Referenced by [37].

Overlap of [8] adabac=bd with [12] caa=adda:

Critical pair: adabaadda=bdaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [8] adabac=bd with [10] cad=addd:

Critical pair: adabaaddd=bdad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [49].

Overlap of [10] cad=addd with [8] adabac=bd:

Critical pair: cbd=adddabac.

Reduce LHS:

Defines rule #25.

Referenced by [36], [37], [39].

Overlap of [12] caa=adda with [7] aababc=db:

Critical pair: cdb=addababc.

Flip LHS and RHS.

Defines rule #47.

Referenced by [38], [39].

Overlap of [4] baa=ada with [14] addabac=cd:

Critical pair: bacd=adaddabac.

Reduce RHS:

Defines rule #26.

Referenced by [27], [28], [29].

Overlap of [12] caa=adda with [14] addabac=cd:

Critical pair: cacd=addaddabac.

Reduce RHS:

Defines rule #18.

Referenced by [30], [31], [32].

Overlap of [10] cad=addd with [14] addabac=cd:

Critical pair: ccd=addddabac.

Flip LHS and RHS.

Defines rule #24.

Referenced by [40], [41], [42], [43], [44], [49], [50].

Overlap of [14] addabac=cd with [12] caa=adda:

Critical pair: addabaadda=cdaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [14] addabac=cd with [10] cad=addd:

Critical pair: addabaaddd=cdad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [50].

Overlap of [3] aabac=d with [22] bacd=adcd:

Critical pair: aaadcd=dd.

Defines rule #3.

Overlap of [8] adabac=bd with [22] bacd=adcd:

Critical pair: adaadcd=bdd.

Flip LHS and RHS.

Defines rule #13.

Overlap of [14] addabac=cd with [22] bacd=adcd:

Critical pair: addaadcd=cdd.

Flip LHS and RHS.

Defines rule #7.

Overlap of [3] aabac=d with [23] cacd=addcd:

Critical pair: aabaaddcd=dacd.

Reduce LHS:

Defines rule #4.

Overlap of [8] adabac=bd with [23] cacd=addcd:

Critical pair: adabaaddcd=bdacd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [14] addabac=cd with [23] cacd=addcd:

Critical pair: addabaaddcd=cdacd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [3] aabac=d with [16] cabd=addbd:

Critical pair: aabaaddbd=dabd.

Reduce LHS:

Defines rule #10.

Overlap of [8] adabac=bd with [16] cabd=addbd:

Critical pair: adabaaddbd=bdabd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #36.

Overlap of [14] addabac=cd with [16] cabd=addbd:

Critical pair: addabaaddbd=cdabd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #32.

Overlap of [5] cb=bc with [20] bcd=adddabac:

Critical pair: cadddabac=bccd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #41.

Overlap of [17] adababc=bdb with [20] bcd=adddabac:

Critical pair: adabaadddabac=bdbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #35.

Overlap of [10] cad=addd with [21] addababc=cdb:

Critical pair: ccdb=addddababc.

Defines rule #48.

Overlap of [21] addababc=cdb with [20] bcd=adddabac:

Critical pair: addabaadddabac=cdbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #31.

Overlap of [4] baa=ada with [24] addddabac=ccd:

Critical pair: baccd=adaddddabac.

Reduce RHS:

Defines rule #42.

Overlap of [12] caa=adda with [24] addddabac=ccd:

Critical pair: caccd=addaddddabac.

Reduce RHS:

Defines rule #38.

Referenced by [47], [48].

Overlap of [10] cad=addd with [24] addddabac=ccd:

Critical pair: cccd=addddddabac.

Defines rule #37.

Overlap of [11] aaadaddd=dad with [24] addddabac=ccd:

Critical pair: aaadccd=daddabac.

Reduce RHS:

Defines rule #16.

Referenced by [45], [46].

Overlap of [13] aaadadda=daa with [24] addddabac=ccd:

Critical pair: aaadaddccd=daaddddabac.

Reduce RHS:

Defines rule #17.

Overlap of [4] baa=ada with [43] aaadccd=dcd:

Critical pair: bdcd=adaadccd.

Defines rule #27.

Overlap of [12] caa=adda with [43] aaadccd=dcd:

Critical pair: cdcd=addaadccd.

Defines rule #19.

Overlap of [8] adabac=bd with [41] caccd=addccd:

Critical pair: adabaaddccd=bdaccd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #44.

Overlap of [14] addabac=cd with [41] caccd=addccd:

Critical pair: addabaaddccd=cdaccd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #40.

Overlap of [19] bdad=adaadaddd with [24] addddabac=ccd:

Critical pair: bdccd=adaadaddddddabac.

Defines rule #43.

Overlap of [26] cdad=addaadaddd with [24] addddabac=ccd:

Critical pair: cdccd=addaadaddddddabac.

Defines rule #39.