Certificate for #3271 ⟨a, b | abbaaaabaab=1⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(a) = deg(d) = 0, a < d; deg(c) = deg(b) = 1, c < b
• Auxiliary generators:
  1. ababb=c
  2. abac=d

Axiom: abbaaaabaab=1.

Referenced by [4], [5], [6], [7].

Axiom: ababb=c.

Referenced by [5], [9], [11].

Axiom: abac=d.

Referenced by [8], [13], [14], [19].

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

Critical pair: abbaaaaba=baaaabaab.

Referenced by [6], [7].

Overlap of [2] ababb=c with [1] abbaaaabaab=1:

Critical pair: ab=caaaabaab.

Flip LHS and RHS.

Referenced by [6].

Overlap of [5] caaaabaab=ab with [1] abbaaaabaab=1:

Critical pair: caaaaba=abbaaaabaab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [7].

Overlap of [1] abbaaaabaab=1 with [4] abbaaaaba=baaaabaab:

Critical pair: baaaabaabab=1.

Reduce LHS:

Referenced by [8], [9], [12], [17].

Overlap of [3] abac=d with [7] caaaaba=1:

Critical pair: aba=daaaaba.

Flip LHS and RHS.

Referenced by [11], [14].

Overlap of [7] caaaaba=1 with [2] ababb=c:

Critical pair: caaac=bb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [10], [15], [23], [27], [36].

Overlap of [9] bb=caaac with [9] bb=caaac:

Critical pair: bcaaac=caaacb.

Flip LHS and RHS.

Defines rule #13.

Overlap of [8] daaaaba=aba with [2] ababb=c:

Critical pair: daaac=ababb.

Reduce RHS:

Referenced by [12].

Overlap of [11] daaac=c with [7] caaaaba=1:

Critical pair: daaa=caaaaba.

Reduce RHS:

Defines rule #2.

Referenced by [13], [14], [16], [20], [24], [25], [26], [28], [29], [30], [31], [32], [33], [35], [37], [39], [40], [41], [44], [45], [47], [48], [49], [51], [52].

Overlap of [12] daaa=1 with [3] abac=d:

Critical pair: daad=bac.

Flip LHS and RHS.

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

Overlap of [8] daaaaba=aba with [13] bac=daad:

Critical pair: daaaadaad=abac.

Reduce LHS:

Reduce RHS:

Referenced by [16], [18].

Overlap of [9] bb=caaac with [13] bac=daad:

Critical pair: bdaad=caaacac.

Flip LHS and RHS.

Referenced by [22].

Overlap of [14] adaad=d with [12] daaa=1:

Critical pair: adaa=daaa.

Reduce RHS:

Referenced by [17], [18].

Overlap of [7] caaaaba=1 with [16] adaa=1:

Critical pair: caaaab=daa.

Defines rule #4.

Referenced by [23], [29], [41].

Overlap of [14] adaad=d with [16] adaa=1:

Critical pair: ada=daa.

Referenced by [19], [20].

Overlap of [18] ada=daa with [3] abac=d:

Critical pair: add=daabac.

Reduce RHS:

Referenced by [20].

Overlap of [19] add=dad with [12] daaa=1:

Critical pair: ad=dadaaa.

Reduce RHS:

Defines rule #1.

Referenced by [21], [22], [28], [29], [30], [31], [37], [38], [39], [40], [42], [45], [49].

Simplify [13] bac=daad.

Reduce RHS:

Defines rule #3.

Referenced by [24], [28], [32], [37].

Simplify [15] caaacac=bdaad.

Reduce RHS:

Defines rule #9.

Referenced by [24], [33].

Overlap of [17] caaaab=daa with [9] bb=caaac:

Critical pair: caaaacaaac=daab.

Defines rule #10.

Referenced by [29], [30], [43], [45].

Overlap of [21] bac=ddaa with [22] caaacac=bddaa:

Critical pair: babddaa=ddaaaaacac.

Reduce RHS:

Referenced by [25].

Overlap of [24] babddaa=daacac with [12] daaa=1:

Critical pair: babd=daacaca.

Referenced by [26].

Overlap of [25] babd=daacaca with [12] daaa=1:

Critical pair: bab=daacacaaaa.

Defines rule #6.

Referenced by [27], [28], [40].

Overlap of [9] bb=caaac with [26] bab=daacacaaaa:

