Certificate for #995 ⟨a, b | abbaaab=ba⟩

Completion settings:

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

Axiom: abbaaab=ba.

Referenced by [4].

Axiom: baaa=c.

Referenced by [4], [5].

Axiom: ab=d.

Defines rule #28.

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

Overlap of [1] abbaaab=ba with [3] ab=d:

Critical pair: dbaaab=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #31.

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

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

Critical pair: dcbaa=c.

Reduce LHS:

Defines rule #3.

Referenced by [8], [9], [11], [15], [16], [21], [28].

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

Critical pair: adcb=da.

Flip LHS and RHS.

Defines rule #30.

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

Critical pair: bd=dcbb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [9], [12], [22], [33].

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

Critical pair: dcdcdcdcb=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [10].

Overlap of [5] dcdcdcb=c with [7] dcbb=bd:

Critical pair: dcdcbd=cb.

Defines rule #2.

Referenced by [11], [12], [13], [14], [23], [29], [30].

Overlap of [8] ca=dcc with [3] ab=d:

Critical pair: cd=dccb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [14], [19], [24].

Overlap of [9] dcdcbd=cb with [5] dcdcdcb=c:

Critical pair: dcdcbc=cbcdcdcb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [16], [17], [18], [29].

Overlap of [9] dcdcbd=cb with [7] dcbb=bd:

Critical pair: dcdcbbd=cbcbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [15], [27].

Overlap of [9] dcdcbd=cb with [9] dcdcbd=cb:

Critical pair: dcdcbcb=cbcdcbd.

Defines rule #14.

Referenced by [27].

Overlap of [9] dcdcbd=cb with [10] dccb=cd:

Critical pair: dcdcbcd=cbccb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [18], [20], [32].

Overlap of [5] dcdcdcb=c with [12] cbcbb=dcbdd:

Critical pair: dcdcddcbdd=ccbb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [19], [20].

Overlap of [5] dcdcdcb=c with [11] cbcdcdcb=dcdcbc:

Critical pair: dcdcddcdcbc=ccdcdcb.

Defines rule #5.

Referenced by [29], [30], [31].

Overlap of [11] cbcdcdcb=dcdcbc with [11] cbcdcdcb=dcdcbc:

Critical pair: cbcdcddcdcbc=dcdcbccdcdcb.

Flip LHS and RHS.

Defines rule #17.

Overlap of [11] cbcdcdcb=dcdcbc with [14] cbccb=dcdcbcd:

Critical pair: cbcdcddcdcbcd=dcdcbcccb.

Flip LHS and RHS.

Defines rule #16.

Overlap of [10] dccb=cd with [15] ccbb=dcdcddcbdd:

Critical pair: ddcdcddcbdd=cdb.

Defines rule #4.

Referenced by [21], [22], [23], [24], [25], [26], [31].

Overlap of [14] cbccb=dcdcbcd with [15] ccbb=dcdcddcbdd:

Critical pair: cbdcdcddcbdd=dcdcbcdb.

Flip LHS and RHS.

Defines rule #15.

Overlap of [19] ddcdcddcbdd=cdb with [5] dcdcdcb=c:

Critical pair: ddcdcddcbdc=cdbcdcdcb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [32].

Overlap of [19] ddcdcddcbdd=cdb with [7] dcbb=bd:

Critical pair: ddcdcddcbdbd=cdbcbb.

Flip LHS and RHS.

Defines rule #25.

Overlap of [19] ddcdcddcbdd=cdb with [9] dcdcbd=cb:

Critical pair: ddcdcddcbdcb=cdbcdcbd.

Defines rule #19.

Referenced by [33].

Overlap of [19] ddcdcddcbdd=cdb with [10] dccb=cd:

Critical pair: ddcdcddcbdcd=cdbccb.

Flip LHS and RHS.

Defines rule #9.

Overlap of [19] ddcdcddcbdd=cdb with [19] ddcdcddcbdd=cdb:

Critical pair: ddcdcddcbcdb=cdbcdcddcbdd.

Defines rule #18.

Overlap of [19] ddcdcddcbdd=cdb with [19] ddcdcddcbdd=cdb:

Critical pair: ddcdcddcbdcdb=cdbdcdcddcbdd.

Defines rule #20.

Overlap of [13] dcdcbcb=cbcdcbd with [12] cbcbb=dcbdd:

Critical pair: dcddcbdd=cbcdcbdb.

Flip LHS and RHS.

Defines rule #24.

Referenced by [28], [30].

Overlap of [5] dcdcdcb=c with [27] cbcdcbdb=dcddcbdd:

Critical pair: dcdcddcddcbdd=ccdcbdb.

Flip LHS and RHS.

Defines rule #13.

Overlap of [16] dcdcddcdcbc=ccdcdcb with [11] cbcdcdcb=dcdcbc:

Critical pair: dcdcddcddcdcbc=ccdcdcbdcdcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [16] dcdcddcdcbc=ccdcdcb with [27] cbcdcbdb=dcddcbdd:

Critical pair: dcdcddcddcddcbdd=ccdcdcbdcbdb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Overlap of [19] ddcdcddcbdd=cdb with [16] dcdcddcdcbc=ccdcdcb:

Critical pair: ddcdcddcbdccdcdcb=cdbcdcddcdcbc.

Defines rule #22.

Overlap of [21] cdbcdcdcb=ddcdcddcbdc with [14] cbccb=dcdcbcd:

Critical pair: cdbcdcddcdcbcd=ddcdcddcbdcccb.

Flip LHS and RHS.

Defines rule #21.

Overlap of [23] ddcdcddcbdcb=cdbcdcbd with [7] dcbb=bd:

Critical pair: ddcdcddcbbd=cdbcdcbdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.