Certificate for #3102 ⟨a, b | aabbaaabbaa=1⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(c) = 0; deg(d) = 1; deg(b) = 2; deg(a) = 3
• Auxiliary generators:
  1. aaaa=c
  2. bbaaabb=d

Axiom: aabbaaabbaa=1.

Referenced by [4].

Axiom: aaaa=c.

Referenced by [5], [6], [9], [10], [11], [12], [13], [16], [17], [18], [19].

Axiom: bbaaabb=d.

Referenced by [4], [15], [18], [24].

Overlap of [1] aabbaaabbaa=1 with [3] bbaaabb=d:

Critical pair: aadaa=1.

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Referenced by [10], [12], [23], [24].

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

Critical pair: aadc=aa.

Referenced by [9], [10].

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

Critical pair: aad=daa.

Flip LHS and RHS.

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

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

Critical pair: aada=adaa.

Reduce RHS:

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

Overlap of [4] aadaa=1 with [6] aadc=aa:

Critical pair: aadaa=dc.

Reduce LHS:

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

Overlap of [4] aadaa=1 with [6] aadc=aa:

Critical pair: aadaaa=adc.

Reduce LHS:

Referenced by [12].

Overlap of [7] daa=aad with [4] aadaa=1:

Critical pair: d=aaddaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12].

Overlap of [7] daa=aad with [4] aadaa=1:

Critical pair: da=aadadaa.

Reduce RHS:

Referenced by [15], [16], [18].

Overlap of [4] aadaa=1 with [8] aada=aaad:

Critical pair: aaada=1.

Reduce LHS:

Defines rule #1.

Referenced by [14], [20], [25], [26], [27], [28], [29], [31], [39], [40], [41], [42], [43], [44].

Simplify [9] cd=dc.

Reduce RHS:

Defines rule #2.

Referenced by [16], [17], [21], [23], [32], [33], [34], [35], [36], [37], [38].

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

Critical pair: bbaaad=daaabb.

Reduce RHS:

Referenced by [16].

Overlap of [15] bbaaad=aaadbb with [12] da=ad:

Critical pair: bbaaaad=aaadbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [2] aaaa=c with [16] aaadbba=bb:

Critical pair: abb=cdbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [18], [19], [24].

Overlap of [3] bbaaabb=d with [17] bba=abb:

Critical pair: bbaaaabb=da.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [17] bba=abb with [2] aaaa=c:

Critical pair: bbc=abbaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [13] dc=1 with [19] cbb=bbc:

Critical pair: dbbc=bb.

Referenced by [21].

Overlap of [20] dbbc=bb with [14] cd=1:

Critical pair: dbb=bbd.

Referenced by [25], [26], [27], [28], [29], [31].

Simplify [18] ad=cbbbb.

Reduce RHS:

Referenced by [23].

Overlap of [5] ca=ac with [22] ad=bbbbc:

Critical pair: cbbbbc=acd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [24].

Overlap of [3] bbaaabb=d with [17] bba=abb:

Critical pair: abbaabb=d.

Reduce LHS:

Referenced by [25].

Overlap of [21] dbb=bbd with [24] bbbbbbbbbbbbbbbbcccccc=d:

Critical pair: dd=bbdbbbbbbbbbbbbbbcccccc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [21] dbb=bbd with [25] bbbbbbbbbbbbbbbbccccc=dd:

Critical pair: ddd=bbdbbbbbbbbbbbbbbccccc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [21] dbb=bbd with [26] bbbbbbbbbbbbbbbbcccc=ddd:

Critical pair: dddd=bbdbbbbbbbbbbbbbbcccc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [21] dbb=bbd with [27] bbbbbbbbbbbbbbbbccc=dddd:

Critical pair: ddddd=bbdbbbbbbbbbbbbbbccc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [21] dbb=bbd with [28] bbbbbbbbbbbbbbbbcc=ddddd:

Critical pair: dddddd=bbdbbbbbbbbbbbbbbcc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [30], [31].

Overlap of [19] cbb=bbc with [29] bbbbbbbbbbbbbbbbc=dddddd:

Critical pair: cbdddddd=bbcbbbbbbbbbbbbbbbc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [21] dbb=bbd with [29] bbbbbbbbbbbbbbbbc=dddddd:

Critical pair: ddddddd=bbdbbbbbbbbbbbbbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [14] cd=1 with [30] ddddddbc=cbdddddd:

Critical pair: ccbdddddd=dddddbc.

Flip LHS and RHS.

Referenced by [33].

Overlap of [14] cd=1 with [32] dddddbc=ccbdddddd:

Critical pair: cccbdddddd=ddddbc.

Flip LHS and RHS.

Referenced by [34].

Overlap of [14] cd=1 with [33] ddddbc=cccbdddddd:

Critical pair: ccccbdddddd=dddbc.

Flip LHS and RHS.

Referenced by [35].

Overlap of [14] cd=1 with [34] dddbc=ccccbdddddd:

Critical pair: cccccbdddddd=ddbc.

Flip LHS and RHS.

Referenced by [36].

Overlap of [14] cd=1 with [35] ddbc=cccccbdddddd:

Critical pair: ccccccbdddddd=dbc.

Flip LHS and RHS.

Referenced by [37], [38].

Overlap of [14] cd=1 with [36] dbc=ccccccbdddddd:

Critical pair: cccccccbdddddd=bc.

Referenced by [39].

Overlap of [36] dbc=ccccccbdddddd with [14] cd=1:

Critical pair: db=ccccccbddddddd.

Defines rule #4.

Overlap of [37] cccccccbdddddd=bc with [13] dc=1:

Critical pair: cccccccbddddd=bcc.

Referenced by [40].

Overlap of [39] cccccccbddddd=bcc with [13] dc=1:

Critical pair: cccccccbdddd=bccc.

Referenced by [41].

Overlap of [40] cccccccbdddd=bccc with [13] dc=1:

Critical pair: cccccccbddd=bcccc.

Referenced by [42].

Overlap of [41] cccccccbddd=bcccc with [13] dc=1:

Critical pair: cccccccbdd=bccccc.

Referenced by [43].

Overlap of [42] cccccccbdd=bccccc with [13] dc=1:

Critical pair: cccccccbd=bcccccc.

Referenced by [44].

Overlap of [43] cccccccbd=bcccccc with [13] dc=1:

Critical pair: cccccccb=bccccccc.

Defines rule #3.