Certificate for #3227 ⟨a, b | ababaaaaaab=1⟩

Completion settings:

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

Axiom: ababaaaaaab=1.

Referenced by [4].

Axiom: aaaaaa=c.

Defines rule #2.

Referenced by [4], [11], [12], [18], [27], [28], [32], [37], [44].

Axiom: babab=d.

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

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

Critical pair: ababcb=1.

Referenced by [6], [7], [12], [14].

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

Critical pair: bad=dab.

Referenced by [9], [10].

Overlap of [3] babab=d with [4] ababcb=1:

Critical pair: b=dcb.

Flip LHS and RHS.

Referenced by [8], [9], [16].

Overlap of [4] ababcb=1 with [3] babab=d:

Critical pair: ababcd=abab.

Referenced by [13].

Overlap of [6] dcb=b with [3] babab=d:

Critical pair: dcd=babab.

Reduce RHS:

Referenced by [10], [15].

Overlap of [5] bad=dab with [6] dcb=b:

Critical pair: bab=dabcb.

Referenced by [12], [13], [14], [16], [17].

Overlap of [5] bad=dab with [8] dcd=d:

Critical pair: bad=dabcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16], [17], [19].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #1.

Referenced by [23], [31], [44].

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

Critical pair: aaaaa=cbabcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15], [16].

Simplify [7] ababcd=abab.

Reduce LHS:

Reduce RHS:

Referenced by [17], [19].

Overlap of [4] ababcb=1 with [9] bab=dabcb:

Critical pair: adabcbcb=1.

Referenced by [16], [17], [19], [20].

Overlap of [8] dcd=d with [12] cdabcbcb=aaaaa:

Critical pair: daaaaa=dabcbcb.

Flip LHS and RHS.

Referenced by [20], [22].

Overlap of [10] dabcd=dab with [12] cdabcbcb=aaaaa:

Critical pair: dabaaaaa=dababcbcb.

Reduce RHS:

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

Overlap of [13] adabcbcd=adabcb with [16] dabaaaaa=b:

Critical pair: adabcbcb=adabcbabaaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [20], [21], [24].

Overlap of [16] dabaaaaa=b with [2] aaaaaa=c:

Critical pair: dabc=ba.

Flip LHS and RHS.

Referenced by [19], [23], [36].

Overlap of [14] adabcbcb=1 with [18] ba=dabc:

Critical pair: adabcbcdabc=a.

Reduce LHS:

Referenced by [21].

Overlap of [17] adaaaaa=1 with [14] adabcbcb=1:

Critical pair: adaaaa=dabcbcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [22], [24].

Overlap of [17] adaaaaa=1 with [19] adc=a:

Critical pair: adaaaaa=dc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [27], [33].

Simplify [15] dabcbcb=daaaaa.

Reduce RHS:

Referenced by [34].

Overlap of [16] dabaaaaa=b with [18] ba=dabc:

Critical pair: dadabcaaaa=b.

Reduce LHS:

Referenced by [37].

Overlap of [17] adaaaaa=1 with [20] daaaaa=adaaaa:

Critical pair: aadaaaa=1.

Referenced by [25], [26].

Overlap of [24] aadaaaa=1 with [24] aadaaaa=1:

Critical pair: aadaa=daaaa.

Flip LHS and RHS.

Referenced by [26], [27], [29], [30].

Overlap of [24] aadaaaa=1 with [24] aadaaaa=1:

Critical pair: aadaaa=adaaaa.

Reduce RHS:

Referenced by [27], [30], [34].

Overlap of [25] daaaa=aadaa with [2] aaaaaa=c:

Critical pair: dc=aadaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [28], [29], [30].

Overlap of [2] aaaaaa=c with [27] aaaadaa=1:

Critical pair: aa=cdaa.

Flip LHS and RHS.

Referenced by [31].

Overlap of [25] daaaa=aadaa with [27] aaaadaa=1:

Critical pair: d=aadaadaa.

Flip LHS and RHS.

Referenced by [30].

Overlap of [25] daaaa=aadaa with [27] aaaadaa=1:

Critical pair: da=aadaaadaa.

Reduce RHS:

Defines rule #5.

Referenced by [31], [34], [35], [36], [37].

Simplify [28] cdaa=aa.

Reduce LHS:

Referenced by [32].

Overlap of [2] aaaaaa=c with [31] aacd=aa:

Critical pair: aaaaaa=ccd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [21] dc=1 with [32] ccd=c:

Critical pair: dc=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [37], [38], [39], [40], [41], [42], [43], [44].

Simplify [22] dabcbcb=adaaaa.

Reduce RHS:

Referenced by [35].

Overlap of [34] dabcbcb=aaaaad with [30] da=ad:

Critical pair: adbcbcb=aaaaad.

Referenced by [44].

Simplify [18] ba=dabc.

Reduce RHS:

Defines rule #6.

Overlap of [23] dadadadadadabccccc=b with [30] da=ad:

Critical pair: addadadadadabccccc=b.

Reduce LHS:

Referenced by [38], [39].

Overlap of [33] cd=1 with [37] dddddbccccc=b:

Critical pair: cb=ddddbccccc.

Flip LHS and RHS.

Referenced by [40].

Overlap of [37] dddddbccccc=b with [33] cd=1:

Critical pair: dddddbcccc=bd.

Flip LHS and RHS.

Defines rule #8.

Overlap of [33] cd=1 with [38] ddddbccccc=cb:

Critical pair: ccb=dddbccccc.

Flip LHS and RHS.

Referenced by [41].

Overlap of [33] cd=1 with [40] dddbccccc=ccb:

Critical pair: cccb=ddbccccc.

Flip LHS and RHS.

Referenced by [42].

Overlap of [33] cd=1 with [41] ddbccccc=cccb:

Critical pair: ccccb=dbccccc.

Flip LHS and RHS.

Referenced by [43].

Overlap of [33] cd=1 with [42] dbccccc=ccccb:

Critical pair: cccccb=bccccc.

Flip LHS and RHS.

Defines rule #7.

Overlap of [2] aaaaaa=c with [35] adbcbcb=aaaaad:

Critical pair: aaaaaaaaaad=cdbcbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.