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

Completion settings:

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

Axiom: aaabbaa=baaa.

Referenced by [4].

Axiom: abb=c.

Defines rule #29.

Referenced by [4], [5], [6], [9], [14], [21].

Axiom: aacac=d.

Defines rule #14.

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

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

Critical pair: aacaa=baaa.

Flip LHS and RHS.

Defines rule #24.

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

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], [14], [23].

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

Critical pair: bad=aacaacac.

Reduce RHS:

Defines rule #23.

Referenced by [14], [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.

Referenced by [11].

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

Critical pair: bd=dac.

Defines rule #22.

Referenced by [11].

Simplify [9] abd=caac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [12], [13], [17], [35].

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

Critical pair: aacaadac=daac.

Referenced by [24].

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

Critical pair: cd=adacac.

Flip LHS and RHS.

Defines rule #15.

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

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

Critical pair: abaacd=cad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

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

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

Critical pair: aacaadd=dad.

Referenced by [21], [25].

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

Critical pair: bcd=aacdacac.

Defines rule #27.

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

Critical pair: adacaadac=cdaac.

Referenced by [26].

Overlap of [13] adacac=cd with [14] cad=add:

Critical pair: adacaadd=cdad.

Referenced by [27].

Overlap of [14] cad=add with [13] adacac=cd:

Critical pair: ccd=addacac.

Defines rule #18.

Referenced by [37].

Simplify [8] baad=aacad.

Reduce RHS:

Defines rule #25.

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].

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

Critical pair: bacd=aaaddacac.

Defines rule #28.

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].

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

Critical pair: aaadadac=daac.

Defines rule #4.

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

Critical pair: aaadadd=dad.

Defines rule #1.

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

Critical pair: adaadadac=cdaac.

Flip LHS and RHS.

Defines rule #17.

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.

Overlap of [13] 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 [13] 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 [13] adacac=cd:

Critical pair: cacd=adadacac.

Reduce RHS:

Defines rule #19.

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 [11] caac=adac with [32] cacd=adcd:

Critical pair: caaadcd=adacacd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

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

Critical pair: adacaadcd=cdacd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

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

Critical pair: adacaaddacac=cdcd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.