Certificate for #998 ⟨a, b | abbabba=ab⟩

Completion settings:

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

Axiom: abbabba=ab.

Referenced by [3], [4], [5], [7], [8], [19].

Axiom: abbbb=c.

Defines rule #18.

Referenced by [4], [5], [9], [11], [12], [13], [14], [29], [30], [34].

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

Critical pair: abbab=abbba.

Defines rule #19.

Referenced by [4], [5], [7], [8], [9], [10], [11], [15], [16], [19], [30].

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

Critical pair: abbabbc=abbbbb.

Reduce LHS:

Reduce RHS:

Referenced by [5], [6], [10], [12], [15], [20].

Overlap of [1] abbabba=ab with [4] abbbabc=cb:

Critical pair: abbabbcb=abbbbabc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [6], [12], [17], [28], [29], [31], [38], [42].

Overlap of [4] abbbabc=cb with [5] cabc=cbb:

Critical pair: abbbabcbb=cbabc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32], [39], [43].

Overlap of [1] abbabba=ab with [3] abbab=abbba:

Critical pair: abbbaba=ab.

Referenced by [11], [12], [13], [16].

Overlap of [1] abbabba=ab with [3] abbab=abbba:

Critical pair: abbabbba=abb.

Reduce LHS:

Referenced by [10], [21].

Overlap of [3] abbab=abbba with [2] abbbb=c:

Critical pair: abbc=abbbabbb.

Flip LHS and RHS.

Referenced by [22].

Overlap of [3] abbab=abbba with [4] abbbabc=cb:

Critical pair: abbcb=abbbabbabc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [7] abbbaba=ab with [3] abbab=abbba:

Critical pair: abbbababbba=abbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [12], [13], [19], [20], [21], [22].

Overlap of [7] abbbaba=ab with [4] abbbabc=cb:

Critical pair: abbbabcb=abbbbabc.

Reduce LHS:

Reduce RHS:

Referenced by [15], [18].

Overlap of [7] abbbaba=ab with [7] abbbaba=ab:

Critical pair: abbbabab=abbbbaba.

Reduce LHS:

Reduce RHS:

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

Overlap of [13] caab=caba with [2] abbbb=c:

Critical pair: cac=cababbb.

Flip LHS and RHS.

Referenced by [15], [16].

Overlap of [13] caab=caba with [4] abbbabc=cb:

Critical pair: cacb=cababbabc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [17], [18], [24].

Overlap of [13] caab=caba with [7] abbbaba=ab:

Critical pair: caab=cababbaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [5] cabc=cbb with [15] cacac=cbb:

Critical pair: cabcbb=cbbacac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [15] cacac=cbb with [15] cacac=cbb:

Critical pair: cacbb=cbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [27], [39], [43].

Overlap of [1] abbabba=ab with [3] abbab=abbba:

Critical pair: abbbaba=ab.

Reduce LHS:

Defines rule #5.

Referenced by [28].

Overlap of [4] abbbabc=cb with [11] abbbab=ca:

Critical pair: cac=cb.

Defines rule #3.

Referenced by [24], [26], [33], [35], [36], [40].

Overlap of [8] abbbabba=abb with [11] abbbab=ca:

Critical pair: caba=abb.

Referenced by [25], [28], [29].

Overlap of [9] abbbabbb=abbc with [11] abbbab=ca:

Critical pair: cabb=abbc.

Flip LHS and RHS.

Referenced by [23], [45].

Simplify [10] abbbc=abbcb.

Reduce RHS:

Referenced by [44].

Overlap of [15] cacac=cbb with [20] cac=cb:

Critical pair: cbac=cbb.

Defines rule #8.

Referenced by [31], [38], [42].

Simplify [16] cacaa=caba.

Reduce RHS:

Referenced by [26].

Overlap of [25] cacaa=abb with [20] cac=cb:

Critical pair: cbaa=abb.

Defines rule #10.

Referenced by [29], [30].

Overlap of [17] cbbacac=cbbbb with [18] cbbac=cbbb:

Critical pair: cbbbac=cbbbb.

Defines rule #24.

Overlap of [5] cabc=cbb with [19] caa=ab:

Critical pair: cabab=cbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [5] cabc=cbb with [26] cbaa=abb:

Critical pair: cababb=cbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Referenced by [35].

Overlap of [26] cbaa=abb with [3] abbab=abbba:

Critical pair: cbaabbba=abbbbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [31], [32], [33], [34], [37], [38], [41], [42], [44], [45].

Overlap of [5] cabc=cbb with [30] cab=cba:

Critical pair: cabcba=cbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [34], [44].

Overlap of [6] cbabc=cbbb with [30] cab=cba:

Critical pair: cbabcba=cbbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34], [46].

Overlap of [20] cac=cb with [30] cab=cba:

Critical pair: cacba=cbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [34], [39], [43], [44], [45].

Overlap of [30] cab=cba with [2] abbbb=c:

Critical pair: cc=cbabbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [35], [43], [46].

Overlap of [20] cac=cb with [29] cbbbaa=c:

Critical pair: cac=cbbbbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [36], [37].

Overlap of [35] cca=cb with [20] cac=cb:

Critical pair: ccb=cbc.

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [35] cca=cb with [30] cab=cba:

Critical pair: ccba=cbb.

Defines rule #6.

Referenced by [41], [42], [43].

Overlap of [5] cabc=cbb with [36] cbc=ccb:

Critical pair: cabccb=cbbbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [39], [43], [47].

Overlap of [6] cbabc=cbbb with [36] cbc=ccb:

Critical pair: cbabccb=cbbbbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [48].

Overlap of [20] cac=cb with [36] cbc=ccb:

Critical pair: caccb=cbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [42], [43], [47], [48].

Overlap of [36] cbc=ccb with [30] cab=cba:

Critical pair: cbcba=ccbab.

Reduce LHS:

Reduce RHS:

Defines rule #12.

Overlap of [5] cabc=cbb with [37] ccba=cbb:

Critical pair: cabcbb=cbbcba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [6] cbabc=cbbb with [37] ccba=cbb:

Critical pair: cbabcbb=cbbbcba.

Reduce LHS:

Reduce RHS:

Defines rule #22.

Simplify [23] abbbc=cabbb.

Reduce RHS:

Defines rule #17.

Simplify [22] abbc=cabb.

Reduce RHS:

Defines rule #11.

Simplify [32] cbbbab=cbbbba.

Reduce RHS:

Defines rule #25.

Simplify [38] cbbbc=cbbcb.

Reduce RHS:

Defines rule #13.

Simplify [39] cbbbbc=cbbcbb.

Reduce RHS:

Defines rule #21.