Certificate for #3094 ⟨a, b | aababbbbbba=1⟩

Completion settings:

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

Axiom: aababbbbbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [14], [18].

Axiom: babbbbbb=d.

Defines rule #17.

Referenced by [4], [11], [15], [17].

Overlap of [1] aababbbbbba=1 with [3] babbbbbb=d:

Critical pair: aada=1.

Referenced by [6], [7], [8], [9], [10].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [16], [25].

Overlap of [2] aaa=c with [4] aada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aad=ada.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [6] cda=a with [4] aada=1:

Critical pair: cd=aada.

Reduce RHS:

Defines rule #2.

Referenced by [14], [18], [20], [21], [22], [23], [24], [28].

Overlap of [4] aada=1 with [7] ada=aad:

Critical pair: aadaad=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [10], [11], [12], [18].

Overlap of [9] da=ad with [2] aaa=c:

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [19], [26].

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

Critical pair: babbbbbd=dabbbbbb.

Reduce RHS:

Defines rule #12.

Referenced by [12], [13].

Overlap of [11] babbbbbd=adbbbbbb with [9] da=ad:

Critical pair: babbbbbad=adbbbbbba.

Defines rule #14.

Overlap of [11] babbbbbd=adbbbbbb with [10] dc=1:

Critical pair: babbbbb=adbbbbbbc.

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] aaa=c with [13] adbbbbbbc=babbbbb:

Critical pair: aababbbbb=cdbbbbbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [15], [16].

Overlap of [3] babbbbbb=d with [14] bbbbbbc=aababbbbb:

Critical pair: babaababbbbb=dbc.

Referenced by [17].

Overlap of [14] bbbbbbc=aababbbbb with [5] ca=ac:

Critical pair: bbbbbbac=aababbbbba.

Defines rule #13.

Referenced by [25].

Overlap of [15] babaababbbbb=dbc with [3] babbbbbb=d:

Critical pair: babaad=dbcb.

Referenced by [18], [19].

Overlap of [17] babaad=dbcb with [9] da=ad:

Critical pair: babaaad=dbcba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20], [21], [22], [23].

Overlap of [17] babaad=dbcb with [10] dc=1:

Critical pair: babaa=dbcbc.

Defines rule #7.

Referenced by [21].

Overlap of [8] cd=1 with [18] dbcba=bab:

Critical pair: cbab=bcba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [24].

Overlap of [18] dbcba=bab with [19] babaa=dbcbc:

Critical pair: dbcdbcbc=babbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [22].

Overlap of [18] dbcba=bab with [21] babbaa=dbbcbc:

Critical pair: dbcdbbcbc=babbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [23].

Overlap of [18] dbcba=bab with [22] babbbaa=dbbbcbc:

Critical pair: dbcdbbbcbc=babbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [24].

Overlap of [20] bcba=cbab with [23] babbbbaa=dbbbbcbc:

Critical pair: bcdbbbbcbc=cbabbbbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [16] bbbbbbac=aababbbbba with [5] ca=ac:

Critical pair: bbbbbbaac=aababbbbbaa.

Referenced by [27].

Overlap of [10] dc=1 with [24] cbabbbbbaa=bbbbbcbc:

Critical pair: dbbbbbcbc=babbbbbaa.

Flip LHS and RHS.

Defines rule #16.

Referenced by [27].

Simplify [25] bbbbbbaac=aababbbbbaa.

Reduce RHS:

Referenced by [28].

Overlap of [27] bbbbbbaac=aadbbbbbcbc with [8] cd=1:

Critical pair: bbbbbbaa=aadbbbbbcbcd.

Reduce RHS:

Defines rule #15.