Certificate for #3111 ⟨a, b | aabbaabbaba=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. aabbabaaa=d

Axiom: aabbaabbaba=1.

Referenced by [4].

Axiom: bb=c.

Defines rule #5.

Referenced by [3], [4], [5], [14], [16], [18], [29], [30], [33], [38], [47], [48].

Axiom: aabbabaaa=d.

Reduce LHS:

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

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

Critical pair: aacaabbaba=1.

Reduce LHS:

Referenced by [6], [8], [9], [10], [11], [13].

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

Critical pair: bc=cb.

Defines rule #3.

Referenced by [12], [27], [32], [44], [47].

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

Critical pair: aacaacab=acaacaba.

Flip LHS and RHS.

Referenced by [8], [13], [27], [30].

Overlap of [3] aacabaaa=d with [3] aacabaaa=d:

Critical pair: aacabad=dcabaaa.

Flip LHS and RHS.

Referenced by [21].

Overlap of [3] aacabaaa=d with [4] aacaacaba=1:

Critical pair: aacabaa=dacaacaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [38].

Overlap of [4] aacaacaba=1 with [3] aacabaaa=d:

Critical pair: aacd=aa.

Referenced by [10].

Overlap of [4] aacaacaba=1 with [9] aacd=aa:

Critical pair: aacaacabaa=acd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] aacaacaba=1 with [10] acd=a:

Critical pair: aacaacaba=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [12], [15], [16], [18], [20], [23], [28], [34], [39], [41], [42], [43], [45], [46], [49].

Overlap of [5] bc=cb with [11] cd=1:

Critical pair: b=cbd.

Flip LHS and RHS.

Referenced by [16].

Overlap of [4] aacaacaba=1 with [6] acaacaba=aacaacab:

Critical pair: aaacaacab=1.

Referenced by [14], [17], [22].

Overlap of [13] aaacaacab=1 with [2] bb=c:

Critical pair: aaacaacac=b.

Referenced by [15], [16].

Overlap of [14] aaacaacac=b with [11] cd=1:

Critical pair: aaacaaca=bd.

Referenced by [16], [17], [19].

Overlap of [14] aaacaacac=b with [12] cbd=b:

Critical pair: aaacaacab=bbd.

Reduce LHS:

Reduce RHS:

Referenced by [17], [24].

Overlap of [13] aaacaacab=1 with [16] bdb=1:

Critical pair: aaacaaca=db.

Reduce LHS:

Defines rule #4.

Referenced by [18], [19], [29], [34], [35], [41], [47], [49].

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

Critical pair: bdb=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [21], [25], [27], [29], [31], [47].

Simplify [15] aaacaaca=bd.

Reduce RHS:

Defines rule #16.

Referenced by [20], [22], [27].

Overlap of [19] aaacaaca=db with [19] aaacaaca=db:

Critical pair: aaacaacdb=dbaacaaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30], [39].

Simplify [7] dcabaaa=aacabad.

Reduce LHS:

Referenced by [22].

Overlap of [13] aaacaacab=1 with [21] abaaa=aacabad:

Critical pair: aaacaacaacabad=aaa.

Reduce LHS:

Referenced by [23], [24].

Overlap of [11] cd=1 with [22] dbacabad=aaa:

Critical pair: caaa=bacabad.

Flip LHS and RHS.

Referenced by [25].

Overlap of [16] bdb=1 with [22] dbacabad=aaa:

Critical pair: baaa=acabad.

Defines rule #6.

Referenced by [47].

Overlap of [23] bacabad=caaa with [18] dc=1:

Critical pair: bacaba=caaac.

Defines rule #7.

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

Overlap of [25] bacaba=caaac with [25] bacaba=caaac:

Critical pair: bacacaaac=caaaccaba.

Referenced by [42].

Overlap of [19] aaacaaca=db with [6] acaacaba=aacaacab:

Critical pair: aaacaacaacaacab=dbcaacaba.

