Certificate for #2928 ⟨a, b | aaababaaaba=1⟩

Completion settings:

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

Axiom: aaababaaaba=1.

Referenced by [4], [5], [6], [10], [14], [24].

Axiom: baaabaa=c.

Referenced by [3], [5], [6], [7], [9], [20], [25].

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

Critical pair: baaac=cabaa.

Flip LHS and RHS.

Referenced by [8], [21].

Overlap of [1] aaababaaaba=1 with [1] aaababaaaba=1:

Critical pair: aaabab=baaaba.

Referenced by [8], [14], [17], [24].

Overlap of [1] aaababaaaba=1 with [2] baaabaa=c:

Critical pair: aaabac=a.

Referenced by [7], [8], [11], [12], [17].

Overlap of [2] baaabaa=c with [1] aaababaaaba=1:

Critical pair: baaab=cababaaaba.

Flip LHS and RHS.

Referenced by [26].

Overlap of [2] baaabaa=c with [5] aaabac=a:

Critical pair: baaaba=cabac.

Referenced by [8], [9], [10], [11], [14], [17], [20], [24], [25], [26].

Overlap of [5] aaabac=a with [3] cabaa=baaac:

Critical pair: aaababaaac=aabaa.

Reduce LHS:

Referenced by [27].

Overlap of [2] baaabaa=c with [7] baaaba=cabac:

Critical pair: cabaca=c.

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

Overlap of [7] baaaba=cabac with [1] aaababaaaba=1:

Critical pair: b=cabacbaaaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [7] baaaba=cabac with [5] aaabac=a:

Critical pair: ba=cabacc.

Flip LHS and RHS.

Referenced by [16].

Overlap of [5] aaabac=a with [9] cabaca=c:

Critical pair: aaabac=aabaca.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [9] cabaca=c with [9] cabaca=c:

Critical pair: cabac=cbaca.

Referenced by [14], [16], [17], [20], [23], [24], [25], [26], [27], [28].

Overlap of [12] aabaca=a with [1] aaababaaaba=1:

Critical pair: aabac=aaababaaaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [12] aabaca=a with [9] cabaca=c:

Critical pair: aabac=abaca.

Referenced by [18], [20], [21], [22], [23], [28], [29], [35], [38], [41], [57].

Simplify [11] cabacc=ba.

Reduce LHS:

Referenced by [17], [18], [19], [23], [28], [36], [40].

Overlap of [5] aaabac=a with [16] cbacac=ba:

Critical pair: aaababa=abacac.

Reduce LHS:

Referenced by [23], [24], [25], [26], [27], [30], [31].

Overlap of [16] cbacac=ba with [9] cabaca=c:

Critical pair: cbacac=baabaca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [16] cbacac=ba with [16] cbacac=ba:

Critical pair: cbacaba=babacac.

Referenced by [20].

Overlap of [2] baaabaa=c with [15] aabac=abaca:

Critical pair: baaababaca=cbac.

Reduce LHS:

Referenced by [32].

Overlap of [3] cabaa=baaac with [15] aabac=abaca:

Critical pair: cababaca=baaacbac.

Referenced by [33].

Overlap of [12] aabaca=a with [15] aabac=abaca:

Critical pair: abacaa=a.

Referenced by [35], [39], [53].

Overlap of [15] aabac=abaca with [16] cbacac=ba:

Critical pair: aababa=abacabacac.

Reduce RHS:

Referenced by [41].

Overlap of [1] aaababaaaba=1 with [4] aaabab=baaaba:

Critical pair: baaabaaaaba=1.

Reduce LHS:

Referenced by [44].

Overlap of [2] baaabaa=c with [7] baaaba=cabac:

Critical pair: cabaca=c.

Reduce LHS:

Referenced by [26], [27], [30], [31], [36], [44].

Overlap of [6] cababaaaba=baaab with [7] baaaba=cabac:

Critical pair: cabacabac=baaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33], [42].

Overlap of [8] cabacaaac=aabaa with [13] cabac=cbaca:

Critical pair: cbacaaaac=aabaa.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [10] cabaccabac=b with [13] cabac=cbaca:

Critical pair: cbacacabac=b.

