Certificate for #2009 ⟨a, b | aabbbbaa=ab⟩

Completion settings:

• Auxiliary generators:
  1. c = abbb
• Reduction order:
  • Right-to-left shortlex with a < c < b

Axiom: aabbbbaa=ab.

Referenced by [3].

Axiom: abbb=c.

Defines rule #1.

Referenced by [3], [4], [9], [11], [13], [22].

Overlap of [1] aabbbbaa=ab with [2] abbb=c:

Critical pair: acbaa=ab.

Defines rule #2.

Referenced by [4], [5], [6], [7], [9], [18], [32], [38], [60].

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

Critical pair: acbac=abbbb.

Reduce RHS:

Defines rule #4.

Referenced by [6], [7], [8], [10], [12], [14], [17], [19], [32], [34], [38], [47], [61], [74].

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

Critical pair: acbaab=abcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [9], [10], [11], [15], [21], [26], [33], [39].

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

Critical pair: acbacb=abcbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [10], [18], [19], [20], [21], [26], [33], [35], [39].

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

Critical pair: acbab=cbbaa.

Defines rule #5.

Referenced by [21], [22], [23], [24], [25], [36], [40], [52], [67].

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

Critical pair: acbcb=cbbac.

Defines rule #6.

Referenced by [26], [27], [28], [29], [30], [31], [37], [41], [43], [44], [48], [49], [53], [62], [68], [69], [75].

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

Critical pair: acbaabb=abbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

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

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

Critical pair: abcbacb=abbcbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

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

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

Critical pair: abcbaabb=abbbcbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [12], [13], [14], [15], [16], [24], [29].

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

Critical pair: acbacb=cbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [17], [20], [25], [27], [30].

Overlap of [11] ccbaa=cb with [2] abbb=c:

Critical pair: ccbac=cbbbb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [21], [23], [26], [28], [31], [33], [35], [39], [42], [54].

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

Critical pair: ccbacb=cbcbac.

Defines rule #12.

Referenced by [23], [24], [28], [29], [40], [41].

Overlap of [11] ccbaa=cb with [5] abcbaa=abb:

Critical pair: ccbaabb=cbbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

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

Overlap of [11] ccbaa=cb with [9] abbcbaa=c:

Critical pair: ccbac=cbbbcbaa.

Flip LHS and RHS.

Defines rule #24.

Overlap of [12] cbcbaa=cbb with [4] acbac=cb:

Critical pair: cbcbacb=cbbcbac.

Defines rule #19.

Referenced by [20], [24], [25], [29], [30], [52], [53], [55].

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

Critical pair: abcbab=cbbbaa.

Defines rule #11.

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

Critical pair: abcbcb=cbbbac.

Defines rule #13.

Referenced by [42], [45], [46], [50], [51], [63], [64], [70], [71].

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

Critical pair: cbcbacbb=cbbbcbac.

Reduce LHS:

Defines rule #28.

Referenced by [25], [30], [35], [36], [37], [67], [68].

Overlap of [5] abcbaa=abb with [7] acbab=cbbaa:

Critical pair: abcbacbbaa=abbcbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [7] acbab=cbbaa with [2] abbb=c:

Critical pair: acbc=cbbaabb.

Flip LHS and RHS.

Defines rule #21.

Referenced by [38], [39].

Overlap of [9] abbcbaa=c with [7] acbab=cbbaa:

Critical pair: abbcbacbbaa=ccbab.

Reduce LHS:

Defines rule #22.

Referenced by [43], [44], [45], [46], [56], [57].

Overlap of [11] ccbaa=cb with [7] acbab=cbbaa:

Critical pair: ccbacbbaa=cbcbab.

Reduce LHS:

Defines rule #34.

Overlap of [12] cbcbaa=cbb with [7] acbab=cbbaa:

Critical pair: cbcbacbbaa=cbbcbab.

Reduce LHS:

Defines rule #46.

Overlap of [5] abcbaa=abb with [8] acbcb=cbbac:

Critical pair: abcbacbbac=abbcbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [54], [55], [56], [57], [58], [59], [65], [66], [72], [73], [74].

Overlap of [8] acbcb=cbbac with [12] cbcbaa=cbb:

Critical pair: acbb=cbbacaa.

Flip LHS and RHS.

Defines rule #14.

Referenced by [32], [33], [34].

Overlap of [9] abbcbaa=c with [8] acbcb=cbbac:

Critical pair: abbcbacbbac=ccbcb.

Reduce LHS:

Defines rule #25.

Referenced by [48], [49], [50], [51], [58], [59].

Overlap of [11] ccbaa=cb with [8] acbcb=cbbac:

