Certificate for #5077 ⟨a, b | aaabbaa=baaa⟩

Completion settings:

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

Axiom: aaabbaa=baaa.

Referenced by [4].

Axiom: abb=c.

Defines rule #30.

Referenced by [4], [5], [6], [9], [11], [12], [21].

Axiom: aacac=d.

Defines rule #18.

Referenced by [6], [7], [8], [10], [13], [15], [28], [30], [33], [34], [44].

Overlap of [1] aaabbaa=baaa with [2] abb=c:

Critical pair: aacaa=baaa.

Flip LHS and RHS.

Defines rule #16.

Referenced by [5], [6], [7], [8], [21], [38], [39].

Overlap of [2] abb=c with [4] baaa=aacaa:

Critical pair: abaacaa=caaa.

Referenced by [23].

Overlap of [4] baaa=aacaa with [2] abb=c:

Critical pair: baac=aacaabb.

Reduce RHS:

Defines rule #26.

Referenced by [9], [10], [12], [23], [40].

Overlap of [4] baaa=aacaa with [3] aacac=d:

Critical pair: bad=aacaacac.

Reduce RHS:

Defines rule #15.

Referenced by [12], [16].

Overlap of [4] baaa=aacaa with [3] aacac=d:

Critical pair: baad=aacaaacac.

Reduce RHS:

Referenced by [20].

Overlap of [2] abb=c with [6] baac=d:

Critical pair: abd=caac.

Flip LHS and RHS.

Referenced by [14].

Overlap of [6] baac=d with [3] aacac=d:

Critical pair: bd=dac.

Defines rule #14.

Referenced by [11], [14].

Overlap of [2] abb=c with [10] bd=dac:

Critical pair: abdac=cd.

Reduce LHS:

Defines rule #19.

Referenced by [16], [17], [18], [19], [22], [29], [31], [32], [35], [36], [37], [45], [47], [48].

Overlap of [2] abb=c with [7] bad=aacd:

Critical pair: abaacd=cad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [13], [18], [19], [20].

Overlap of [3] aacac=d with [12] cad=add:

Critical pair: aacaadd=dad.

Referenced by [21], [24].

Simplify [9] caac=abd.

Reduce RHS:

Defines rule #20.

Referenced by [15], [17], [35], [38], [41].

Overlap of [3] aacac=d with [14] caac=adac:

Critical pair: aacaadac=daac.

Referenced by [25].

Overlap of [7] bad=aacd with [11] adacac=cd:

Critical pair: bcd=aacdacac.

Flip LHS and RHS.

Defines rule #31.

Referenced by [38], [39], [40], [41], [42], [43], [46].

Overlap of [11] adacac=cd with [14] caac=adac:

Critical pair: adacaadac=cdaac.

Referenced by [26].

Overlap of [11] adacac=cd with [12] cad=add:

Critical pair: adacaadd=cdad.

Referenced by [27].

Overlap of [12] cad=add with [11] adacac=cd:

Critical pair: ccd=addacac.

Defines rule #22.

Referenced by [37].

Simplify [8] baad=aacad.

Reduce RHS:

Defines rule #17.

Referenced by [21], [22].

Overlap of [2] abb=c with [20] baad=aaadd:

Critical pair: abaaadd=caad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [24], [25], [26], [27], [28], [29], [30], [31], [32], [34], [36], [37], [44], [45], [47], [48].

Overlap of [20] baad=aaadd with [11] adacac=cd:

Critical pair: bacd=aaaddacac.

Defines rule #29.

Overlap of [5] abaacaa=caaa with [6] baac=d:

Critical pair: adaa=caaa.

Flip LHS and RHS.

Defines rule #9.

Referenced by [28], [29], [35], [39], [42], [43].

Overlap of [13] aacaadd=dad with [21] caad=adad:

Critical pair: aaadadd=dad.

Defines rule #1.

Overlap of [15] aacaadac=daac with [21] caad=adad:

Critical pair: aaadadac=daac.

Defines rule #4.

Overlap of [17] adacaadac=cdaac with [21] caad=adad:

Critical pair: adaadadac=cdaac.

Flip LHS and RHS.

Defines rule #21.

Overlap of [18] adacaadd=cdad with [21] caad=adad:

Critical pair: adaadadd=cdad.

Flip LHS and RHS.

Defines rule #11.

Overlap of [3] aacac=d with [23] caaa=adaa:

Critical pair: aacaadaa=daaa.

Reduce LHS:

Defines rule #2.

Referenced by [46].

Overlap of [11] adacac=cd with [23] caaa=adaa:

Critical pair: adacaadaa=cdaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [3] aacac=d with [21] caad=adad:

Critical pair: aacaadad=daad.

Reduce LHS:

Defines rule #3.

Overlap of [11] adacac=cd with [21] caad=adad:

Critical pair: adacaadad=cdaad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [21] caad=adad with [11] adacac=cd:

Critical pair: cacd=adadacac.

Reduce RHS:

Defines rule #23.

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

Overlap of [3] aacac=d with [32] cacd=adcd:

Critical pair: aaadcd=dd.

Defines rule #5.

Overlap of [3] aacac=d with [32] cacd=adcd:

Critical pair: aacaadcd=dacd.

Reduce LHS:

Defines rule #6.

Overlap of [14] caac=adac with [32] cacd=adcd:

Critical pair: caaadcd=adacacd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [11] adacac=cd with [32] cacd=adcd:

Critical pair: adacaadcd=cdacd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [11] adacac=cd with [19] ccd=addacac:

Critical pair: adacaaddacac=cdcd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [4] baaa=aacaa with [16] aacdacac=bcd:

Critical pair: babcd=aacaacdacac.

Reduce RHS:

Defines rule #39.

Overlap of [4] baaa=aacaa with [16] aacdacac=bcd:

Critical pair: baabcd=aacaaacdacac.

Reduce RHS:

Defines rule #40.

Overlap of [6] baac=d with [16] aacdacac=bcd:

Critical pair: bbcd=ddacac.

Defines rule #38.

Overlap of [14] caac=adac with [16] aacdacac=bcd:

Critical pair: cbcd=adacdacac.

Defines rule #32.

Referenced by [48].

Overlap of [23] caaa=adaa with [16] aacdacac=bcd:

Critical pair: cabcd=adaacdacac.

Reduce RHS:

Defines rule #33.

Referenced by [44], [45].

Overlap of [23] caaa=adaa with [16] aacdacac=bcd:

Critical pair: caabcd=adaaacdacac.

Reduce RHS:

Defines rule #35.

Referenced by [47].

Overlap of [3] aacac=d with [42] cabcd=adbcd:

Critical pair: aacaadbcd=dabcd.

Reduce LHS:

Defines rule #27.

Overlap of [11] adacac=cd with [42] cabcd=adbcd:

Critical pair: adacaadbcd=cdabcd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #36.

Overlap of [28] aaadadaa=daaa with [16] aacdacac=bcd:

Critical pair: aaadadabcd=daaaacdacac.

Reduce RHS:

Defines rule #28.

Overlap of [11] adacac=cd with [43] caabcd=adabcd:

Critical pair: adacaadabcd=cdaabcd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #37.

Overlap of [11] adacac=cd with [41] cbcd=adacdacac:

Critical pair: adacaadacdacac=cdbcd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #34.