Certificate for #2946 ⟨a, b | aaababbabba=1⟩

Completion settings:

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

Axiom: aaababbabba=1.

Referenced by [4].

Axiom: bb=c.

Defines rule #5.

Referenced by [3], [4], [5], [16], [24], [30], [40], [42], [45], [51], [55], [56], [57], [61].

Axiom: abbaaaaba=d.

Reduce LHS:

Referenced by [7], [8], [9], [10].

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

Critical pair: aaabacabba=1.

Reduce LHS:

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

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

Critical pair: bc=cb.

Defines rule #3.

Referenced by [34], [40], [43], [49], [50], [60].

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

Critical pair: aaabacac=aabacaca.

Flip LHS and RHS.

Referenced by [8], [15].

Overlap of [3] acaaaaba=d with [4] aaabacaca=1:

Critical pair: aca=dcaca.

Flip LHS and RHS.

Referenced by [11].

Overlap of [3] acaaaaba=d with [4] aaabacaca=1:

Critical pair: acaaaab=daabacaca.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [4] aaabacaca=1 with [3] acaaaaba=d:

Critical pair: aaabacd=aaaba.

Referenced by [12].

Overlap of [4] aaabacaca=1 with [3] acaaaaba=d:

Critical pair: aaabacacd=caaaaba.

Flip LHS and RHS.

Referenced by [27].

Overlap of [7] dcaca=aca with [4] aaabacaca=1:

Critical pair: dcac=acaaabacaca.

Reduce RHS:

Referenced by [17].

Overlap of [4] aaabacaca=1 with [9] aaabacd=aaaba:

Critical pair: aaabacacaaaba=aabacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [4] aaabacaca=1 with [12] aabacd=aaba:

Critical pair: aaabacacaaba=abacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [14].

Overlap of [4] aaabacaca=1 with [13] abacd=aba:

Critical pair: aaabacacaba=bacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [4] aaabacaca=1 with [6] aabacaca=aaabacac:

Critical pair: aaaabacac=1.

Referenced by [18], [19], [20], [23].

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

Critical pair: bba=cacd.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [11] dcac=ac with [16] cacd=ca:

Critical pair: dca=acd.

Referenced by [19], [21].

Overlap of [15] aaaabacac=1 with [16] cacd=ca:

Critical pair: aaaabaca=d.

Defines rule #15.

Referenced by [20], [32], [33], [40], [55].

Overlap of [17] dca=acd with [15] aaaabacac=1:

Critical pair: dc=acdaaabacac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [15] aaaabacac=1 with [18] aaaabaca=d:

Critical pair: dc=1.

Defines rule #2.

Referenced by [21], [22], [30], [32], [34], [37], [38], [40], [41], [42], [45], [49], [50], [53], [55], [56], [57], [58].

Overlap of [17] dca=acd with [20] dc=1:

Critical pair: a=acd.

Flip LHS and RHS.

Referenced by [26], [32].

Simplify [19] acacaaaab=dc.

Reduce RHS:

Referenced by [23], [24], [25], [28].

Overlap of [15] aaaabacac=1 with [22] acacaaaab=1:

Critical pair: aaaabac=acaaaab.

Flip LHS and RHS.

Referenced by [25].

Overlap of [22] acacaaaab=1 with [2] bb=c:

Critical pair: acacaaaac=b.

Referenced by [25], [26].

Overlap of [24] acacaaaac=b with [22] acacaaaab=1:

Critical pair: acacaaa=bacaaaab.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [24] acacaaaac=b with [21] acd=a:

Critical pair: acacaaaa=bd.

Referenced by [28], [31].

Simplify [10] caaaaba=aaabacacd.

Reduce RHS:

Referenced by [40].

Overlap of [22] acacaaaab=1 with [26] acacaaaa=bd:

Critical pair: bdb=1.

Referenced by [29], [35].

Overlap of [28] bdb=1 with [28] bdb=1:

Critical pair: bd=db.

Defines rule #4.

Referenced by [30], [31], [40], [44], [54], [62].

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

Critical pair: bdb=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [36], [46], [48], [59], [62].

Simplify [26] acacaaaa=bd.

Reduce RHS:

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

Overlap of [18] aaaabaca=d with [31] acacaaaa=db:

Critical pair: aaaabacdb=dcacaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [34], [39], [40], [47].

Overlap of [31] acacaaaa=db with [18] aaaabaca=d:

Critical pair: acacad=dbabaca.

Flip LHS and RHS.

Referenced by [35], [36].

Overlap of [31] acacaaaa=db with [31] acacaaaa=db:

Critical pair: acacaaadb=dbcacaaaa.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [28] bdb=1 with [33] dbabaca=acacad:

Critical pair: bacacad=abaca.

Referenced by [37].

Overlap of [30] cd=1 with [33] dbabaca=acacad:

Critical pair: cacacad=babaca.

