Certificate for #4285 ⟨a, b | ababaaaab=ba⟩

Completion settings:

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

Axiom: ababaaaab=ba.

Referenced by [4].

Axiom: aaab=c.

Defines rule #27.

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

Axiom: ababa=d.

Referenced by [4], [5].

Overlap of [1] ababaaaab=ba with [3] ababa=d:

Critical pair: daaab=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #30.

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

Overlap of [3] ababa=d with [4] ba=dc:

Critical pair: adcba=d.

Reduce LHS:

Defines rule #1.

Referenced by [8], [9], [10], [11], [14], [18], [20], [22], [29], [32].

Overlap of [2] aaab=c with [4] ba=dc:

Critical pair: aaadc=ca.

Referenced by [9], [12], [17].

Overlap of [4] ba=dc with [2] aaab=c:

Critical pair: bc=dcaab.

Defines rule #28.

Overlap of [4] ba=dc with [5] adcdc=d:

Critical pair: bd=dcdcdc.

Defines rule #29.

Overlap of [6] aaadc=ca with [5] adcdc=d:

Critical pair: aad=cadc.

Defines rule #5.

Referenced by [10], [12], [17], [25].

Overlap of [9] aad=cadc with [5] adcdc=d:

Critical pair: ad=cadccdc.

Flip LHS and RHS.

Defines rule #2.

Referenced by [11], [12], [13], [19], [23].

Overlap of [5] adcdc=d with [10] cadccdc=ad:

Critical pair: adcdad=dadccdc.

Defines rule #6.

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

Overlap of [6] aaadc=ca with [10] cadccdc=ad:

Critical pair: aaadad=caadccdc.

Reduce LHS:

Reduce RHS:

Defines rule #21.

Referenced by [18], [19], [31].

Overlap of [10] cadccdc=ad with [10] cadccdc=ad:

Critical pair: cadccdad=adadccdc.

Flip LHS and RHS.

Defines rule #12.

Referenced by [30].

Overlap of [11] adcdad=dadccdc with [5] adcdc=d:

Critical pair: adcdd=dadccdccdc.

Flip LHS and RHS.

Defines rule #3.

Referenced by [16], [24], [33].

Overlap of [11] adcdad=dadccdc with [11] adcdad=dadccdc:

Critical pair: adcddadccdc=dadccdccdad.

Defines rule #14.

Overlap of [11] adcdad=dadccdc with [14] dadccdccdc=adcdd:

Critical pair: adcadcdd=dadccdcccdccdc.

Defines rule #11.

Overlap of [6] aaadc=ca with [9] aad=cadc:

Critical pair: acadcc=ca.

Defines rule #9.

Referenced by [25], [26].

Overlap of [12] acadcad=ccadcccdc with [5] adcdc=d:

Critical pair: acadcd=ccadcccdccdc.

Defines rule #10.

Referenced by [20], [21].

Overlap of [12] acadcad=ccadcccdc with [10] cadccdc=ad:

Critical pair: acadad=ccadcccdcccdc.

Defines rule #20.

Referenced by [29], [30].

Overlap of [18] acadcd=ccadcccdccdc with [5] adcdc=d:

Critical pair: acd=ccadcccdccdcc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [22], [23], [24], [25], [26], [27], [28].

Overlap of [18] acadcd=ccadcccdccdc with [11] adcdad=dadccdc:

Critical pair: acdadccdc=ccadcccdccdcad.

Defines rule #13.

Overlap of [5] adcdc=d with [20] ccadcccdccdcc=acd:

Critical pair: adcdacd=dcadcccdccdcc.

Defines rule #7.

Overlap of [10] cadccdc=ad with [20] ccadcccdccdcc=acd:

Critical pair: cadccdacd=adcadcccdccdcc.

Flip LHS and RHS.

Defines rule #16.

Referenced by [31].

Overlap of [14] dadccdccdc=adcdd with [20] ccadcccdccdcc=acd:

Critical pair: dadccdccdacd=adcddcadcccdccdcc.

Flip LHS and RHS.

Defines rule #19.

Overlap of [17] acadcc=ca with [20] ccadcccdccdcc=acd:

Critical pair: acadacd=caadcccdccdcc.

Reduce RHS:

Defines rule #23.

Overlap of [17] acadcc=ca with [20] ccadcccdccdcc=acd:

Critical pair: acadcacd=cacadcccdccdcc.

Reduce RHS:

Defines rule #24.

Overlap of [20] ccadcccdccdcc=acd with [20] ccadcccdccdcc=acd:

Critical pair: ccadcccdccdacd=acdadcccdccdcc.

Flip LHS and RHS.

Defines rule #17.

Overlap of [20] ccadcccdccdcc=acd with [20] ccadcccdccdcc=acd:

Critical pair: ccadcccdccdcacd=acdcadcccdccdcc.

Flip LHS and RHS.

Defines rule #18.

Overlap of [19] acadad=ccadcccdcccdc with [5] adcdc=d:

Critical pair: acadd=ccadcccdcccdccdc.

Defines rule #8.

Overlap of [19] acadad=ccadcccdcccdc with [13] adadccdc=cadccdad:

Critical pair: accadccdad=ccadcccdcccdcccdc.

Defines rule #22.

Referenced by [32], [33].

Overlap of [12] acadcad=ccadcccdc with [23] adcadcccdccdcc=cadccdacd:

Critical pair: accadccdacd=ccadcccdccccdccdcc.

Defines rule #25.

Overlap of [30] accadccdad=ccadcccdcccdcccdc with [5] adcdc=d:

Critical pair: accadccdd=ccadcccdcccdcccdccdc.

Defines rule #15.

Overlap of [30] accadccdad=ccadcccdcccdcccdc with [14] dadccdccdc=adcdd:

Critical pair: accadccadcdd=ccadcccdcccdcccdcccdccdc.

Defines rule #26.