Certificate for #678 ⟨a, b | aabbaaabb=1⟩

Completion settings:

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

Axiom: aabbaaabb=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #9.

Referenced by [4], [5], [6], [10], [14], [22], [30].

Axiom: bbaabb=d.

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

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

Critical pair: aabbcbb=1.

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [18], [29].

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

Critical pair: a=cbbcbb.

Flip LHS and RHS.

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

Overlap of [3] bbaabb=d with [4] aabbcbb=1:

Critical pair: bb=dcbb.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [4] aabbcbb=1 with [3] bbaabb=d:

Critical pair: aabbcbd=baabb.

Flip LHS and RHS.

Referenced by [29].

Overlap of [7] dcbb=bb with [6] cbbcbb=a:

Critical pair: da=bbcbb.

Flip LHS and RHS.

Referenced by [10], [11], [13], [20].

Overlap of [9] bbcbb=da with [3] bbaabb=d:

Critical pair: bbcd=daaabb.

Reduce RHS:

Referenced by [12].

Overlap of [9] bbcbb=da with [6] cbbcbb=a:

Critical pair: bba=dacbb.

Referenced by [21].

Overlap of [6] cbbcbb=a with [10] bbcd=bb:

Critical pair: cbbcbb=acd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15], [19].

Overlap of [4] aabbcbb=1 with [9] bbcbb=da:

Critical pair: aada=1.

Referenced by [14], [15], [16], [17].

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

Critical pair: aadc=aa.

Referenced by [16].

Overlap of [13] aada=1 with [12] acd=a:

Critical pair: aada=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [25], [30], [31], [32], [33], [34], [35], [36], [38], [39], [40].

Overlap of [13] aada=1 with [14] aadc=aa:

Critical pair: aadaa=adc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [21].

Overlap of [13] aada=1 with [16] adc=a:

Critical pair: aada=dc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [18], [23], [27], [28], [30], [37], [41].

Overlap of [17] dc=1 with [5] ca=ac:

Critical pair: dac=a.

Referenced by [19].

Overlap of [18] dac=a with [12] acd=a:

Critical pair: da=ad.

Defines rule #4.

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

Simplify [9] bbcbb=da.

Reduce RHS:

Referenced by [24].

Simplify [11] bba=dacbb.

Reduce RHS:

Referenced by [22], [30].

Overlap of [21] bba=abb with [2] aaa=c:

Critical pair: bbc=abbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [23], [29].

Overlap of [17] dc=1 with [22] cbb=bbc:

Critical pair: dbbc=bb.

Referenced by [24], [25].

Overlap of [23] dbbc=bb with [20] bbcbb=ad:

Critical pair: dad=bbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [26], [30].

Overlap of [23] dbbc=bb with [15] cd=1:

Critical pair: dbb=bbd.

Referenced by [29].

Overlap of [24] bbbb=add with [24] bbbb=add:

Critical pair: badd=addb.

Referenced by [27].

Overlap of [26] badd=addb with [17] dc=1:

Critical pair: bad=addbc.

Referenced by [28].

Overlap of [27] bad=addbc with [17] dc=1:

Critical pair: ba=addbcc.

Referenced by [29], [41].

Simplify [8] baabb=aabbcbd.

Reduce LHS:

Referenced by [30].

Overlap of [21] bba=abb with [29] aabbddddbcccc=aabbcbd:

Critical pair: bbaabbcbd=abbabbddddbcccc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [15] cd=1 with [30] dddddbcccc=bd:

Critical pair: cbd=ddddbcccc.

Flip LHS and RHS.

Referenced by [32].

Overlap of [15] cd=1 with [31] ddddbcccc=cbd:

Critical pair: ccbd=dddbcccc.

Flip LHS and RHS.

Referenced by [33].

Overlap of [15] cd=1 with [32] dddbcccc=ccbd:

Critical pair: cccbd=ddbcccc.

Flip LHS and RHS.

Referenced by [34].

Overlap of [15] cd=1 with [33] ddbcccc=cccbd:

Critical pair: ccccbd=dbcccc.

Flip LHS and RHS.

Referenced by [35], [36].

Overlap of [15] cd=1 with [34] dbcccc=ccccbd:

Critical pair: cccccbd=bcccc.

Referenced by [37].

Overlap of [34] dbcccc=ccccbd with [15] cd=1:

Critical pair: dbccc=ccccbdd.

Referenced by [38].

Overlap of [35] cccccbd=bcccc with [17] dc=1:

Critical pair: cccccb=bccccc.

Defines rule #5.

Overlap of [36] dbccc=ccccbdd with [15] cd=1:

Critical pair: dbcc=ccccbddd.

Referenced by [39].

Overlap of [38] dbcc=ccccbddd with [15] cd=1:

Critical pair: dbc=ccccbdddd.

Referenced by [40].

Overlap of [39] dbc=ccccbdddd with [15] cd=1:

Critical pair: db=ccccbddddd.

Defines rule #6.

Referenced by [41].

Simplify [28] ba=addbcc.

Reduce RHS:

Defines rule #7.