Flip LHS and RHS.

Defines rule #7.

Referenced by [38], [39], [45], [52].

Overlap of [35] bacacad=abaca with [20] dc=1:

Critical pair: bacaca=abacac.

Defines rule #6.

Referenced by [38].

Overlap of [36] babaca=cacacad with [37] bacaca=abacac:

Critical pair: baabacac=cacacadca.

Reduce RHS:

Referenced by [46].

Overlap of [36] babaca=cacacad with [32] acaaaa=aaaabab:

Critical pair: babaaaabab=cacacadaaa.

Reduce LHS:

Referenced by [56].

Overlap of [27] caaaaba=aaabaca with [18] aaaabaca=d:

Critical pair: caaaabd=aaabacaaaabaca.

Reduce LHS:

Reduce RHS:

Referenced by [41], [42].

Overlap of [20] dc=1 with [40] caaaadb=aaaba:

Critical pair: daaaba=aaaadb.

Defines rule #9.

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

Overlap of [40] caaaadb=aaaba with [2] bb=c:

Critical pair: caaaadc=aaabab.

Reduce LHS:

Defines rule #8.

Referenced by [43], [55].

Overlap of [5] bc=cb with [42] caaaa=aaabab:

Critical pair: baaabab=cbaaaa.

Flip LHS and RHS.

Defines rule #11.

Referenced by [51], [60].

Overlap of [29] bd=db with [41] daaaba=aaaadb:

Critical pair: baaaadb=dbaaaba.

Flip LHS and RHS.

Defines rule #12.

Referenced by [49], [50].

Overlap of [41] daaaba=aaaadb with [36] babaca=cacacad:

Critical pair: daaacacacad=aaaadbbaca.

Reduce RHS:

Referenced by [53].

Overlap of [38] baabacac=cacacaa with [30] cd=1:

Critical pair: baabaca=cacacaad.

Defines rule #10.

Referenced by [47].

Overlap of [46] baabaca=cacacaad with [32] acaaaa=aaaabab:

Critical pair: baabaaaabab=cacacaadaaa.

Reduce LHS:

Referenced by [57].

Overlap of [25] baaaabac=acacaaa with [30] cd=1:

Critical pair: baaaaba=acacaaad.

Defines rule #13.

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

Overlap of [41] daaaba=aaaadb with [25] baaaabac=acacaaa:

Critical pair: daaaacacaaa=aaaadbaaabac.

Reduce RHS:

Defines rule #21.

Overlap of [44] dbaaaba=baaaadb with [25] baaaabac=acacaaa:

Critical pair: dbaaaacacaaa=baaaadbaaabac.

Reduce RHS:

Referenced by [59].

Overlap of [43] cbaaaa=baaabab with [48] baaaaba=acacaaad:

Critical pair: cacacaaad=baaababba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [48] baaaaba=acacaaad with [36] babaca=cacacad:

Critical pair: baaaacacacad=acacaaadbaca.

Referenced by [58].

Overlap of [45] daaacacacad=aaaaaca with [20] dc=1:

Critical pair: daaacacaca=aaaaacac.

Defines rule #16.

Referenced by [54], [55].

Overlap of [29] bd=db with [53] daaacacaca=aaaaacac:

Critical pair: baaaaacac=dbaaacacaca.

Flip LHS and RHS.

Defines rule #18.

Overlap of [53] daaacacaca=aaaaacac with [42] caaaa=aaabab:

Critical pair: daaacacaaaabab=aaaaacacaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [39] baacacaaadb=cacacadaaa with [2] bb=c:

Critical pair: baacacaaadc=cacacadaaab.

Reduce LHS:

Defines rule #17.

Overlap of [47] baaacacaaadb=cacacaadaaa with [2] bb=c:

Critical pair: baaacacaaadc=cacacaadaaab.

Reduce LHS:

Defines rule #20.

Overlap of [52] baaaacacacad=acacaaadbaca with [20] dc=1:

Critical pair: baaaacacaca=acacaaadbacac.

Defines rule #19.

Overlap of [30] cd=1 with [50] dbaaaacacaaa=acacaaadaaab:

Critical pair: cacacaaadaaab=baaaacacaaa.

Flip LHS and RHS.

Defines rule #22.

Referenced by [60].

Overlap of [43] cbaaaa=baaabab with [59] baaaacacaaa=cacacaaadaaab:

Critical pair: ccacacaaadaaab=baaababcacaaa.

Reduce RHS:

Referenced by [61].

Overlap of [60] ccacacaaadaaab=baaabacbacaaa with [2] bb=c:

Critical pair: ccacacaaadaaac=baaabacbacaaab.

Referenced by [62].

Overlap of [61] ccacacaaadaaac=baaabacbacaaab with [30] cd=1:

Critical pair: ccacacaaadaaa=baaabacbacaaabd.

Reduce RHS:

Defines rule #23.