Certificate for #2975 ⟨a, b | aaabbabbaba=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. abbabaaaa=d

Axiom: aaabbabbaba=1.

Referenced by [4].

Axiom: bb=c.

Defines rule #5.

Referenced by [3], [4], [5], [19], [33], [39], [42], [49], [58].

Axiom: abbabaaaa=d.

Reduce LHS:

Defines rule #15.

Referenced by [6], [7], [8], [9], [10], [12], [20], [23], [24], [26], [30], [37], [49].

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

Critical pair: aaacabbaba=1.

Reduce LHS:

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

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

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [28], [45], [51], [52], [55], [57].

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

Critical pair: acabaaad=dcabaaaa.

Referenced by [36].

Overlap of [3] acabaaaa=d with [4] aaacacaba=1:

Critical pair: acaba=dcacaba.

Flip LHS and RHS.

Referenced by [13].

Overlap of [3] acabaaaa=d with [4] aaacacaba=1:

Critical pair: acabaa=dacacaba.

Flip LHS and RHS.

Referenced by [30], [34], [35].

Overlap of [3] acabaaaa=d with [4] aaacacaba=1:

Critical pair: acabaaa=daacacaba.

Flip LHS and RHS.

Referenced by [24].

Overlap of [4] aaacacaba=1 with [3] acabaaaa=d:

Critical pair: aaacd=aaa.

Referenced by [12], [16].

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

Critical pair: aaacacab=aacacaba.

Referenced by [13], [14].

Overlap of [3] acabaaaa=d with [10] aaacd=aaa:

Critical pair: acabaaaa=dcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [7] dcacaba=acaba with [4] aaacacaba=1:

Critical pair: dcacab=acabaaacacaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [4] aaacacaba=1 with [11] aaacacab=aacacaba:

Critical pair: aacacabaa=1.

Referenced by [15], [16], [17], [18], [24], [26].

Overlap of [13] acabaacacabaa=dcacab with [14] aacacabaa=1:

Critical pair: acab=dcacab.

Flip LHS and RHS.

Referenced by [19].

Overlap of [14] aacacabaa=1 with [10] aaacd=aaa:

Critical pair: aacacabaaa=acd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20], [21].

Overlap of [14] aacacabaa=1 with [14] aacacabaa=1:

Critical pair: aacacab=cacabaa.

Referenced by [18], [26].

Overlap of [14] aacacabaa=1 with [14] aacacabaa=1:

Critical pair: aacacaba=acacabaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [15] dcacab=acab with [2] bb=c:

Critical pair: dcacac=acabb.

Reduce RHS:

Referenced by [20], [21].

Overlap of [19] dcacac=acac with [3] acabaaaa=d:

Critical pair: dcacd=acacabaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [19] dcacac=acac with [16] acd=a:

Critical pair: dcaca=acacd.

Reduce RHS:

Referenced by [23].

Overlap of [12] dcd=d with [20] cda=dca:

Critical pair: ddca=da.

Referenced by [24].

Overlap of [20] cda=dca with [3] acabaaaa=d:

Critical pair: cdd=dcacabaaaa.

Reduce RHS:

Referenced by [25].

Overlap of [22] ddca=da with [14] aacacabaa=1:

Critical pair: ddc=daacacabaa.

Reduce RHS:

Referenced by [25].

Overlap of [23] cdd=d with [24] ddc=d:

Critical pair: cd=dc.

Referenced by [26], [27].

Overlap of [14] aacacabaa=1 with [17] aacacab=cacabaa:

Critical pair: cacabaaaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [27], [28], [31], [36], [37], [40], [49], [56], [59].

Simplify [25] cd=dc.

Reduce RHS:

Defines rule #2.

Referenced by [29], [32], [34], [35], [38], [39], [42], [48], [51], [52], [54], [55].

Overlap of [26] dc=1 with [5] cb=bc:

Critical pair: dbc=b.

Referenced by [29].

Overlap of [28] dbc=b with [27] cd=1:

Critical pair: db=bd.

Defines rule #4.

Referenced by [37], [38], [41], [50], [53], [59].

Overlap of [8] dacacaba=acabaa with [3] acabaaaa=d:

Critical pair: dacacabd=acabaacabaaaa.

Reduce RHS:

Referenced by [31].

Overlap of [30] dacacabd=acabad with [26] dc=1:

Critical pair: dacacab=acabadc.

Reduce RHS:

Referenced by [32], [33].

Overlap of [27] cd=1 with [31] dacacab=acaba:

Critical pair: cacaba=acacab.

