Certificate for #4353 ⟨a, b | abbbaaaab=ba⟩

Completion settings:

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

Axiom: abbbaaaab=ba.

Referenced by [4].

Axiom: baaaa=c.

Referenced by [4], [5].

Axiom: abb=d.

Defines rule #24.

Referenced by [4], [6], [7].

Overlap of [1] abbbaaaab=ba with [3] abb=d:

Critical pair: dbaaaab=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

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

Overlap of [2] baaaa=c with [4] ba=dcb:

Critical pair: dcbaaa=c.

Reduce LHS:

Defines rule #1.

Referenced by [8], [9], [10], [11], [13], [18], [20], [22], [29].

Overlap of [3] abb=d with [4] ba=dcb:

Critical pair: abdcb=da.

Flip LHS and RHS.

Defines rule #26.

Overlap of [4] ba=dcb with [3] abb=d:

Critical pair: bd=dcbbb.

Flip LHS and RHS.

Referenced by [9], [16].

Overlap of [5] dcdcdcdcb=c with [4] ba=dcb:

Critical pair: dcdcdcdcdcb=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [5] dcdcdcdcb=c with [7] dcbbb=bd:

Critical pair: dcdcdcbd=cbb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [10], [16], [17], [25].

Overlap of [5] dcdcdcdcb=c with [9] cbb=dcdcdcbd:

Critical pair: dcdcdcddcdcdcbd=cb.

Defines rule #2.

Referenced by [11], [12], [17], [19], [23].

Overlap of [10] dcdcdcddcdcdcbd=cb with [5] dcdcdcdcb=c:

Critical pair: dcdcdcddcdcdcbc=cbcdcdcdcb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [13], [14], [15], [21].

Overlap of [10] dcdcdcddcdcdcbd=cb with [10] dcdcdcddcdcdcbd=cb:

Critical pair: dcdcdcddcdcdcbcb=cbcdcdcddcdcdcbd.

Defines rule #12.

Overlap of [5] dcdcdcdcb=c with [11] cbcdcdcdcb=dcdcdcddcdcdcbc:

Critical pair: dcdcdcddcdcdcddcdcdcbc=ccdcdcdcb.

Defines rule #3.

Referenced by [15], [24], [30].

Overlap of [11] cbcdcdcdcb=dcdcdcddcdcdcbc with [11] cbcdcdcdcb=dcdcdcddcdcdcbc:

Critical pair: cbcdcdcddcdcdcddcdcdcbc=dcdcdcddcdcdcbccdcdcdcb.

Flip LHS and RHS.

Defines rule #14.

Overlap of [13] dcdcdcddcdcdcddcdcdcbc=ccdcdcdcb with [11] cbcdcdcdcb=dcdcdcddcdcdcbc:

Critical pair: dcdcdcddcdcdcddcdcddcdcdcddcdcdcbc=ccdcdcdcbdcdcdcb.

Flip LHS and RHS.

Defines rule #11.

Overlap of [7] dcbbb=bd with [9] cbb=dcdcdcbd:

Critical pair: ddcdcdcbdb=bd.

Defines rule #10.

Referenced by [17], [25], [26].

Overlap of [10] dcdcdcddcdcdcbd=cb with [16] ddcdcdcbdb=bd:

Critical pair: dcdcdcddcdcdcbbd=cbdcdcdcbdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [18], [19].

Overlap of [5] dcdcdcdcb=c with [17] cbdcdcdcbdb=dcdcdcddcdcddcdcdcbdd:

Critical pair: dcdcdcddcdcdcddcdcddcdcdcbdd=cdcdcdcbdb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [20], [21].

Overlap of [10] dcdcdcddcdcdcbd=cb with [17] cbdcdcdcbdb=dcdcdcddcdcddcdcdcbdd:

Critical pair: dcdcdcddcdcddcdcdcddcdcddcdcdcbdd=cbcdcdcbdb.

Flip LHS and RHS.

Defines rule #19.

Referenced by [29], [30].

Overlap of [5] dcdcdcdcb=c with [18] cdcdcdcbdb=dcdcdcddcdcdcddcdcddcdcdcbdd:

Critical pair: ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb.

Defines rule #4.

Referenced by [22], [23], [24], [25], [26], [27], [28].

Overlap of [11] cbcdcdcdcb=dcdcdcddcdcdcbc with [18] cdcdcdcbdb=dcdcdcddcdcdcddcdcddcdcdcbdd:

Critical pair: cbdcdcdcddcdcdcddcdcddcdcdcbdd=dcdcdcddcdcdcbcdb.

Flip LHS and RHS.

Defines rule #13.

Overlap of [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb with [5] dcdcdcdcb=c:

Critical pair: ddcdcdcddcdcdcddcdcddcdcdcbdc=cdbcdcdcdcb.

Flip LHS and RHS.

Defines rule #7.

Overlap of [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb with [10] dcdcdcddcdcdcbd=cb:

Critical pair: ddcdcdcddcdcdcddcdcddcdcdcbdcb=cdbcdcdcddcdcdcbd.

Defines rule #16.

Overlap of [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb with [13] dcdcdcddcdcdcddcdcdcbc=ccdcdcdcb:

Critical pair: ddcdcdcddcdcdcddcdcddcdcdcbdccdcdcdcb=cdbcdcdcddcdcdcddcdcdcbc.

Defines rule #18.

Overlap of [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb with [16] ddcdcdcbdb=bd:

Critical pair: ddcdcdcddcdcdcddcdcddcdcdcbbd=cdbcdcdcbdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb with [16] ddcdcdcbdb=bd:

Critical pair: ddcdcdcddcdcdcddcdcddcdcdcbdbd=cdbdcdcdcbdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb with [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb:

Critical pair: ddcdcdcddcdcdcddcdcddcdcdcbcdb=cdbcdcdcddcdcdcddcdcddcdcdcbdd.

Defines rule #15.

Overlap of [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb with [20] ddcdcdcddcdcdcddcdcddcdcdcbdd=cdb:

Critical pair: ddcdcdcddcdcdcddcdcddcdcdcbdcdb=cdbdcdcdcddcdcdcddcdcddcdcdcbdd.

Defines rule #17.

Overlap of [5] dcdcdcdcb=c with [19] cbcdcdcbdb=dcdcdcddcdcddcdcdcddcdcddcdcdcbdd:

Critical pair: dcdcdcddcdcdcddcdcddcdcdcddcdcddcdcdcbdd=ccdcdcbdb.

Flip LHS and RHS.

Defines rule #8.

Overlap of [13] dcdcdcddcdcdcddcdcdcbc=ccdcdcdcb with [19] cbcdcdcbdb=dcdcdcddcdcddcdcdcddcdcddcdcdcbdd:

Critical pair: dcdcdcddcdcdcddcdcddcdcdcddcdcddcdcdcddcdcddcdcdcbdd=ccdcdcdcbdcdcbdb.

Flip LHS and RHS.

Defines rule #23.