Certificate for #4215 ⟨a, b | aabbbbbaa=ab⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with b < a < c
• Auxiliary generators:
  1. abbbb=c

Axiom: aabbbbbaa=ab.

Referenced by [3].

Axiom: abbbb=c.

Defines rule #1.

Referenced by [3], [4], [11], [15], [16], [30], [31], [46].

Overlap of [1] aabbbbbaa=ab with [2] abbbb=c:

Critical pair: acbaa=ab.

Defines rule #2.

Referenced by [4], [5], [6], [7], [9], [13], [15].

Overlap of [3] acbaa=ab with [2] abbbb=c:

Critical pair: acbac=abbbbb.

Reduce RHS:

Defines rule #3.

Referenced by [6], [7], [8], [10], [14], [15], [17].

Overlap of [3] acbaa=ab with [3] acbaa=ab:

Critical pair: acbaab=abcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [9], [10], [11], [12], [16], [24], [25].

Overlap of [3] acbaa=ab with [4] acbac=cb:

Critical pair: acbacb=abcbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [10], [12], [13], [14], [16], [18], [20], [21], [23], [24], [25], [58].

Overlap of [4] acbac=cb with [3] acbaa=ab:

Critical pair: acbab=cbbaa.

Flip LHS and RHS.

Defines rule #4.

Referenced by [24], [26], [32].

Overlap of [4] acbac=cb with [4] acbac=cb:

Critical pair: acbcb=cbbac.

Flip LHS and RHS.

Defines rule #5.

Referenced by [25], [27], [33].

Overlap of [3] acbaa=ab with [5] abcbaa=abb:

Critical pair: acbaabb=abbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [26], [27], [30], [31].

Overlap of [5] abcbaa=abb with [4] acbac=cb:

Critical pair: abcbacb=abbcbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [26], [27], [28], [29], [30], [31], [36], [39], [59].

Overlap of [5] abcbaa=abb with [5] abcbaa=abb:

Critical pair: abcbaabb=abbbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [15], [16], [17], [18], [19], [22].

Overlap of [5] abcbaa=abb with [6] abcbac=cbb:

Critical pair: abcbacbb=abbbcbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Referenced by [17], [18], [19], [37], [40], [60].

Overlap of [6] abcbac=cbb with [3] acbaa=ab:

Critical pair: abcbab=cbbbaa.

Flip LHS and RHS.

Defines rule #10.

Referenced by [30], [34].

Overlap of [6] abcbac=cbb with [4] acbac=cb:

Critical pair: abcbcb=cbbbac.

Flip LHS and RHS.

Defines rule #11.

Referenced by [31], [35].

Overlap of [3] acbaa=ab with [11] abbbcbaa=c:

Critical pair: acbac=abbbbcbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [20], [21], [22], [32], [33], [34], [35].

Overlap of [5] abcbaa=abb with [11] abbbcbaa=c:

Critical pair: abcbac=abbbbbcbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [23], [28], [51].

Overlap of [11] abbbcbaa=c with [4] acbac=cb:

Critical pair: abbbcbacb=ccbac.

Reduce LHS:

Defines rule #9.

Referenced by [18], [26], [27], [29], [30], [31], [37], [40], [44], [48], [52], [60], [61], [62].

Overlap of [11] abbbcbaa=c with [6] abcbac=cbb:

Critical pair: abbbcbacbb=cbcbac.

Reduce LHS:

Defines rule #13.

Referenced by [21], [30], [31], [32], [33], [34], [35], [38], [41], [44], [45], [48], [49].

Overlap of [11] abbbcbaa=c with [11] abbbcbaa=c:

Critical pair: abbbcbac=cbbbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Referenced by [44], [48].

Overlap of [6] abcbac=cbb with [15] ccbaa=cb:

Critical pair: abcbacb=cbbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [29].

Overlap of [15] ccbaa=cb with [6] abcbac=cbb:

Critical pair: ccbacbb=cbbcbac.

Reduce LHS:

Defines rule #19.

Referenced by [23], [28], [32], [33], [34], [35], [42], [43], [44], [45], [48], [49], [53].

Overlap of [15] ccbaa=cb with [11] abbbcbaa=c:

Critical pair: ccbac=cbbbbcbaa.

Flip LHS and RHS.

Defines rule #28.

Referenced by [45], [49].

Overlap of [16] cbcbaa=cbb with [6] abcbac=cbb:

Critical pair: cbcbacbb=cbbbcbac.

Reduce LHS:

Defines rule #25.

Referenced by [28], [29], [34], [35], [45], [49].

Overlap of [6] abcbac=cbb with [7] cbbaa=acbab:

Critical pair: abcbaacbab=cbbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [6] abcbac=cbb with [8] cbbac=acbcb:

Critical pair: abcbaacbcb=cbbbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [10] abbcbac=cbbb with [7] cbbaa=acbab:

Critical pair: abbcbaacbab=cbbbbbaa.

Reduce LHS:

Reduce RHS:

Defines rule #20.

Referenced by [44], [45], [46], [47], [50], [61], [63], [64], [65].

Overlap of [10] abbcbac=cbbb with [8] cbbac=acbcb:

Critical pair: abbcbaacbcb=cbbbbbac.

Reduce LHS:

Reduce RHS:

Defines rule #23.

Referenced by [48], [49], [50], [51], [52], [53], [54], [55], [56], [57], [62].

Overlap of [16] cbcbaa=cbb with [10] abbcbac=cbbb:

Critical pair: cbcbacbbb=cbbbbcbac.

Reduce LHS:

Defines rule #29.

Referenced by [29].

Overlap of [20] cbbcbaa=cbbb with [10] abbcbac=cbbb:

Critical pair: cbbcbacbbb=cbbbbbcbac.

Reduce LHS:

Reduce RHS:

Defines rule #33.

Overlap of [10] abbcbac=cbbb with [13] cbbbaa=abcbab:

Critical pair: abbcbaabcbab=cbbbbbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #26.

Referenced by [36], [37], [38], [42], [54], [55].

Overlap of [10] abbcbac=cbbb with [14] cbbbac=abcbcb:

Critical pair: abbcbaabcbcb=cbbbbbbac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [39], [40], [41], [43], [56], [57].

Overlap of [18] ccbacb=cbcbac with [7] cbbaa=acbab:

Critical pair: ccbaacbab=cbcbacbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #30.

Overlap of [18] ccbacb=cbcbac with [8] cbbac=acbcb:

Critical pair: ccbaacbcb=cbcbacbac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #31.

Overlap of [18] ccbacb=cbcbac with [13] cbbbaa=abcbab:

Critical pair: ccbaabcbab=cbcbacbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #34.

Overlap of [18] ccbacb=cbcbac with [14] cbbbac=abcbcb:

Critical pair: ccbaabcbcb=cbcbacbbac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #35.

Overlap of [10] abbcbac=cbbb with [30] cbcbacaa=ccbab:

Critical pair: abbcbaccbab=cbbbbcbacaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #38.

Overlap of [12] abbbcbac=cbbbb with [30] cbcbacaa=ccbab:

Critical pair: abbbcbaccbab=cbbbbbcbacaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #43.

Overlap of [18] ccbacb=cbcbac with [30] cbcbacaa=ccbab:

Critical pair: ccbaccbab=cbcbaccbacaa.

Flip LHS and RHS.

Defines rule #46.

Overlap of [10] abbcbac=cbbb with [31] cbcbacac=ccbcb:

Critical pair: abbcbaccbcb=cbbbbcbacac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #39.

Overlap of [12] abbbcbac=cbbbb with [31] cbcbacac=ccbcb:

Critical pair: abbbcbaccbcb=cbbbbbcbacac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #44.

Overlap of [18] ccbacb=cbcbac with [31] cbcbacac=ccbcb:

Critical pair: ccbaccbcb=cbcbaccbacac.

Flip LHS and RHS.

Defines rule #47.

Overlap of [21] cbcbacb=cbbcbac with [30] cbcbacaa=ccbab:

Critical pair: cbcbaccbab=cbbcbaccbacaa.

Flip LHS and RHS.

Defines rule #49.

Overlap of [21] cbcbacb=cbbcbac with [31] cbcbacac=ccbcb:

Critical pair: cbcbaccbcb=cbbcbaccbacac.

Flip LHS and RHS.

Defines rule #50.

Overlap of [19] cbbbcbaa=cbbbb with [26] abbbcbab=ccbacaa:

Critical pair: cbbbcbaccbacaa=cbbbbbbbcbab.

Reduce RHS:

Defines rule #56.

Overlap of [22] cbbbbcbaa=ccbac with [26] abbbcbab=ccbacaa:

Critical pair: cbbbbcbaccbacaa=ccbacbbbcbab.

Reduce RHS:

Defines rule #58.

Overlap of [26] abbbcbab=ccbacaa with [2] abbbb=c:

