Certificate for #1431 ⟨a, b | aababbabba=1⟩

Completion settings:

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

Axiom: aababbabba=1.

Referenced by [4].

Axiom: bb=c.

Defines rule #5.

Referenced by [3], [4], [5], [12], [28], [33], [36], [40], [45], [51].

Axiom: abbaaaba=d.

Reduce LHS:

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

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

Critical pair: aabacabba=1.

Reduce LHS:

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

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

Critical pair: bc=cb.

Defines rule #3.

Referenced by [22], [29], [34], [42], [46], [49].

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

Critical pair: aabacac=abacaca.

Flip LHS and RHS.

Referenced by [14], [20].

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

Critical pair: acaaabd=dcaaaba.

Flip LHS and RHS.

Referenced by [15].

Overlap of [4] aabacaca=1 with [3] acaaaba=d:

Critical pair: aabacd=aaba.

Referenced by [10].

Overlap of [4] aabacaca=1 with [3] acaaaba=d:

Critical pair: aabacacd=caaaba.

Flip LHS and RHS.

Referenced by [13], [16].

Overlap of [4] aabacaca=1 with [8] aabacd=aaba:

Critical pair: aabacacaaba=abacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] aabacaca=1 with [10] abacd=aba:

Critical pair: aabacacaba=bacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

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

Critical pair: bba=cacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [16].

Overlap of [3] acaaaba=d with [9] caaaba=aabacacd:

Critical pair: aaabacacd=d.

Reduce LHS:

Defines rule #14.

Referenced by [14], [17], [18], [20], [21], [30], [31].

Overlap of [4] aabacaca=1 with [6] abacaca=aabacac:

Critical pair: aaabacac=1.

Reduce LHS:

Defines rule #2.

Referenced by [15], [18], [19], [20], [21], [23], [28], [33], [34], [35], [36], [42], [43], [45], [46], [50].

Overlap of [7] dcaaaba=acaaabd with [14] dc=1:

Critical pair: aaaba=acaaabd.

Flip LHS and RHS.

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

Simplify [9] caaaba=aabacacd.

Reduce RHS:

Referenced by [20], [21].

Overlap of [13] aaabaca=d with [15] acaaabd=aaaba:

Critical pair: aaabaaaba=daabd.

Referenced by [24].

Overlap of [13] aaabaca=d with [15] acaaabd=aaaba:

Critical pair: aaabacaaaba=dcaaabd.

Reduce LHS:

Reduce RHS:

Referenced by [25].

Overlap of [15] acaaabd=aaaba with [14] dc=1:

Critical pair: acaaab=aaabac.

Referenced by [21], [31].

Overlap of [16] caaaba=aabaca with [13] aaabaca=d:

Critical pair: cd=aabacaca.

Reduce RHS:

Defines rule #1.

Referenced by [22], [32], [48], [52].

Overlap of [16] caaaba=aabaca with [13] aaabaca=d:

Critical pair: caaabd=aabacaaabaca.

Reduce RHS:

Referenced by [26].

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

Critical pair: b=cbd.

Flip LHS and RHS.

Referenced by [23].

Overlap of [14] dc=1 with [22] cbd=b:

Critical pair: db=bd.

Flip LHS and RHS.

Defines rule #4.

Referenced by [24], [25], [26], [27], [33], [44], [47], [52].

Simplify [17] aaabaaaba=daabd.

Reduce RHS:

Referenced by [38].

Simplify [18] daaba=aaabd.

Reduce RHS:

Defines rule #7.

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

Overlap of [21] caaabd=aaba with [23] bd=db:

Critical pair: caaadb=aaba.

Referenced by [28].

Overlap of [23] bd=db with [25] daaba=aaadb:

Critical pair: baaadb=dbaaba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [34], [39].

Overlap of [26] caaadb=aaba with [2] bb=c:

Critical pair: caaadc=aabab.

Reduce LHS:

Defines rule #6.

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

Overlap of [5] bc=cb with [28] caaa=aabab:

