Certificate for #2811 ⟨a, b | aaaaabaaaba=1⟩

Completion settings:

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

Axiom: aaaaabaaaba=1.

Referenced by [4].

Axiom: aaaaaa=c.

Referenced by [6], [7], [8], [17].

Axiom: baaab=d.

Referenced by [4], [5], [16], [18], [21].

Overlap of [1] aaaaabaaaba=1 with [3] baaab=d:

Critical pair: aaaaada=1.

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

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

Critical pair: baaad=daaab.

Flip LHS and RHS.

Referenced by [11], [19], [29], [33].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [27], [29], [31], [33], [37].

Overlap of [2] aaaaaa=c with [4] aaaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [10], [11].

Overlap of [4] aaaaada=1 with [2] aaaaaa=c:

Critical pair: aaaaadc=aaaaa.

Referenced by [12].

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

Critical pair: aaaaad=aaaada.

Flip LHS and RHS.

Referenced by [14].

Overlap of [7] cda=a with [4] aaaaada=1:

Critical pair: cd=aaaaada.

Reduce RHS:

Referenced by [16], [29], [33], [34].

Overlap of [7] cda=a with [5] daaab=baaad:

Critical pair: cbaaad=aaab.

Referenced by [14], [15].

Overlap of [4] aaaaada=1 with [8] aaaaadc=aaaaa:

Critical pair: aaaaadaaaaa=aaaadc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [4] aaaaada=1 with [12] aaaadc=aaaa:

Critical pair: aaaaadaaaa=aaadc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [12] aaaadc=aaaa with [11] cbaaad=aaab:

Critical pair: aaaadaaab=aaaabaaad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [11] cbaaad=aaab with [13] aaadc=aaa:

Critical pair: cbaaa=aaabc.

Referenced by [16], [20], [21], [29], [31], [33].

Overlap of [15] cbaaa=aaabc with [3] baaab=d:

Critical pair: cd=aaabcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [18], [19], [20], [21], [23], [28], [30].

Overlap of [2] aaaaaa=c with [16] aaabcb=1:

Critical pair: aaa=cbcb.

Referenced by [19], [20], [21], [23], [26].

Overlap of [3] baaab=d with [16] aaabcb=1:

Critical pair: b=dcb.

Flip LHS and RHS.

Referenced by [19], [22].

Overlap of [5] daaab=baaad with [16] aaabcb=1:

Critical pair: d=baaadcb.

Reduce RHS:

Referenced by [21], [22], [25].

Overlap of [15] cbaaa=aaabc with [16] aaabcb=1:

Critical pair: cb=aaabcbcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [16] aaabcb=1 with [15] cbaaa=aaabc:

Critical pair: aaabaaabc=aaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [22], [23], [25], [26].

Simplify [18] dcb=b.

Reduce LHS:

Referenced by [23], [24], [32].

Overlap of [16] aaabcb=1 with [22] bcbbcbbc=b:

Critical pair: aaab=bcbbc.

Reduce LHS:

Referenced by [28], [30].

Overlap of [22] bcbbcbbc=b with [22] bcbbcbbc=b:

Critical pair: bcbb=bbbc.

Referenced by [25], [28], [29], [30], [31], [32], [33], [35].

Simplify [19] d=bcbcbb.

Reduce RHS:

Referenced by [29], [33], [34], [37], [39].

Simplify [17] aaa=cbcb.

Reduce RHS:

Referenced by [27], [28], [29], [30], [31], [33], [37], [38].

Overlap of [6] ca=ac with [26] aaa=cbbc:

Critical pair: ccbbc=acaa.

Reduce RHS:

Referenced by [32].

Overlap of [16] aaabcb=1 with [26] aaa=cbbc:

Critical pair: cbbcbcb=1.

Reduce LHS:

Referenced by [29], [30], [31], [32], [36], [37].

Overlap of [5] daaab=baaad with [28] bbbcccb=1:

Critical pair: daaa=baaadbbcccb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [16] aaabcb=1 with [28] bbbcccb=1:

Critical pair: aaabc=bbcccb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [28] bbbcccb=1 with [15] cbaaa=aaabc:

Critical pair: bbbccaaabc=aaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [28] bbbcccb=1 with [22] bcbbcbbc=b:

Critical pair: bbbcccb=cbbcbbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [33], [34], [35], [40].

Overlap of [5] daaab=baaad with [32] bbbbccc=1:

Critical pair: daaa=baaadbbbccc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [32] bbbbccc=1 with [10] cd=1:

Critical pair: bbbbcc=d.

Reduce RHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [24] bcbb=bbbc with [32] bbbbccc=1:

Critical pair: bcb=bbbcbbbccc.

Reduce RHS:

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

Overlap of [28] bbbcccb=1 with [35] bcb=bbc:

Critical pair: bbbcccbbc=cb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

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

Overlap of [14] aaaabaaad=ab with [26] aaa=cbbc:

Critical pair: cbbcabaaad=ab.

Reduce LHS:

Referenced by [40].

Simplify [26] aaa=cbbc.

Reduce RHS:

Defines rule #6.

Simplify [25] d=bbbccb.

Reduce RHS:

Defines rule #5.

Overlap of [37] bbabbbccc=ab with [36] cb=bc:

Critical pair: bbabbbccbc=abb.

Reduce LHS:

Defines rule #4.