Critical pair: abbbcbc=ccbacaabbb.

Flip LHS and RHS.

Defines rule #36.

Overlap of [26] abbbcbab=ccbacaa with [26] abbbcbab=ccbacaa:

Critical pair: abbbcbccbacaa=ccbacaabbcbab.

Flip LHS and RHS.

Defines rule #51.

Overlap of [19] cbbbcbaa=cbbbb with [27] abbbcbcb=ccbacac:

Critical pair: cbbbcbaccbacac=cbbbbbbbcbcb.

Reduce RHS:

Defines rule #57.

Overlap of [22] cbbbbcbaa=ccbac with [27] abbbcbcb=ccbacac:

Critical pair: cbbbbcbaccbacac=ccbacbbbcbcb.

Reduce RHS:

Defines rule #59.

Overlap of [26] abbbcbab=ccbacaa with [27] abbbcbcb=ccbacac:

Critical pair: abbbcbccbacac=ccbacaabbcbcb.

Flip LHS and RHS.

Defines rule #52.

Overlap of [27] abbbcbcb=ccbacac with [16] cbcbaa=cbb:

Critical pair: abbbcbb=ccbacacaa.

Flip LHS and RHS.

Defines rule #32.

Referenced by [58], [59], [60], [61], [62].

Overlap of [27] abbbcbcb=ccbacac with [17] cbbbbb=ccbac:

Critical pair: abbbcbccbac=ccbacacbbbb.

Flip LHS and RHS.

Defines rule #40.

Overlap of [27] abbbcbcb=ccbacac with [21] cbcbacb=cbbcbac:

Critical pair: abbbcbbcbac=ccbacacacb.

Defines rule #37.

Referenced by [63].

Overlap of [27] abbbcbcb=ccbacac with [30] cbcbacaa=ccbab:

Critical pair: abbbccbab=ccbacacacaa.

Flip LHS and RHS.

Defines rule #41.

Overlap of [27] abbbcbcb=ccbacac with [30] cbcbacaa=ccbab:

Critical pair: abbbcbccbab=ccbacaccbacaa.

Flip LHS and RHS.

Defines rule #54.

Overlap of [27] abbbcbcb=ccbacac with [31] cbcbacac=ccbcb:

Critical pair: abbbccbcb=ccbacacacac.

Flip LHS and RHS.

Defines rule #42.

Overlap of [27] abbbcbcb=ccbacac with [31] cbcbacac=ccbcb:

Critical pair: abbbcbccbcb=ccbacaccbacac.

Flip LHS and RHS.

Defines rule #55.

Overlap of [51] ccbacacaa=abbbcbb with [6] abcbac=cbb:

Critical pair: ccbacacacbb=abbbcbbbcbac.

Flip LHS and RHS.

Defines rule #45.

Referenced by [64].

Overlap of [51] ccbacacaa=abbbcbb with [10] abbcbac=cbbb:

Critical pair: ccbacacacbbb=abbbcbbbbcbac.

Flip LHS and RHS.

Defines rule #48.

Referenced by [65].

Overlap of [51] ccbacacaa=abbbcbb with [12] abbbcbac=cbbbb:

Critical pair: ccbacacacbbbb=abbbcbbbbbcbac.

Reduce RHS:

Defines rule #53.

Overlap of [51] ccbacacaa=abbbcbb with [26] abbbcbab=ccbacaa:

Critical pair: ccbacacaccbacaa=abbbcbbbbbcbab.

Reduce RHS:

Defines rule #60.

Overlap of [51] ccbacacaa=abbbcbb with [27] abbbcbcb=ccbacac:

Critical pair: ccbacacaccbacac=abbbcbbbbbcbcb.

Reduce RHS:

Defines rule #61.

Overlap of [26] abbbcbab=ccbacaa with [53] abbbcbbcbac=ccbacacacb:

Critical pair: abbbcbccbacacacb=ccbacaabbcbbcbac.

Flip LHS and RHS.

Defines rule #62.

Overlap of [26] abbbcbab=ccbacaa with [58] abbbcbbbcbac=ccbacacacbb:

Critical pair: abbbcbccbacacacbb=ccbacaabbcbbbcbac.

Flip LHS and RHS.

Defines rule #63.

Overlap of [26] abbbcbab=ccbacaa with [59] abbbcbbbbcbac=ccbacacacbbb:

Critical pair: abbbcbccbacacacbbb=ccbacaabbcbbbbcbac.

Flip LHS and RHS.

Defines rule #64.