Critical pair: baabab=cbaaa.

Flip LHS and RHS.

Defines rule #10.

Referenced by [40], [49].

Overlap of [28] caaa=aabab with [13] aaabaca=d:

Critical pair: cad=aabababaca.

Flip LHS and RHS.

Referenced by [31].

Overlap of [19] acaaab=aaabac with [30] aabababaca=cad:

Critical pair: acacad=aaabacababaca.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [20] cd=1 with [31] dbabaca=acacad:

Critical pair: cacacad=babaca.

Flip LHS and RHS.

Defines rule #9.

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

Overlap of [23] bd=db with [31] dbabaca=acacad:

Critical pair: bacacad=dbbabaca.

Reduce RHS:

Referenced by [34], [35].

Overlap of [31] dbabaca=acacad with [33] bacacad=abaca:

Critical pair: dbaabaca=acacadcad.

Reduce LHS:

Reduce RHS:

Defines rule #12.

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

Overlap of [33] bacacad=abaca with [14] dc=1:

Critical pair: bacaca=abacac.

Defines rule #8.

Overlap of [25] daaba=aaadb with [32] babaca=cacacad:

Critical pair: daacacacad=aaadbbaca.

Reduce RHS:

Referenced by [43].

Overlap of [32] babaca=cacacad with [28] caaa=aabab:

Critical pair: babaaabab=cacacadaa.

Reduce LHS:

Referenced by [45].

Overlap of [24] aaabaaaba=daadb with [34] baaaba=acacaad:

Critical pair: aaaacacaad=daadb.

Referenced by [42].

Overlap of [25] daaba=aaadb with [34] baaaba=acacaad:

Critical pair: daaacacaad=aaadbaaba.

Reduce RHS:

Referenced by [46].

Overlap of [29] cbaaa=baabab with [34] baaaba=acacaad:

Critical pair: cacacaad=baababba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [34] baaaba=acacaad with [32] babaca=cacacad:

Critical pair: baaacacacad=acacaadbaca.

Referenced by [50].

Overlap of [38] aaaacacaad=daadb with [14] dc=1:

Critical pair: aaaacacaa=daadbc.

Reduce RHS:

Defines rule #22.

Overlap of [36] daacacacad=aaaaca with [14] dc=1:

Critical pair: daacacaca=aaaacac.

Defines rule #15.

Referenced by [44].

Overlap of [23] bd=db with [43] daacacaca=aaaacac:

Critical pair: baaaacac=dbaacacaca.

Flip LHS and RHS.

Defines rule #17.

Overlap of [37] baacacaadb=cacacadaa with [2] bb=c:

Critical pair: baacacaadc=cacacadaab.

Reduce LHS:

Defines rule #16.

Overlap of [39] daaacacaad=aaabaaadb with [14] dc=1:

Critical pair: daaacacaa=aaabaaadbc.

Reduce RHS:

Defines rule #18.

Referenced by [47].

Overlap of [23] bd=db with [46] daaacacaa=aaabaaab:

Critical pair: baaabaaab=dbaaacacaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [48].

Overlap of [20] cd=1 with [47] dbaaacacaa=acacaadaab:

Critical pair: cacacaadaab=baaacacaa.

Flip LHS and RHS.

Defines rule #19.

Referenced by [49].

Overlap of [29] cbaaa=baabab with [48] baaacacaa=cacacaadaab:

Critical pair: ccacacaadaab=baababcacaa.

Reduce RHS:

Referenced by [51].

Overlap of [41] baaacacacad=acacaadbaca with [14] dc=1:

Critical pair: baaacacaca=acacaadbacac.

Defines rule #20.

Overlap of [49] ccacacaadaab=baabacbacaa with [2] bb=c:

Critical pair: ccacacaadaac=baabacbacaab.

Referenced by [52].

Overlap of [51] ccacacaadaac=baabacbacaab with [20] cd=1:

Critical pair: ccacacaadaa=baabacbacaabd.

Reduce RHS:

Defines rule #21.