Certificate for #4356 ⟨a, b | abbbabbba=ab⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(a) = 0; deg(b) = deg(c) = 1, b < c
• Auxiliary generators:
  1. abbbbbb=c

Axiom: abbbabbba=ab.

Referenced by [3], [4], [5], [6], [7], [27].

Axiom: abbbbbb=c.

Defines rule #24.

Referenced by [4], [8], [14], [15], [16], [17], [18], [19], [20], [21], [22], [23], [45], [49], [50], [51].

Overlap of [1] abbbabbba=ab with [1] abbbabbba=ab:

Critical pair: abbbab=abbbba.

Defines rule #11.

Referenced by [4], [5], [6], [7], [8], [9], [10], [15], [20], [27], [45].

Overlap of [1] abbbabbba=ab with [2] abbbbbb=c:

Critical pair: abbbabbbc=abbbbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [5], [9], [16], [21], [24], [26], [28].

Overlap of [1] abbbabbba=ab with [4] abbbbabbc=cb:

Critical pair: abbbabbbcb=abbbbbabbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [1] abbbabbba=ab with [3] abbbab=abbbba:

Critical pair: abbbbabba=ab.

Referenced by [10], [11], [12], [14], [17], [22].

Overlap of [1] abbbabbba=ab with [3] abbbab=abbbba:

Critical pair: abbbabbbba=abb.

Reduce LHS:

Referenced by [9], [13].

Overlap of [3] abbbab=abbbba with [2] abbbbbb=c:

Critical pair: abbbc=abbbbabbbbb.

Flip LHS and RHS.

Referenced by [31].

Overlap of [3] abbbab=abbbba with [4] abbbbabbc=cb:

Critical pair: abbbcb=abbbbabbbabbc.

Reduce RHS:

Defines rule #20.

Referenced by [12], [19], [23], [45].

Overlap of [6] abbbbabba=ab with [3] abbbab=abbbba:

Critical pair: abbbbabbabbbba=abbbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [11], [12], [13], [14], [24], [26], [27], [28], [31].

Overlap of [6] abbbbabba=ab with [6] abbbbabba=ab:

Critical pair: abbbbabbab=abbbbbabba.

Reduce LHS:

Referenced by [12], [14].

Overlap of [6] abbbbabba=ab with [9] abbbcb=abbbbc:

Critical pair: abbbbabbabbbbc=abbbbcb.

Reduce LHS:

Referenced by [32].

Simplify [7] abbbbabbba=abb.

Reduce LHS:

Referenced by [14], [15], [16], [17], [18], [19], [30].

Overlap of [6] abbbbabba=ab with [13] abbbbbabba=abb:

Critical pair: abbbbabbabb=abbbbbbabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [17], [20], [21], [22], [23], [25].

Overlap of [13] abbbbbabba=abb with [3] abbbab=abbbba:

Critical pair: abbbbbabbabbbba=abbbbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [16], [17], [18], [19], [24], [26], [27], [28], [29], [30], [31], [32].

Overlap of [13] abbbbbabba=abb with [4] abbbbabbc=cb:

Critical pair: abbbbbabbcb=abbbbbbabbc.

Reduce LHS:

Reduce RHS:

Referenced by [33].

Overlap of [13] abbbbbabba=abb with [6] abbbbabba=ab:

Critical pair: abbbbbabbab=abbbbbbabba.

Reduce LHS:

Reduce RHS:

Referenced by [18], [19].

Overlap of [13] abbbbbabba=abb with [13] abbbbbabba=abb:

Critical pair: abbbbbabbabb=abbbbbbbabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [22], [35].

Overlap of [13] abbbbbabba=abb with [9] abbbcb=abbbbc:

Critical pair: abbbbbabbabbbbc=abbbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Overlap of [14] cabba=abbb with [3] abbbab=abbbba:

Critical pair: cabbabbbba=abbbbbbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [21], [22], [23], [24], [25], [29], [30], [31], [32], [33], [34], [42], [45].

Overlap of [14] cabba=abbb with [4] abbbbabbc=cb:

Critical pair: cabbcb=abbbbbbbabbc.

Reduce LHS:

Reduce RHS:

Referenced by [36].

Overlap of [14] cabba=abbb with [6] abbbbabba=ab:

Critical pair: cabbab=abbbbbbbabba.

Reduce LHS:

Reduce RHS:

Referenced by [23].

Overlap of [14] cabba=abbb with [9] abbbcb=abbbbc:

Critical pair: cabbabbbbc=abbbbbbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [26], [43], [45].

