Certificate for #3078 ⟨a, b | aababbaabba=1⟩

Completion settings:

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

Axiom: aababbaabba=1.

Referenced by [4].

Axiom: bb=c.

Defines rule #5.

Referenced by [3], [4], [5], [24], [27], [34], [41], [49], [52], [54], [65], [72], [74], [75].

Axiom: aabbaaaba=d.

Reduce LHS:

Referenced by [7], [8], [9], [10], [11], [14], [16].

Overlap of [1] aababbaabba=1 with [2] bb=c:

Critical pair: aabacaabba=1.

Reduce LHS:

Referenced by [6], [7], [8], [9], [10], [12], [13], [15], [17].

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

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [53], [58], [59], [70], [73].

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

Critical pair: aabacaac=abacaaca.

Referenced by [10], [12], [13], [17], [29].

Overlap of [3] aacaaaba=d with [4] aabacaaca=1:

Critical pair: aaca=dcaaca.

Flip LHS and RHS.

Referenced by [11], [28].

Overlap of [3] aacaaaba=d with [4] aabacaaca=1:

Critical pair: aacaaab=dabacaaca.

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

Overlap of [4] aabacaaca=1 with [3] aacaaaba=d:

Critical pair: aabacd=aaba.

Referenced by [12], [13].

Overlap of [4] aabacaaca=1 with [3] aacaaaba=d:

Critical pair: aabacaacd=acaaaba.

Reduce LHS:

Referenced by [30].

Overlap of [7] dcaaca=aaca with [3] aacaaaba=d:

Critical pair: dcd=aacaaaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [14], [15], [18].

Overlap of [4] aabacaaca=1 with [9] aabacd=aaba:

Critical pair: aabacaacaaba=abacd.

Reduce LHS:

Referenced by [13].

Overlap of [4] aabacaaca=1 with [12] abacdcd=abacd:

Critical pair: aabacaacabacd=bacdcd.

Reduce LHS:

Referenced by [19].

Overlap of [11] dabacaacaa=dcd with [3] aacaaaba=d:

Critical pair: dabacaacd=dcdcaaaba.

Referenced by [21].

Overlap of [11] dabacaacaa=dcd with [4] aabacaaca=1:

Critical pair: dabacaac=dcdbacaaca.

Referenced by [16], [18], [22], [23].

Overlap of [3] aacaaaba=d with [8] aacaaab=dabacaaca:

Critical pair: dabacaacaa=d.

Reduce LHS:

Referenced by [18], [26].

Overlap of [4] aabacaaca=1 with [6] aabacaac=abacaaca:

Critical pair: abacaacaa=1.

Referenced by [20], [25], [29], [31].

Overlap of [11] dabacaacaa=dcd with [15] dabacaac=dcdbacaaca:

Critical pair: dcdbacaacaaa=dcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19], [21], [22], [23], [26].

Simplify [13] abacaacaaba=bacdcd.

Reduce RHS:

Referenced by [20].

Overlap of [19] abacaacaaba=bacd with [17] abacaacaa=1:

Critical pair: ba=bacd.

Flip LHS and RHS.

Referenced by [24], [27].

Simplify [14] dabacaacd=dcdcaaaba.

Reduce RHS:

Referenced by [22].

Overlap of [21] dabacaacd=dcaaaba with [15] dabacaac=dcdbacaaca:

Critical pair: dcdbacaacad=dcaaaba.

Reduce LHS:

Referenced by [44].

Simplify [15] dabacaac=dcdbacaaca.

Reduce RHS:

Referenced by [43].

Overlap of [2] bb=c with [20] bacd=ba:

Critical pair: bba=cacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [17] abacaacaa=1 with [17] abacaacaa=1:

Critical pair: abacaaca=bacaacaa.

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

Simplify [16] dcdbacaacaaa=d.

Reduce LHS:

Referenced by [27], [40].

Overlap of [20] bacd=ba with [26] dbacaacaaa=d:

Critical pair: bacd=babacaacaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [28], [37].