Critical pair: ccbacbbac=cbcbcb.

Reduce LHS:

Defines rule #36.

Overlap of [12] cbcbaa=cbb with [8] acbcb=cbbac:

Critical pair: cbcbacbbac=cbbcbcb.

Reduce LHS:

Defines rule #48.

Overlap of [8] acbcb=cbbac with [13] cbbbb=ccbac:

Critical pair: acbccbac=cbbacbbb.

Flip LHS and RHS.

Defines rule #31.

Overlap of [4] acbac=cb with [27] cbbacaa=acbb:

Critical pair: acbaacbb=cbbbacaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [47].

Overlap of [6] abcbac=cbb with [27] cbbacaa=acbb:

Critical pair: abcbaacbb=cbbbbacaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #32.

Overlap of [27] cbbacaa=acbb with [4] acbac=cb:

Critical pair: cbbacacb=acbbcbac.

Defines rule #27.

Overlap of [15] cbbcbaa=cbbb with [6] abcbac=cbb:

Critical pair: cbbcbacbb=cbbbbcbac.

Reduce LHS:

Reduce RHS:

Defines rule #40.

Referenced by [36], [37], [75].

Overlap of [15] cbbcbaa=cbbb with [7] acbab=cbbaa:

Critical pair: cbbcbacbbaa=cbbbcbab.

Reduce LHS:

Defines rule #56.

Overlap of [15] cbbcbaa=cbbb with [8] acbcb=cbbac:

Critical pair: cbbcbacbbac=cbbbcbcb.

Reduce LHS:

Defines rule #59.

Overlap of [4] acbac=cb with [22] cbbaabb=acbc:

Critical pair: acbaacbc=cbbbaabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #30.

Overlap of [6] abcbac=cbb with [22] cbbaabb=acbc:

Critical pair: abcbaacbc=cbbbbaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #43.

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

Critical pair: ccbcbbaa=cbcbacab.

Flip LHS and RHS.

Defines rule #26.

Referenced by [62], [63], [64], [65], [66].

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

Critical pair: ccbcbbac=cbcbaccb.

Flip LHS and RHS.

Defines rule #29.

Referenced by [69], [70], [71], [72], [73].

Overlap of [19] abcbcb=cbbbac with [13] cbbbb=ccbac:

Critical pair: abcbccbac=cbbbacbbb.

Flip LHS and RHS.

Defines rule #44.

Overlap of [8] acbcb=cbbac with [23] cbcbacaa=ccbab:

Critical pair: accbab=cbbacacaa.

Flip LHS and RHS.

Defines rule #33.

Overlap of [8] acbcb=cbbac with [23] cbcbacaa=ccbab:

Critical pair: acbccbab=cbbaccbacaa.

Flip LHS and RHS.

Defines rule #57.

Overlap of [19] abcbcb=cbbbac with [23] cbcbacaa=ccbab:

Critical pair: abccbab=cbbbacacaa.

Flip LHS and RHS.

Defines rule #45.

Overlap of [19] abcbcb=cbbbac with [23] cbcbacaa=ccbab:

Critical pair: abcbccbab=cbbbaccbacaa.

Flip LHS and RHS.

Defines rule #67.

Overlap of [32] cbbbacaa=abcbb with [4] acbac=cb:

Critical pair: cbbbacacb=abcbbcbac.

Defines rule #39.

Overlap of [8] acbcb=cbbac with [28] cbcbacac=ccbcb:

Critical pair: accbcb=cbbacacac.

Flip LHS and RHS.

Defines rule #35.

Referenced by [60], [61].

Overlap of [8] acbcb=cbbac with [28] cbcbacac=ccbcb:

Critical pair: acbccbcb=cbbaccbacac.

Flip LHS and RHS.

Defines rule #60.

Overlap of [19] abcbcb=cbbbac with [28] cbcbacac=ccbcb:

Critical pair: abccbcb=cbbbacacac.

Flip LHS and RHS.

Defines rule #47.

Overlap of [19] abcbcb=cbbbac with [28] cbcbacac=ccbcb:

Critical pair: abcbccbcb=cbbbaccbacac.

Flip LHS and RHS.

Defines rule #68.

Overlap of [17] cbcbacb=cbbcbac with [7] acbab=cbbaa:

Critical pair: cbcbcbbaa=cbbcbacab.

Flip LHS and RHS.

Defines rule #38.

Overlap of [17] cbcbacb=cbbcbac with [8] acbcb=cbbac:

Critical pair: cbcbcbbac=cbbcbaccb.

Flip LHS and RHS.

Defines rule #42.