Reduce LHS:

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

Simplify [14] cbacaaaaba=aabac.

Reduce RHS:

Referenced by [30].

Overlap of [29] cbacaaaaba=abaca with [17] cbacaa=abacac:

Critical pair: abacacaaba=abaca.

Reduce LHS:

Referenced by [44], [45].

Simplify [17] cbacaa=abacac.

Reduce RHS:

Referenced by [37].

Overlap of [20] babacacca=cbac with [28] babaca=b:

Critical pair: bcca=cbac.

Flip LHS and RHS.

Referenced by [33], [36], [37], [38], [40], [41], [42].

Simplify [21] cababaca=baaacbac.

Reduce RHS:

Referenced by [34].

Overlap of [33] cababaca=bccacca with [28] babaca=b:

Critical pair: cab=bccacca.

Referenced by [35], [36], [38], [43], [55], [56], [57].

Overlap of [22] abacaa=a with [15] aabac=abaca:

Critical pair: abacabaca=abac.

Reduce LHS:

Referenced by [46].

Overlap of [25] abacac=c with [16] cbacac=ba:

Critical pair: abacaba=cbacac.

Reduce LHS:

Reduce RHS:

Referenced by [46].

Simplify [31] cbacaa=c.

Reduce LHS:

Referenced by [38], [52], [55], [56], [58].

Overlap of [37] bccaaa=c with [15] aabac=abaca:

Critical pair: bccaaabaca=cabac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [55], [56].

Overlap of [28] babaca=b with [22] abacaa=a:

Critical pair: babaca=bbacaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [57].

Overlap of [16] cbacac=ba with [32] cbac=bcca:

Critical pair: bccaac=ba.

Referenced by [46].

Overlap of [27] aabaa=caac with [15] aabac=abaca:

Critical pair: aababaca=caacbac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [43].

Simplify [26] baaab=cbac.

Reduce RHS:

Referenced by [43], [55], [56].

Overlap of [27] aabaa=caac with [42] baaab=bcca:

Critical pair: aabcca=caacab.

Reduce RHS:

Referenced by [47].

Overlap of [24] abacacaaba=1 with [25] abacac=c:

Critical pair: caaba=1.

Reduce LHS:

Referenced by [45], [48].

Simplify [30] caaba=abaca.

Reduce RHS:

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

Overlap of [35] ababccaccaaca=abac with [36] ababccaccaa=bccaac:

Critical pair: bccaacca=abac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [47], [48], [53].

Simplify [43] aabcca=abacccacca.

Reduce RHS:

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

Simplify [44] abaca=1.

Reduce LHS:

Defines rule #3.

Referenced by [54], [57].

Overlap of [45] caaba=1 with [27] aabaa=caac:

Critical pair: ccaac=a.

Defines rule #2.

Referenced by [50], [51], [55], [56], [57].

Overlap of [49] ccaac=a with [45] caaba=1:

Critical pair: ccaa=aaaba.

Flip LHS and RHS.

Referenced by [52], [53], [54].

Overlap of [49] ccaac=a with [49] ccaac=a:

Critical pair: ccaaa=acaac.

Defines rule #1.

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

Overlap of [37] bccaaa=c with [50] aaaba=ccaa:

Critical pair: bccccaa=cba.

Flip LHS and RHS.

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

Overlap of [22] abacaa=a with [50] aaaba=ccaa:

Critical pair: abacccaa=aaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [57].

Overlap of [48] bacaa=1 with [50] aaaba=ccaa:

Critical pair: bacccaa=aba.

Flip LHS and RHS.

Referenced by [55], [57].

Overlap of [54] aba=bacccaa with [42] baaab=bcca:

Critical pair: abcca=bacccaaaab.

Reduce RHS:

Referenced by [57].

Overlap of [52] cba=bccccaa with [42] baaab=bcca:

Critical pair: cbcca=bccccaaaab.

Reduce RHS:

Referenced by [57].

Overlap of [15] aabac=abaca with [34] cab=bccacca:

Critical pair: aababccacca=abacaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [58].

Overlap of [37] bccaaa=c with [57] ab=baccca:

Critical pair: bccaabaccca=cb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.