Certificate for #3643 ⟨a, b | aabbabaaab=a⟩

Completion settings:

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

Axiom: aabbabaaab=a.

Referenced by [4].

Axiom: baba=c.

Defines rule #26.

Referenced by [4], [5], [6], [9], [13].

Axiom: caa=d.

Referenced by [4], [7], [8], [10], [16], [20].

Overlap of [1] aabbabaaab=a with [2] baba=c:

Critical pair: aabcaab=a.

Reduce LHS:

Referenced by [6], [7], [8], [9], [12], [17], [21].

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

Critical pair: bac=cba.

Flip LHS and RHS.

Defines rule #20.

Referenced by [26], [33], [39].

Overlap of [2] baba=c with [4] aabdb=a:

Critical pair: baba=cabdb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [3] caa=d with [4] aabdb=a:

Critical pair: ca=dbdb.

Referenced by [8], [10], [11], [13], [16], [18], [20], [23].

Overlap of [3] caa=d with [4] aabdb=a:

Critical pair: caa=dabdb.

Reduce LHS:

Referenced by [10], [16].

Overlap of [4] aabdb=a with [2] baba=c:

Critical pair: aabdc=aaba.

Flip LHS and RHS.

Referenced by [16].

Overlap of [3] caa=d with [7] ca=dbdb:

Critical pair: dbdba=d.

Reduce LHS:

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

Simplify [6] cabdb=c.

Reduce LHS:

Referenced by [12], [13], [14], [15], [18], [22].

Overlap of [4] aabdb=a with [11] dbdbbdb=c:

Critical pair: aabc=adbbdb.

Referenced by [24].

Overlap of [11] dbdbbdb=c with [2] baba=c:

Critical pair: dbdbbdc=caba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [11] dbdbbdb=c with [11] dbdbbdb=c:

Critical pair: dbdbbc=cdbbdb.

Referenced by [27].

Overlap of [10] dabdb=d with [11] dbdbbdb=c:

Critical pair: dabc=ddbbdb.

Referenced by [28].

Overlap of [3] caa=d with [9] aaba=aabdc:

Critical pair: caabdc=dba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [17], [18], [19], [26], [33], [39].

Overlap of [4] aabdb=a with [16] dba=dbdc:

Critical pair: aabdbdc=aa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Referenced by [21], [24].

Overlap of [11] dbdbbdb=c with [16] dba=dbdc:

Critical pair: dbdbbdbdc=ca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [20], [22], [23], [25], [26], [27], [30], [31], [32], [42].

Overlap of [10] dabdb=d with [16] dba=dbdc:

Critical pair: dabdbdc=da.

Reduce LHS:

Flip LHS and RHS.

Referenced by [28], [37].

Overlap of [3] caa=d with [7] ca=dbdb:

Critical pair: dbdba=d.

Reduce LHS:

Defines rule #3.

Referenced by [29], [34], [36], [40], [43].

Overlap of [4] aabdb=a with [17] aa=adc:

Critical pair: adcbdb=a.

Defines rule #14.

Referenced by [32].

Overlap of [11] dbdbbdb=c with [18] dbdb=cdc:

Critical pair: cdcbdb=c.

Defines rule #7.

Referenced by [31].

Simplify [7] ca=dbdb.

Reduce RHS:

Defines rule #18.

Overlap of [12] aabc=adbbdb with [17] aa=adc:

Critical pair: adcbc=adbbdb.

Flip LHS and RHS.

Defines rule #15.

Simplify [13] dbdbba=dbdbbdc.

Reduce RHS:

Referenced by [26].

Overlap of [25] dbdbba=cdcbdc with [18] dbdb=cdc:

Critical pair: cdcba=cdcbdc.

Reduce LHS:

Referenced by [33].

Overlap of [14] dbdbbc=cdbbdb with [18] dbdb=cdc:

Critical pair: cdcbc=cdbbdb.

Flip LHS and RHS.

Defines rule #8.

Overlap of [15] dabc=ddbbdb with [19] da=ddc:

Critical pair: ddcbc=ddbbdb.

Flip LHS and RHS.

Referenced by [38].

Overlap of [20] cdcdc=d with [20] cdcdc=d:

Critical pair: cdd=ddc.

Flip LHS and RHS.

Defines rule #1.

Referenced by [36], [37], [38].

Overlap of [18] dbdb=cdc with [18] dbdb=cdc:

Critical pair: dbcdc=cdcdb.

Defines rule #5.

Overlap of [22] cdcbdb=c with [18] dbdb=cdc:

Critical pair: cdcbcdc=cdb.

Defines rule #10.

Referenced by [33], [34], [35], [41].

Overlap of [21] adcbdb=a with [18] dbdb=cdc:

Critical pair: adcbcdc=adb.

Defines rule #16.

Referenced by [39], [40], [41].

Overlap of [31] cdcbcdc=cdb with [5] cba=bac:

Critical pair: cdcbcdbac=cdbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Referenced by [43].

Overlap of [31] cdcbcdc=cdb with [20] cdcdc=d:

Critical pair: cdcbd=cdbdc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [36], [39].

Overlap of [31] cdcbcdc=cdb with [31] cdcbcdc=cdb:

Critical pair: cdcbcdb=cdbbcdc.

Flip LHS and RHS.

Defines rule #11.

Overlap of [20] cdcdc=d with [34] cdbdc=cdcbd:

Critical pair: cdcdcdcbd=ddbdc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Simplify [19] da=ddc.

Reduce RHS:

Defines rule #19.

Simplify [28] ddbbdb=ddcbc.

Reduce RHS:

Defines rule #9.

Referenced by [42].

Overlap of [32] adcbcdc=adb with [5] cba=bac:

Critical pair: adcbcdbac=adbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [32] adcbcdc=adb with [20] cdcdc=d:

Critical pair: adcbd=adbdc.

Flip LHS and RHS.

Defines rule #13.

Overlap of [32] adcbcdc=adb with [31] cdcbcdc=cdb:

Critical pair: adcbcdb=adbbcdc.

Flip LHS and RHS.

Defines rule #17.

Overlap of [38] ddbbdb=cddbc with [18] dbdb=cdc:

Critical pair: ddbbcdc=cddbcdb.

Defines rule #12.

Overlap of [20] cdcdc=d with [33] cdbba=cdbbdc:

Critical pair: cdcdcdbbdc=ddbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.