Overlap of [7] dcaaca=aaca with [27] cacaacaaaa=ba:

Critical pair: dcaaba=aacacaacaaaa.

Reduce RHS:

Referenced by [29].

Overlap of [28] dcaaba=aaba with [17] abacaacaa=1:

Critical pair: dca=aabacaacaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [10] abacaacad=acaaaba with [25] abacaaca=bacaacaa:

Critical pair: bacaacaad=acaaaba.

Referenced by [38], [60].

Overlap of [17] abacaacaa=1 with [25] abacaaca=bacaacaa:

Critical pair: bacaacaaa=1.

Referenced by [32], [34], [35], [37], [38].

Overlap of [29] bacaacaaaa=dca with [31] bacaacaaa=1:

Critical pair: a=dca.

Flip LHS and RHS.

Referenced by [33], [36].

Overlap of [32] dca=a with [24] cacd=ca:

Critical pair: dca=acd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [2] bb=c with [31] bacaacaaa=1:

Critical pair: b=cacaacaaa.

Flip LHS and RHS.

Referenced by [36], [37].

Overlap of [31] bacaacaaa=1 with [33] acd=a:

Critical pair: bacaacaaa=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [49], [52], [53], [54], [56], [60], [61], [72], [73], [74].

Overlap of [32] dca=a with [34] cacaacaaa=b:

Critical pair: db=acaacaaa.

Flip LHS and RHS.

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

Overlap of [27] cacaacaaaa=ba with [36] acaacaaa=db:

Critical pair: cacaacaaadb=bacaacaaa.

Reduce LHS:

Reduce RHS:

Referenced by [40], [41].

Overlap of [31] bacaacaaa=1 with [36] acaacaaa=db:

Critical pair: bacaacaadb=caacaaa.

Reduce LHS:

Referenced by [42], [61].

Overlap of [36] acaacaaa=db with [36] acaacaaa=db:

Critical pair: acaacaadb=dbcaacaaa.

Referenced by [47].

Overlap of [37] bdb=1 with [26] dbacaacaaa=d:

Critical pair: bd=acaacaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [41], [42], [43], [45], [46], [47], [48], [52], [54], [68], [69], [76].

Overlap of [40] db=bd with [2] bb=c:

Critical pair: dc=bdb.

Reduce RHS:

Defines rule #1.

Referenced by [42], [44], [47], [50], [52], [55], [66], [68], [71], [76].

Overlap of [36] acaacaaa=db with [38] acaaabab=caacaaa:

Critical pair: acaacaacaacaaa=dbcaaabab.

Reduce LHS:

Reduce RHS:

Referenced by [62].

Simplify [23] dabacaac=dbacaaca.

Reduce RHS:

Referenced by [52], [53].

Simplify [22] dbacaacad=dcaaaba.

Reduce RHS:

Referenced by [45].

Overlap of [44] dbacaacad=aaaba with [40] db=bd:

Critical pair: bdacaacad=aaaba.

Referenced by [49], [50].

Simplify [36] acaacaaa=db.

Reduce RHS:

Defines rule #16.

Referenced by [51], [52], [73].

Simplify [39] acaacaadb=dbcaacaaa.

Reduce RHS:

Referenced by [48].

Overlap of [47] acaacaadb=baacaaa with [40] db=bd:

Critical pair: acaacaabd=baacaaa.

Referenced by [51], [66].

Overlap of [2] bb=c with [45] bdacaacad=aaaba:

Critical pair: baaaba=cdacaacad.

Reduce RHS:

Flip LHS and RHS.

Referenced by [63].

Overlap of [45] bdacaacad=aaaba with [41] dc=1:

Critical pair: bdacaaca=aaabac.

Flip LHS and RHS.

Referenced by [51].

Overlap of [46] acaacaaa=bd with [50] aaabac=bdacaaca:

Critical pair: acaacaabdacaaca=bdaabac.

Reduce LHS:

Referenced by [69].

