Certificate for #5401 ⟨a, b | abbabba=abab⟩

Completion settings:

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

Axiom: abbabba=abab.

Referenced by [4].

Axiom: ababbb=c.

Referenced by [6].

Axiom: bab=d.

Defines rule #23.

Referenced by [4], [5], [6], [7], [8], [10], [11], [14], [16], [24], [27], [34].

Simplify [1] abbabba=abab.

Reduce RHS:

Referenced by [5].

Overlap of [4] abbabba=ad with [3] bab=d:

Critical pair: abdba=ad.

Defines rule #28.

Referenced by [10], [11], [12], [32].

Overlap of [2] ababbb=c with [3] bab=d:

Critical pair: adbb=c.

Referenced by [8], [13], [20].

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

Critical pair: bad=dab.

Defines rule #12.

Referenced by [9], [10], [12], [14], [15], [17].

Overlap of [6] adbb=c with [3] bab=d:

Critical pair: adbd=cab.

Flip LHS and RHS.

Referenced by [9], [21].

Overlap of [8] cab=adbd with [7] bad=dab:

Critical pair: cadab=adbdad.

Flip LHS and RHS.

Referenced by [22].

Overlap of [3] bab=d with [5] abdba=ad:

Critical pair: bad=ddba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [17], [18], [19], [30].

Overlap of [5] abdba=ad with [3] bab=d:

Critical pair: abdd=adb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [13], [14], [15], [20], [21], [22], [26].

Overlap of [5] abdba=ad with [7] bad=dab:

Critical pair: abddab=add.

Defines rule #27.

Referenced by [20], [28].

Overlap of [6] adbb=c with [11] adb=abdd:

Critical pair: abddb=c.

Defines rule #20.

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

Overlap of [7] bad=dab with [11] adb=abdd:

Critical pair: babdd=dabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [25], [28].

Overlap of [11] adb=abdd with [7] bad=dab:

Critical pair: addab=abddad.

Flip LHS and RHS.

Defines rule #17.

Overlap of [3] bab=d with [13] abddb=c:

Critical pair: bc=dddb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [19], [23].

Overlap of [10] ddba=dab with [7] bad=dab:

Critical pair: dddab=dabd.

Defines rule #10.

Referenced by [20], [25], [31].

Overlap of [13] abddb=c with [10] ddba=dab:

Critical pair: abdab=ca.

Defines rule #26.

Referenced by [24], [26], [29], [33], [34].

Overlap of [16] dddb=bc with [10] ddba=dab:

Critical pair: ddab=bca.

Flip LHS and RHS.

Defines rule #13.

Referenced by [20].

Overlap of [6] adbb=c with [19] bca=ddab:

Critical pair: adbddab=cca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [23].

Simplify [8] cab=adbd.

Reduce RHS:

Defines rule #11.

Referenced by [23].

Overlap of [9] adbdad=cadab with [11] adb=abdd:

Critical pair: abdddad=cadab.

Defines rule #18.

Overlap of [20] cca=addd with [21] cab=abddd:

Critical pair: cabddd=adddb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [33].

Overlap of [18] abdab=ca with [3] bab=d:

Critical pair: abdad=caab.

Defines rule #16.

Referenced by [26], [29], [34].

Overlap of [17] dddab=dabd with [14] dabb=ddd:

Critical pair: ddddd=dabdb.

Flip LHS and RHS.

Defines rule #22.

Referenced by [31], [32].

Overlap of [24] abdad=caab with [11] adb=abdd:

Critical pair: abdabdd=caabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Referenced by [27].

Overlap of [26] caabb=cadd with [3] bab=d:

Critical pair: caabd=caddab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [12] abddab=add with [14] dabb=ddd:

Critical pair: abdddd=addb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [29], [30].

Overlap of [24] abdad=caab with [28] addb=abdddd:

Critical pair: abdabdddd=caabdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [28] addb=abdddd with [10] ddba=dab:

Critical pair: adab=abdddda.

Flip LHS and RHS.

Defines rule #19.

Referenced by [34].

Overlap of [17] dddab=dabd with [25] dabdb=ddddd:

Critical pair: ddddddd=dabddb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [25] dabdb=ddddd with [5] abdba=ad:

Critical pair: dad=ddddda.

Flip LHS and RHS.

Defines rule #2.

Overlap of [18] abdab=ca with [23] abc=abdddddd:

Critical pair: abdabdddddd=cac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [18] abdab=ca with [30] abdddda=adab:

Critical pair: abdadab=cadddda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.