Overlap of [26] abbcbcb=ccbacac with [13] cbbbb=ccbac:

Critical pair: abbcbccbac=ccbacacbbb.

Flip LHS and RHS.

Defines rule #54.

Overlap of [26] abbcbcb=ccbacac with [17] cbcbacb=cbbcbac:

Critical pair: abbcbbcbac=ccbacacacb.

Flip LHS and RHS.

Defines rule #51.

Overlap of [26] abbcbcb=ccbacac with [23] cbcbacaa=ccbab:

Critical pair: abbccbab=ccbacacacaa.

Flip LHS and RHS.

Defines rule #55.

Overlap of [26] abbcbcb=ccbacac with [23] cbcbacaa=ccbab:

Critical pair: abbcbccbab=ccbacaccbacaa.

Flip LHS and RHS.

Defines rule #71.

Overlap of [26] abbcbcb=ccbacac with [28] cbcbacac=ccbcb:

Critical pair: abbccbcb=ccbacacacac.

Flip LHS and RHS.

Defines rule #58.

Overlap of [26] abbcbcb=ccbacac with [28] cbcbacac=ccbcb:

Critical pair: abbcbccbcb=ccbacaccbacac.

Flip LHS and RHS.

Defines rule #72.

Overlap of [48] cbbacacac=accbcb with [3] acbaa=ab:

Critical pair: cbbacacab=accbcbbaa.

Defines rule #37.

Referenced by [74].

Overlap of [48] cbbacacac=accbcb with [4] acbac=cb:

Critical pair: cbbacaccb=accbcbbac.

Defines rule #41.

Overlap of [8] acbcb=cbbac with [40] cbcbacab=ccbcbbaa:

Critical pair: acbccbcbbaa=cbbaccbacab.

Flip LHS and RHS.

Defines rule #63.

Overlap of [19] abcbcb=cbbbac with [40] cbcbacab=ccbcbbaa:

Critical pair: abccbcbbaa=cbbbacacab.

Flip LHS and RHS.

Defines rule #49.

Overlap of [19] abcbcb=cbbbac with [40] cbcbacab=ccbcbbaa:

Critical pair: abcbccbcbbaa=cbbbaccbacab.

Flip LHS and RHS.

Defines rule #69.

Overlap of [26] abbcbcb=ccbacac with [40] cbcbacab=ccbcbbaa:

Critical pair: abbccbcbbaa=ccbacacacab.

Flip LHS and RHS.

Defines rule #61.

Overlap of [26] abbcbcb=ccbacac with [40] cbcbacab=ccbcbbaa:

Critical pair: abbcbccbcbbaa=ccbacaccbacab.

Flip LHS and RHS.

Defines rule #73.

Overlap of [20] cbbcbacb=cbbbcbac with [7] acbab=cbbaa:

Critical pair: cbbcbcbbaa=cbbbcbacab.

Flip LHS and RHS.

Defines rule #50.

Overlap of [20] cbbcbacb=cbbbcbac with [8] acbcb=cbbac:

Critical pair: cbbcbcbbac=cbbbcbaccb.

Flip LHS and RHS.

Defines rule #53.

Overlap of [8] acbcb=cbbac with [41] cbcbaccb=ccbcbbac:

Critical pair: acbccbcbbac=cbbaccbaccb.

Flip LHS and RHS.

Defines rule #66.

Overlap of [19] abcbcb=cbbbac with [41] cbcbaccb=ccbcbbac:

Critical pair: abccbcbbac=cbbbacaccb.

Flip LHS and RHS.

Defines rule #52.

Overlap of [19] abcbcb=cbbbac with [41] cbcbaccb=ccbcbbac:

Critical pair: abcbccbcbbac=cbbbaccbaccb.

Flip LHS and RHS.

Defines rule #70.

Overlap of [26] abbcbcb=ccbacac with [41] cbcbaccb=ccbcbbac:

Critical pair: abbccbcbbac=ccbacacaccb.

Flip LHS and RHS.

Defines rule #64.

Overlap of [26] abbcbcb=ccbacac with [41] cbcbaccb=ccbcbbac:

Critical pair: abbcbccbcbbac=ccbacaccbaccb.

Flip LHS and RHS.

Defines rule #74.

Overlap of [26] abbcbcb=ccbacac with [60] cbbacacab=accbcbbaa:

Critical pair: abbcbaccbcbbaa=ccbacacbacacab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #62.

Overlap of [35] cbbbcbacb=ccbaccbac with [8] acbcb=cbbac:

Critical pair: cbbbcbcbbac=ccbaccbaccb.

Flip LHS and RHS.

Defines rule #65.