Overlap of [43] dabacaac=bdacaaca with [46] acaacaaa=bd:

Critical pair: dabacabd=bdacaacaaacaaa.

Reduce RHS:

Referenced by [54], [55].

Overlap of [35] cd=1 with [43] dabacaac=bdacaaca:

Critical pair: cbdacaaca=abacaac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [58], [59].

Overlap of [52] dabacabd=aaa with [40] db=bd:

Critical pair: dabacabbd=aaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [60], [61], [62], [63], [74].

Overlap of [52] dabacabd=aaa with [41] dc=1:

Critical pair: dabacab=aaac.

Referenced by [56], [57], [59].

Overlap of [35] cd=1 with [55] dabacab=aaac:

Critical pair: caaac=abacab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [57], [64], [74].

Overlap of [55] dabacab=aaac with [56] abacab=caaac:

Critical pair: dabaccaaac=aaacacab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [53] abacaac=bacaaca with [5] cb=bc:

Critical pair: abacaabc=bacaacab.

Defines rule #10.

Overlap of [55] dabacab=aaac with [53] abacaac=bacaaca:

Critical pair: dabacbacaaca=aaacacaac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [70], [74].

Simplify [30] bacaacaad=acaaaba.

Reduce RHS:

Referenced by [65].

Overlap of [38] acaaabab=caacaaa with [54] aaab=dabaca:

Critical pair: acdabacaab=caacaaa.

Reduce LHS:

Defines rule #14.

Referenced by [64], [67].

Simplify [42] acaacabd=baaabab.

Reduce RHS:

Defines rule #11.

Simplify [49] acaacad=baaaba.

Reduce RHS:

Defines rule #9.

Overlap of [61] aabacaab=caacaaa with [56] abacab=caaac:

Critical pair: aabacacaaac=caacaaaacab.

Flip LHS and RHS.

Referenced by [71].

Overlap of [2] bb=c with [60] bacaacaad=aabacaa:

Critical pair: baabacaa=cacaacaad.

Flip LHS and RHS.

Referenced by [68].

Overlap of [48] acaacaabd=baacaaa with [41] dc=1:

Critical pair: acaacaab=baacaaac.

Defines rule #13.

Referenced by [67].

Overlap of [66] acaacaab=baacaaac with [61] aabacaab=caacaaa:

Critical pair: acaaccaacaaa=baacaaacacaab.

Flip LHS and RHS.

Referenced by [75].

Overlap of [41] dc=1 with [65] cacaacaad=baabacaa:

Critical pair: dbaabacaa=acaacaad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [40] db=bd with [51] baacaaaacaaca=bdaabac:

Critical pair: dbdaabac=bdaacaaaacaaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [72].

Overlap of [59] aaacacaac=dababcacaaca with [5] cb=bc:

Critical pair: aaacacaabc=dababcacaacab.

Defines rule #18.

Overlap of [41] dc=1 with [64] caacaaaacab=aabacacaaac:

Critical pair: daabacacaaac=aacaaaacab.

Flip LHS and RHS.

Defines rule #19.

Overlap of [2] bb=c with [69] bdaacaaaacaaca=bddaabac:

Critical pair: bbddaabac=cdaacaaaacaaca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [73].

Overlap of [72] aacaaaacaaca=daabac with [46] acaacaaa=bd:

Critical pair: aacaaaacaacbd=daabaccaacaaa.

Reduce LHS:

Defines rule #21.

Referenced by [74].

Overlap of [73] aacaaaacaab=daabaccaacaaa with [2] bb=c:

Critical pair: aacaaaacaac=daabaccaacaaab.

Reduce RHS:

Defines rule #20.

Overlap of [2] bb=c with [67] baacaaacacaab=acaaccaacaaa:

Critical pair: bacaaccaacaaa=caacaaacacaab.

Flip LHS and RHS.

Referenced by [76].

Overlap of [41] dc=1 with [75] caacaaacacaab=bacaaccaacaaa:

Critical pair: dbacaaccaacaaa=aacaaacacaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.