Certificate for #3298 ⟨a, b | abbbaabbbba=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. aa=c
  2. bbbbaabbb=d

Axiom: abbbaabbbba=1.

Referenced by [4].

Axiom: aa=c.

Defines rule #6.

Referenced by [3], [4], [5], [6], [19].

Axiom: bbbbaabbb=d.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [1] abbbaabbbba=1 with [2] aa=c:

Critical pair: abbbcbbbba=1.

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [16], [18].

Overlap of [4] abbbcbbbba=1 with [2] aa=c:

Critical pair: abbbcbbbbc=a.

Referenced by [8], [9].

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

Critical pair: abbbcbbbb=bbbcbbbba.

Flip LHS and RHS.

Referenced by [17].

Overlap of [4] abbbcbbbba=1 with [6] abbbcbbbbc=a:

Critical pair: abbbcbbbba=bbbcbbbbc.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [6] abbbcbbbbc=a with [8] bbbcbbbbc=1:

Critical pair: abbbcb=abbbbc.

Referenced by [16], [17].

Overlap of [8] bbbcbbbbc=1 with [8] bbbcbbbbc=1:

Critical pair: bbbcb=bbbbc.

Referenced by [11], [12], [13], [15], [16], [17], [18].

Overlap of [8] bbbcbbbbc=1 with [10] bbbcb=bbbbc:

Critical pair: bbbbcbbbc=1.

Reduce LHS:

Defines rule #2.

Referenced by [12], [13], [21], [29].

Overlap of [10] bbbcb=bbbbc with [10] bbbcb=bbbbc:

Critical pair: bbbcbbbbc=bbbbcbbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [10] bbbcb=bbbbc with [12] bbbbbbccb=1:

Critical pair: bbbc=bbbbcbbbbbccb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [14].

Overlap of [12] bbbbbbccb=1 with [13] bbcb=bbbc:

Critical pair: bbbbbbccbbbc=bcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20], [22], [23], [24], [25].

Simplify [3] d=bbbbcbbb.

Reduce RHS:

Defines rule #5.

Overlap of [4] abbbcbbbba=1 with [9] abbbcb=abbbbc:

Critical pair: abbbbcbbba=1.

Reduce LHS:

Referenced by [19].

Simplify [7] bbbcbbbba=abbbcbbbb.

Reduce RHS:

Referenced by [18].

Overlap of [17] bbbcbbbba=abbbbbbbc with [10] bbbcb=bbbbc:

Critical pair: bbbbcbbba=abbbbbbbc.

Reduce LHS:

Referenced by [19], [22].

Simplify [16] abbbbbbbac=1.

Reduce LHS:

Referenced by [20].

Overlap of [19] cbbbbbbbc=1 with [14] bcb=bbc:

Critical pair: cbbbbbbbbc=b.

Referenced by [21].

Overlap of [20] cbbbbbbbbc=b with [11] bbbbbbbcc=1:

Critical pair: cb=bc.

Defines rule #1.

Referenced by [22], [26], [27], [28].

Overlap of [18] bbbbbbbac=abbbbbbbc with [21] cb=bc:

Critical pair: bbbbbbbabc=abbbbbbbcb.

Reduce RHS:

Referenced by [23].

Overlap of [22] bbbbbbbabc=abbbbbbbbc with [14] bcb=bbc:

Critical pair: bbbbbbbabbc=abbbbbbbbcb.

Reduce RHS:

Referenced by [24].

Overlap of [23] bbbbbbbabbc=abbbbbbbbbc with [14] bcb=bbc:

Critical pair: bbbbbbbabbbc=abbbbbbbbbcb.

Reduce RHS:

Referenced by [25].

Overlap of [24] bbbbbbbabbbc=abbbbbbbbbbc with [14] bcb=bbc:

Critical pair: bbbbbbbabbbbc=abbbbbbbbbbcb.

Reduce RHS:

Referenced by [26].

Overlap of [25] bbbbbbbabbbbc=abbbbbbbbbbbc with [21] cb=bc:

Critical pair: bbbbbbbabbbbbc=abbbbbbbbbbbcb.

Reduce RHS:

Referenced by [27].

Overlap of [26] bbbbbbbabbbbbc=abbbbbbbbbbbbc with [21] cb=bc:

Critical pair: bbbbbbbabbbbbbc=abbbbbbbbbbbbcb.

Reduce RHS:

Referenced by [28].

Overlap of [27] bbbbbbbabbbbbbc=abbbbbbbbbbbbbc with [21] cb=bc:

Critical pair: bbbbbbbabbbbbbbc=abbbbbbbbbbbbbcb.

Reduce RHS:

Referenced by [29].

Overlap of [28] bbbbbbbabbbbbbbc=abbbbbbbbbbbbbbc with [11] bbbbbbbcc=1:

Critical pair: bbbbbbba=abbbbbbbbbbbbbbcc.

Reduce RHS:

Defines rule #4.