Critical pair: bdaacacaaaa=caaacab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [26] bab=daacacaaaa with [21] bac=ddaa:

Critical pair: baddaa=daacacaaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [23] caaaacaaac=daab with [17] caaaab=daa:

Critical pair: caaaacaaadaa=daabaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [39], [40].

Overlap of [23] caaaacaaac=daab with [23] caaaacaaac=daab:

Critical pair: caaaacaaadaab=daabaaaacaaac.

Reduce LHS:

Defines rule #16.

Overlap of [20] ad=da with [28] daacacaaaaac=bd:

Critical pair: abd=daaacacaaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

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

Overlap of [21] bac=ddaa with [31] cacaaaaac=abd:

Critical pair: baabd=ddaaacaaaaac.

Reduce RHS:

Referenced by [35].

Overlap of [31] cacaaaaac=abd with [22] caaacac=bddaa:

Critical pair: cacaaaaabddaa=abdaaacac.

Reduce RHS:

Referenced by [47].

Overlap of [31] cacaaaaac=abd with [31] cacaaaaac=abd:

Critical pair: cacaaaaaabd=abdacaaaaac.

Referenced by [51].

Overlap of [32] baabd=dcaaaaac with [12] daaa=1:

Critical pair: baab=dcaaaaacaaa.

Defines rule #7.

Referenced by [36], [37].

Overlap of [9] bb=caaac with [35] baab=dcaaaaacaaa:

Critical pair: bdcaaaaacaaa=caaacaab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [35] baab=dcaaaaacaaa with [21] bac=ddaa:

Critical pair: baaddaa=dcaaaaacaaaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [38].

Overlap of [20] ad=da with [37] dcaaaaacaaaac=bda:

Critical pair: abda=dacaaaaacaaaac.

Flip LHS and RHS.

Referenced by [42].

Overlap of [20] ad=da with [29] daabaaaab=caaaacaa:

Critical pair: acaaaacaa=daaabaaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [41].

Overlap of [29] daabaaaab=caaaacaa with [26] bab=daacacaaaa:

Critical pair: daabaaaadaacacaaaa=caaaacaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [17] caaaab=daa with [39] baaaab=acaaaacaa:

Critical pair: caaaaacaaaacaa=daaaaaab.

Reduce RHS:

Referenced by [43], [44], [45], [46].

Overlap of [20] ad=da with [38] dacaaaaacaaaac=abda:

Critical pair: aabda=daacaaaaacaaaac.

Flip LHS and RHS.

Referenced by [49].

Overlap of [23] caaaacaaac=daab with [41] caaaaacaaaacaa=aaab:

Critical pair: caaaacaaaaaab=daabaaaaacaaaacaa.

Defines rule #22.

Overlap of [31] cacaaaaac=abd with [41] caaaaacaaaacaa=aaab:

Critical pair: cacaaaaaaaab=abdaaaaacaaaacaa.

Reduce RHS:

Defines rule #24.

Overlap of [41] caaaaacaaaacaa=aaab with [23] caaaacaaac=daab:

Critical pair: caaaaacaaaadaab=aaabaacaaac.

Reduce LHS:

Defines rule #18.

Overlap of [41] caaaaacaaaacaa=aaab with [41] caaaaacaaaacaa=aaab:

Critical pair: caaaaacaaaaaaab=aaabaaacaaaacaa.

Defines rule #23.

Overlap of [33] cacaaaaabddaa=abcac with [12] daaa=1:

Critical pair: cacaaaaabd=abcaca.

Referenced by [48].

Overlap of [47] cacaaaaabd=abcaca with [12] daaa=1:

Critical pair: cacaaaaab=abcacaaaa.

Defines rule #19.

Overlap of [20] ad=da with [42] daacaaaaacaaaac=aabda:

Critical pair: aaabda=daaacaaaaacaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [50].

Overlap of [49] caaaaacaaaac=aaabda with [31] cacaaaaac=abd:

Critical pair: caaaaacaaaaabd=aaabdaacaaaaac.

Referenced by [52].

Overlap of [34] cacaaaaaabd=abdacaaaaac with [12] daaa=1:

Critical pair: cacaaaaaab=abdacaaaaacaaa.

Defines rule #21.

Overlap of [50] caaaaacaaaaabd=aaabdaacaaaaac with [12] daaa=1:

Critical pair: caaaaacaaaaab=aaabdaacaaaaacaaa.

Defines rule #20.