Reduce LHS:

Reduce RHS:

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

Overlap of [11] cd=1 with [27] dbacaacab=baacaba:

Critical pair: cbaacaba=bacaacab.

Defines rule #10.

Overlap of [17] bd=db with [27] dbacaacab=baacaba:

Critical pair: bbaacaba=dbbacaacab.

Reduce LHS:

Reduce RHS:

Defines rule #8.

Referenced by [31], [32], [47].

Overlap of [27] dbacaacab=baacaba with [6] acaacaba=aacaacab:

Critical pair: dbaacaacab=baacabaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

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

Overlap of [18] dc=1 with [29] caacaba=acaacab:

Critical pair: dacaacab=aacaba.

Referenced by [33].

Overlap of [29] caacaba=acaacab with [25] bacaba=caaac:

Critical pair: caacacaaac=acaacabcaba.

Reduce RHS:

Referenced by [43].

Overlap of [31] dacaacab=aacaba with [2] bb=c:

Critical pair: dacaacac=aacabab.

Referenced by [34].

Overlap of [33] dacaacac=aacabab with [11] cd=1:

Critical pair: dacaaca=aacababd.

Reduce RHS:

Defines rule #9.

Referenced by [35].

Overlap of [17] bd=db with [34] dacaaca=aacabadb:

Critical pair: baacabadb=dbacaaca.

Flip LHS and RHS.

Defines rule #11.

Overlap of [25] bacaba=caaac with [30] baacabaa=aaacaac:

Critical pair: bacaaaacaac=caaacacabaa.

Referenced by [45].

Overlap of [30] baacabaa=aaacaac with [30] baacabaa=aaacaac:

Critical pair: baacaaaacaac=aaacaaccabaa.

Referenced by [46].

Overlap of [8] daacaacab=aacabaa with [2] bb=c:

Critical pair: daacaacac=aacabaab.

Referenced by [41].

Overlap of [11] cd=1 with [20] dbaacaaca=aaacaab:

Critical pair: caaacaab=baacaaca.

Flip LHS and RHS.

Defines rule #13.

Referenced by [40].

Overlap of [30] baacabaa=aaacaac with [39] baacaaca=caaacaab:

Critical pair: baacacaaacaab=aaacaaccaaca.

Referenced by [48].

Overlap of [38] daacaacac=aacabaab with [11] cd=1:

Critical pair: daacaaca=aacabaabd.

Reduce RHS:

Defines rule #12.

Overlap of [26] bacacaaac=caaaccaba with [11] cd=1:

Critical pair: bacacaaa=caaaccabad.

Defines rule #15.

Overlap of [32] caacacaaac=acaacacbaba with [11] cd=1:

Critical pair: caacacaaa=acaacacbabad.

Defines rule #17.

Referenced by [44].

Overlap of [5] bc=cb with [43] caacacaaa=acaacacbabad:

Critical pair: bacaacacbabad=cbaacacaaa.

Flip LHS and RHS.

Defines rule #18.

Overlap of [36] bacaaaacaac=caaacacabaa with [11] cd=1:

Critical pair: bacaaaacaa=caaacacabaad.

Defines rule #19.

Overlap of [37] baacaaaacaac=aaacaaccabaa with [11] cd=1:

Critical pair: baacaaaacaa=aaacaaccabaad.

Defines rule #21.

Referenced by [47].

Overlap of [2] bb=c with [46] baacaaaacaa=aaacaaccabaad:

Critical pair: baaacaaccabaad=caacaaaacaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [40] baacacaaacaab=aaacaaccaaca with [2] bb=c:

Critical pair: baacacaaacaac=aaacaaccaacab.

Referenced by [49].

Overlap of [48] baacacaaacaac=aaacaaccaacab with [11] cd=1:

Critical pair: baacacaaacaa=aaacaaccaacabd.

Reduce RHS:

Defines rule #22.