Overlap of [4] abbbbabbc=cb with [20] cab=cba:

Critical pair: abbbbabbcba=cbab.

Reduce LHS:

Referenced by [38].

Overlap of [14] cabba=abbb with [20] cab=cba:

Critical pair: cbaba=abbb.

Referenced by [39].

Overlap of [4] abbbbabbc=cb with [23] ccb=cbc:

Critical pair: abbbbabbcbc=cbcb.

Reduce LHS:

Referenced by [40].

Overlap of [1] abbbabbba=ab with [3] abbbab=abbbba:

Critical pair: abbbbabba=ab.

Reduce LHS:

Defines rule #1.

Referenced by [45], [49], [53].

Overlap of [4] abbbbabbc=cb with [10] abbbbab=abbbbba:

Critical pair: abbbbbabc=cb.

Reduce LHS:

Defines rule #5.

Referenced by [38], [40], [41], [49].

Overlap of [5] abbbbbabbc=cbb with [15] abbbbbab=ca:

Critical pair: cabc=cbb.

Reduce LHS:

Defines rule #9.

Referenced by [34], [41], [42], [43], [44], [46], [50].

Overlap of [13] abbbbbabba=abb with [15] abbbbbab=ca:

Critical pair: caba=abb.

Reduce LHS:

Defines rule #2.

Referenced by [32], [50].

Overlap of [8] abbbbabbbbb=abbbc with [10] abbbbab=abbbbba:

Critical pair: abbbbbabbbb=abbbc.

Reduce LHS:

Referenced by [35], [36], [47].

Overlap of [12] abbbbbabbabbbc=abbbbcb with [15] abbbbbab=ca:

Critical pair: cababbbc=abbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [45].

Simplify [16] cabcb=cabbc.

Reduce RHS:

Referenced by [34].

Overlap of [33] cabcb=cbabc with [20] cab=cba:

Critical pair: cbacb=cbabc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [18] cbabba=abbbb with [31] cbabb=abbbc:

Critical pair: abbbca=abbbb.

Defines rule #12.

Referenced by [45], [53].

Simplify [21] cbabcb=cbabbc.

Reduce RHS:

Referenced by [37].

Overlap of [36] cbabcb=abbbcc with [34] cbabc=cbbb:

Critical pair: cbbbb=abbbcc.

Defines rule #21.

Referenced by [44], [46], [52].

Overlap of [24] cacba=cbab with [28] cac=cb:

Critical pair: cbba=cbab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [39], [44], [45], [47].

Overlap of [25] cbaba=abbb with [38] cbab=cbba:

Critical pair: cbbaa=abbb.

Defines rule #6.

Referenced by [51].

Overlap of [26] cacbc=cbcb with [28] cac=cb:

Critical pair: cbbc=cbcb.

Flip LHS and RHS.

Defines rule #17.

Referenced by [46].

Overlap of [28] cac=cb with [29] cbac=cbb:

Critical pair: cacbb=cbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [51], [52].

Overlap of [29] cbac=cbb with [20] cab=cba:

Critical pair: cbacba=cbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [45], [47], [48].

Overlap of [29] cbac=cbb with [23] ccb=cbc:

Critical pair: cbacbc=cbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [29] cbac=cbb with [38] cbab=cbba:

Critical pair: cbacbba=cbbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [45].

Overlap of [38] cbab=cbba with [3] abbbab=abbbba:

Critical pair: cbabbbba=cbbabbab.

Reduce LHS:

Reduce RHS:

Defines rule #26.

Referenced by [49], [50], [51].

Overlap of [29] cbac=cbb with [40] cbcb=cbbc:

Critical pair: cbacbbc=cbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [31] cbabb=abbbc with [38] cbab=cbba:

Critical pair: cbbab=abbbc.

Reduce LHS:

Defines rule #13.

Referenced by [48].

Simplify [42] cbbab=cbbba.

Reduce RHS:

Defines rule #14.

Overlap of [27] caa=ab with [45] abbbbbca=c:

Critical pair: cac=abbbbbbca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [52].

Overlap of [30] cbaa=abb with [45] abbbbbca=c:

Critical pair: cbac=abbbbbbbca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [39] cbbaa=abbb with [45] abbbbbca=c:

Critical pair: cbbac=abbbbbbbbca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [41] cbbac=cbbb with [49] cca=cb:

Critical pair: cbbacb=cbbbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [27] caa=ab with [35] abbbca=abbbb:

Critical pair: caabbbb=abbbbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.