Certificate for #10660 ⟨a, b | aaaa=bab, bbbb=1⟩

Completion settings:

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

Axiom: aaaa=bab.

Flip LHS and RHS.

Defines rule #14.

Referenced by [8], [9], [10], [11], [12], [27], [39].

Axiom: bbbb=1.

Referenced by [5].

Axiom: bbb=c.

Defines rule #21.

Referenced by [5], [6], [7], [9], [11], [16], [21], [25].

Axiom: caaacaaacaaac=d.

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

Overlap of [2] bbbb=1 with [3] bbb=c:

Critical pair: cb=1.

Defines rule #19.

Referenced by [6], [7], [12], [15], [27].

Overlap of [3] bbb=c with [3] bbb=c:

Critical pair: bc=cb.

Reduce RHS:

Defines rule #18.

Referenced by [10], [16], [26].

Overlap of [5] cb=1 with [3] bbb=c:

Critical pair: cc=bb.

Defines rule #20.

Overlap of [1] bab=aaaa with [1] bab=aaaa:

Critical pair: baaaaa=aaaaab.

Flip LHS and RHS.

Defines rule #5.

Referenced by [13].

Overlap of [1] bab=aaaa with [3] bbb=c:

Critical pair: bac=aaaabb.

Referenced by [32].

Overlap of [1] bab=aaaa with [6] bc=1:

Critical pair: ba=aaaac.

Flip LHS and RHS.

Referenced by [16], [22].

Overlap of [3] bbb=c with [1] bab=aaaa:

Critical pair: bbaaaa=cab.

Flip LHS and RHS.

Referenced by [13].

Overlap of [5] cb=1 with [1] bab=aaaa:

Critical pair: caaaa=ab.

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

Overlap of [12] caaaa=ab with [8] aaaaab=baaaaa:

Critical pair: cabaaaaa=abaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [4] caaacaaacaaac=d with [4] caaacaaacaaac=d:

Critical pair: caaad=daaac.

Flip LHS and RHS.

Referenced by [20].

Overlap of [4] caaacaaacaaac=d with [5] cb=1:

Critical pair: caaacaaacaaa=db.

Referenced by [21].

Overlap of [10] aaaac=ba with [4] caaacaaacaaac=d:

Critical pair: aaaad=baaaacaaacaaac.

Reduce RHS:

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

Overlap of [12] caaaa=ab with [16] aaaad=a:

Critical pair: ca=abd.

Defines rule #10.

Referenced by [18], [19], [20], [21], [28], [30].

Overlap of [12] caaaa=ab with [17] ca=abd:

Critical pair: abdaaa=ab.

Defines rule #4.

Referenced by [19], [21], [25].

Overlap of [12] caaaa=ab with [18] abdaaa=ab:

Critical pair: caaaab=abbdaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [21], [25].

Simplify [14] daaac=caaad.

Reduce RHS:

Referenced by [33].

Overlap of [15] caaacaaacaaa=db with [17] ca=abd:

Critical pair: abdaacaaacaaa=db.

Reduce LHS:

Referenced by [22], [23], [24], [26].

Overlap of [10] aaaac=ba with [21] acdaa=db:

Critical pair: aaadb=badaa.

Referenced by [35].

Overlap of [21] acdaa=db with [16] aaaad=a:

Critical pair: acda=dbaad.

Referenced by [24], [25].

Overlap of [21] acdaa=db with [23] acda=dbaad:

Critical pair: dbaada=db.

Referenced by [25], [37].

Overlap of [18] abdaaa=ab with [19] abbdaaa=abb:

Critical pair: abdaaabb=abbbdaaa.

Reduce LHS:

Reduce RHS:

Referenced by [26], [27], [28], [32], [34], [38].

Overlap of [21] acdaa=db with [25] ac=dba:

Critical pair: acdadba=dbc.

Reduce LHS:

Reduce RHS:

Referenced by [39].

Overlap of [25] ac=dba with [5] cb=1:

Critical pair: a=dbab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [29], [39].

Overlap of [25] ac=dba with [17] ca=abd:

Critical pair: aabd=dbaa.

Flip LHS and RHS.

Referenced by [37].

Overlap of [27] daaaa=a with [16] aaaad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #2.

Referenced by [30], [31], [33], [34], [35], [36], [39], [41], [43], [44].

Overlap of [17] ca=abd with [29] ad=da:

Critical pair: cda=abdd.

Referenced by [31].

Overlap of [30] cda=abdd with [29] ad=da:

Critical pair: cdda=abddd.

Referenced by [42].

Overlap of [9] bac=aaaabb with [25] ac=dba:

Critical pair: bdba=aaaabb.

Flip LHS and RHS.

Referenced by [45].

Simplify [20] daaac=abdaad.

Reduce RHS:

Referenced by [34].

Overlap of [33] daaac=abddaa with [25] ac=dba:

Critical pair: daadba=abddaa.

Reduce LHS:

Referenced by [39].

Simplify [22] aaadb=badaa.

Reduce RHS:

Referenced by [36].

Overlap of [35] aaadb=bdaaa with [29] ad=da:

Critical pair: aadab=bdaaa.

Reduce LHS:

Defines rule #9.

Overlap of [24] dbaada=db with [28] dbaa=aabd:

Critical pair: aabdda=db.

Flip LHS and RHS.

Defines rule #6.

Referenced by [38], [41], [45].

Simplify [25] ac=dba.

Reduce RHS:

Defines rule #12.

Referenced by [40].

Overlap of [26] dbadadba=d with [29] ad=da:

Critical pair: dbdaadba=d.

Reduce LHS:

Defines rule #3.

Referenced by [40], [42], [43].

Overlap of [39] ddaaa=d with [38] ac=aabddaa:

Critical pair: ddaaaabddaa=dc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [43].

Overlap of [29] ad=da with [37] db=aabdda:

Critical pair: aaabdda=dab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [43], [44].

Overlap of [31] cdda=abddd with [39] ddaaa=d:

Critical pair: cd=abdddaa.

Defines rule #11.

Simplify [40] dc=dabddaa.

Reduce RHS:

Defines rule #13.

Overlap of [29] ad=da with [41] dab=aaabdda:

Critical pair: aaaabdda=daab.

Flip LHS and RHS.

Defines rule #8.

Simplify [32] aaaabb=bdba.

Reduce RHS:

Defines rule #17.