Certificate for #1356 ⟨a, b | aaabababba=1⟩

Completion settings:

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

Axiom: aaabababba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [12], [16], [17], [21], [25], [28], [31].

Axiom: bababb=d.

Defines rule #15.

Referenced by [4], [9], [17], [19].

Overlap of [1] aaabababba=1 with [3] bababb=d:

Critical pair: aaada=1.

Referenced by [6], [7], [8], [10], [11], [12].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [18], [21], [22], [27], [32], [33].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aaad=aada.

Flip LHS and RHS.

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

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

Critical pair: cd=aaada.

Reduce RHS:

Defines rule #2.

Referenced by [16], [23], [25], [28], [31].

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

Critical pair: bababd=dababb.

Referenced by [13].

Overlap of [4] aaada=1 with [7] aada=aaad:

Critical pair: aaadaaad=ada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

Overlap of [7] aada=aaad with [7] aada=aaad:

Critical pair: aadaaad=aaadada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [12], [13], [14], [24], [26], [28], [30].

Overlap of [11] da=ad with [2] aaaa=c:

Critical pair: dc=adaaa.

Reduce RHS:

Defines rule #1.

Referenced by [15], [17], [20], [29].

Simplify [9] bababd=dababb.

Reduce RHS:

Defines rule #9.

Referenced by [14], [15].

Overlap of [13] bababd=adbabb with [11] da=ad:

Critical pair: bababad=adbabba.

Defines rule #11.

Referenced by [26].

Overlap of [13] bababd=adbabb with [12] dc=1:

Critical pair: babab=adbabbc.

Flip LHS and RHS.

Referenced by [16].

Overlap of [2] aaaa=c with [15] adbabbc=babab:

Critical pair: aaababab=cdbabbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [17], [18], [22].

Overlap of [3] bababb=d with [16] babbc=aaababab:

Critical pair: baaaababab=dc.

Reduce LHS:

Reduce RHS:

Referenced by [19].

Overlap of [16] babbc=aaababab with [5] ca=ac:

Critical pair: babbac=aaabababa.

Defines rule #10.

Referenced by [27].

Overlap of [17] bcbabab=1 with [3] bababb=d:

Critical pair: bcbad=abb.

Referenced by [20].

Overlap of [19] bcbad=abb with [12] dc=1:

Critical pair: bcba=abbc.

Defines rule #6.

Referenced by [21], [22].

Overlap of [20] bcba=abbc with [2] aaaa=c:

Critical pair: bcbc=abbcaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [23].

Overlap of [20] bcba=abbc with [16] babbc=aaababab:

Critical pair: bcaaababab=abbcbbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [21] abbaaac=bcbc with [8] cd=1:

Critical pair: abbaaa=bcbcd.

Reduce RHS:

Referenced by [24].

Overlap of [11] da=ad with [23] abbaaa=bcb:

Critical pair: dbcb=adbbaaa.

Flip LHS and RHS.

Referenced by [25].

Overlap of [2] aaaa=c with [24] adbbaaa=dbcb:

Critical pair: aaadbcb=cdbbaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [28].

Overlap of [14] bababad=adbabba with [11] da=ad:

Critical pair: bababaad=adbabbaa.

Defines rule #13.

Referenced by [28].

Overlap of [18] babbac=aaabababa with [5] ca=ac:

Critical pair: babbaac=aaabababaa.

Defines rule #12.

Overlap of [26] bababaad=adbabbaa with [11] da=ad:

Critical pair: bababaaad=adbabbaaa.

Reduce RHS:

Referenced by [29].

Overlap of [28] bababaaad=adbbcb with [12] dc=1:

Critical pair: bababaaa=adbbcbc.

Defines rule #14.

Overlap of [11] da=ad with [22] abbcbbc=baaacbabab:

Critical pair: dbaaacbabab=adbbcbbc.

Flip LHS and RHS.

Referenced by [31].

Overlap of [2] aaaa=c with [30] adbbcbbc=dbaaacbabab:

Critical pair: aaadbaaacbabab=cdbbcbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [32].

Overlap of [31] bbcbbc=aaadbaaacbabab with [5] ca=ac:

Critical pair: bbcbbac=aaadbaaacbababa.

Defines rule #17.

Referenced by [33].

Overlap of [32] bbcbbac=aaadbaaacbababa with [5] ca=ac:

Critical pair: bbcbbaac=aaadbaaacbababaa.

Defines rule #18.