Certificate for #3044 ⟨a, b | aabaabbabaa=1⟩

Completion settings:

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

Axiom: aabaabbabaa=1.

Referenced by [4].

Axiom: bbab=c.

Defines rule #10.

Referenced by [4], [6], [8], [17], [18], [21], [24], [25].

Axiom: abaac=d.

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

Overlap of [1] aabaabbabaa=1 with [2] bbab=c:

Critical pair: aabaacaa=1.

Reduce LHS:

Referenced by [5], [7], [9], [12].

Overlap of [4] adaa=1 with [4] adaa=1:

Critical pair: ada=daa.

Flip LHS and RHS.

Referenced by [7].

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

Critical pair: bbac=cbab.

Defines rule #15.

Overlap of [5] daa=ada with [4] adaa=1:

Critical pair: da=adadaa.

Reduce RHS:

Defines rule #1.

Referenced by [9], [10], [11], [12], [14], [15], [16], [28], [29], [31], [32], [38], [39], [40].

Overlap of [2] bbab=c with [3] abaac=d:

Critical pair: bbd=caac.

Flip LHS and RHS.

Defines rule #5.

Referenced by [10], [11], [31], [38].

Overlap of [4] adaa=1 with [3] abaac=d:

Critical pair: adad=baac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [17], [19], [28], [29], [32], [36].

Overlap of [8] caac=bbd with [8] caac=bbd:

Critical pair: caabbd=bbdaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [9] baac=aadd with [8] caac=bbd:

Critical pair: baabbd=aaddaac.

Reduce RHS:

Referenced by [13].

Overlap of [4] adaa=1 with [7] da=ad:

Critical pair: aada=1.

Reduce LHS:

Defines rule #2.

Referenced by [13], [16], [20], [22], [23], [26], [27], [28], [29], [30], [31], [32], [35], [36], [38], [39], [40], [41], [42].

Simplify [11] baabbd=aaaaddc.

Reduce RHS:

Referenced by [14].

Overlap of [13] baabbd=adc with [7] da=ad:

Critical pair: baabbad=adca.

Referenced by [15].

Overlap of [14] baabbad=adca with [7] da=ad:

Critical pair: baabbaad=adcaa.

Referenced by [16].

Overlap of [15] baabbaad=adcaa with [7] da=ad:

Critical pair: baabbaaad=adcaaa.

Reduce LHS:

Defines rule #9.

Referenced by [17], [18], [19], [28], [29], [33].

Overlap of [16] baabb=adcaaa with [2] bbab=c:

Critical pair: baac=adcaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [16] baabb=adcaaa with [2] bbab=c:

Critical pair: baabc=adcaaabab.

Defines rule #13.

Overlap of [16] baabb=adcaaa with [9] baac=aadd:

Critical pair: baabaadd=adcaaaaac.

Flip LHS and RHS.

Referenced by [30], [31].

Overlap of [12] aaad=1 with [17] adcaaaab=aadd:

Critical pair: aaaadd=caaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [21], [22], [27].

Overlap of [20] caaaab=ad with [2] bbab=c:

Critical pair: caaaac=adbab.

Defines rule #6.

Referenced by [22], [37].

Overlap of [21] caaaac=adbab with [20] caaaab=ad:

Critical pair: caaaaad=adbabaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [12] aaad=1 with [22] adbabaaaab=caa:

Critical pair: aacaa=babaaaab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [24], [25], [34].

Overlap of [2] bbab=c with [23] babaaaab=aacaa:

Critical pair: bbaaacaa=cabaaaab.

Referenced by [26], [27].

Overlap of [23] babaaaab=aacaa with [2] bbab=c:

Critical pair: babaaaac=aacaabab.

Defines rule #21.

Overlap of [24] bbaaacaa=cabaaaab with [12] aaad=1:

Critical pair: bbaaac=cabaaaabad.

Defines rule #19.

Referenced by [29].

Overlap of [24] bbaaacaa=cabaaaab with [20] caaaab=ad:

Critical pair: bbaaaad=cabaaaabaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [9] baac=aadd with [27] cabaaaabaab=bba:

Critical pair: baabba=aaddabaaaabaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [16] baabb=adcaaa with [26] bbaaac=cabaaaabad:

Critical pair: baacabaaaabad=adcaaaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [12] aaad=1 with [19] adcaaaaac=baabaadd:

Critical pair: aabaabaadd=caaaaac.

Flip LHS and RHS.

Defines rule #7.

Referenced by [32], [39].

Overlap of [19] adcaaaaac=baabaadd with [8] caac=bbd:

Critical pair: adcaaaaabbd=baabaaddaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [9] baac=aadd with [30] caaaaac=aabaabaadd:

Critical pair: baaaabaabaadd=aaddaaaaac.

Reduce RHS:

Referenced by [33], [34].

Overlap of [16] baabb=adcaaa with [32] baaaabaabaadd=ac:

Critical pair: baabac=adcaaaaaaabaabaadd.

Defines rule #16.

Overlap of [23] babaaaab=aacaa with [32] baaaabaabaadd=ac:

Critical pair: babaaaaac=aacaaaaaabaabaadd.

Defines rule #23.

Overlap of [12] aaad=1 with [28] dbaaaabaab=adcaaaa:

Critical pair: aaaadcaaaa=baaaabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [36].

Overlap of [35] baaaabaab=acaaaa with [9] baac=aadd:

Critical pair: baaaabaaaadd=acaaaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37], [38], [39], [40].

Overlap of [21] caaaac=adbab with [36] acaaaaaac=baaaabad:

Critical pair: caaabaaaabad=adbabaaaaaac.

Flip LHS and RHS.

Referenced by [42].

Overlap of [36] acaaaaaac=baaaabad with [8] caac=bbd:

Critical pair: acaaaaaabbd=baaaabadaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [36] acaaaaaac=baaaabad with [30] caaaaac=aabaabaadd:

Critical pair: acaaaaaaaabaabaadd=baaaabadaaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [36] acaaaaaac=baaaabad with [36] acaaaaaac=baaaabad:

Critical pair: acaaaaabaaaabad=baaaabadaaaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [12] aaad=1 with [29] adcaaaaaac=dbaaaabad:

Critical pair: aadbaaaabad=caaaaaac.

Flip LHS and RHS.

Defines rule #8.

Overlap of [12] aaad=1 with [37] adbabaaaaaac=caaabaaaabad:

Critical pair: aacaaabaaaabad=babaaaaaac.

Flip LHS and RHS.

Defines rule #24.