Flip LHS and RHS.

Defines rule #6.

Overlap of [31] dacacab=acaba with [2] bb=c:

Critical pair: dacacac=acabab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [34], [39], [43], [46].

Overlap of [8] dacacaba=acabaa with [33] acabab=dacacac:

Critical pair: dacdacacac=acabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [35], [44].

Overlap of [8] dacacaba=acabaa with [34] acabaab=daacacac:

Critical pair: dacdaacacac=acabaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [38].

Simplify [6] acabaaad=dcabaaaa.

Reduce RHS:

Referenced by [37], [38].

Overlap of [3] acabaaaa=d with [36] acabaaad=abaaaa:

Critical pair: acabaaaabaaaa=dcabaaad.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

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

Overlap of [36] acabaaad=abaaaa with [29] db=bd:

Critical pair: acabaaabd=abaaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [43], [44], [46], [47], [53].

Overlap of [33] acabab=dacacac with [37] abaaad=bdaaaa:

Critical pair: acabbdaaaa=dacacacaaad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [48].

Overlap of [37] abaaad=bdaaaa with [26] dc=1:

Critical pair: abaaa=bdaaaac.

Flip LHS and RHS.

Referenced by [42], [43], [44].

Overlap of [37] abaaad=bdaaaa with [29] db=bd:

Critical pair: abaaabd=bdaaaab.

Defines rule #12.

Referenced by [47].

Overlap of [2] bb=c with [40] bdaaaac=abaaa:

Critical pair: babaaa=cdaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [45], [49].

Overlap of [40] bdaaaac=abaaa with [33] acabab=dacacac:

Critical pair: bdaaadacacac=abaaaabab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [40] bdaaaac=abaaa with [34] acabaab=daacacac:

Critical pair: bdaaadaacacac=abaaaabaab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [55].

Overlap of [42] aaaac=babaaa with [5] cb=bc:

Critical pair: aaaabc=babaaab.

Defines rule #11.

Referenced by [57].

Overlap of [33] acabab=dacacac with [38] abaaaab=daaacaca:

Critical pair: acabdaaacaca=dacacacaaaab.

Flip LHS and RHS.

Referenced by [54].

Overlap of [38] abaaaab=daaacaca with [37] abaaad=bdaaaa:

Critical pair: abaaabdaaaa=daaacacaaaad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [52].

Overlap of [27] cd=1 with [39] dacacacaaad=acaaaaa:

Critical pair: cacaaaaa=acacacaaad.

Flip LHS and RHS.

Defines rule #16.

Referenced by [49], [50].

Overlap of [42] aaaac=babaaa with [48] acacacaaad=cacaaaaa:

Critical pair: aaacacaaaaa=babaaaacacaaad.

Reduce RHS:

Defines rule #24.

Overlap of [48] acacacaaad=cacaaaaa with [29] db=bd:

Critical pair: acacacaaabd=cacaaaaab.

Defines rule #18.

Overlap of [27] cd=1 with [43] daaacacaab=bdaaadacacac:

Critical pair: cbdaaadacacac=aaacacaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [27] cd=1 with [47] daaacacaaaad=bdaaaabaaaa:

Critical pair: cbdaaaabaaaa=aaacacaaaad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [53].

Overlap of [52] aaacacaaaad=baaaabaaaa with [29] db=bd:

Critical pair: aaacacaaaabd=baaaabaaaab.

Reduce RHS:

Referenced by [56].

Overlap of [27] cd=1 with [46] dacacacaaaab=acabdaaacaca:

Critical pair: cacabdaaacaca=acacacaaaab.

Flip LHS and RHS.

Defines rule #19.

Overlap of [27] cd=1 with [44] daaacacaaab=bdaaadaacacac:

Critical pair: cbdaaadaacacac=aaacacaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [53] aaacacaaaabd=baaadaaacaca with [26] dc=1:

Critical pair: aaacacaaaab=baaadaaacacac.

Defines rule #22.

Referenced by [57].

Overlap of [56] aaacacaaaab=baaadaaacacac with [45] aaaabc=babaaab:

Critical pair: aaacacbabaaab=baaadaaacacacc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [58].

Overlap of [2] bb=c with [57] baaadaaacacacc=aaacabcabaaab:

Critical pair: baaacabcabaaab=caaadaaacacacc.

Flip LHS and RHS.

Referenced by [59].

Overlap of [26] dc=1 with [58] caaadaaacacacc=baaacabcabaaab:

Critical pair: dbaaacabcabaaab=aaadaaacacacc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.