Certificate for #3671 ⟨a, b | aabbbabaab=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. ab=c
  2. ca=d

Axiom: aabbbabaab=a.

Referenced by [4].

Axiom: ab=c.

Referenced by [4], [5], [8], [12], [15], [17].

Axiom: ca=d.

Referenced by [4], [5], [6], [7], [9], [18].

Overlap of [1] aabbbabaab=a with [2] ab=c:

Critical pair: acbbabaab=a.

Reduce LHS:

Referenced by [6], [7], [8], [13], [16].

Overlap of [3] ca=d with [2] ab=c:

Critical pair: cc=db.

Flip LHS and RHS.

Defines rule #1.

Referenced by [10], [12], [15], [21], [22], [23], [28], [31].

Overlap of [3] ca=d with [4] acbbdc=a:

Critical pair: ca=dcbbdc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9], [10].

Overlap of [4] acbbdc=a with [3] ca=d:

Critical pair: acbbdd=aa.

Flip LHS and RHS.

Referenced by [14].

Overlap of [4] acbbdc=a with [6] dcbbdc=d:

Critical pair: acbbd=abbdc.

Reduce RHS:

Referenced by [14], [19].

Overlap of [6] dcbbdc=d with [3] ca=d:

Critical pair: dcbbdd=da.

Flip LHS and RHS.

Referenced by [11].

Overlap of [6] dcbbdc=d with [6] dcbbdc=d:

Critical pair: dcbbd=dbbdc.

Reduce RHS:

Defines rule #4.

Referenced by [11], [13], [18], [23], [24].

Simplify [9] da=dcbbdd.

Reduce RHS:

Referenced by [12], [13].

Overlap of [11] da=ccbdcd with [2] ab=c:

Critical pair: dc=ccbdcdb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [13], [18].

Overlap of [11] da=ccbdcd with [4] acbbdc=a:

Critical pair: da=ccbdcdcbbdc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [25].

Simplify [7] aa=acbbdd.

Reduce RHS:

Referenced by [15].

Overlap of [14] aa=cbdcd with [2] ab=c:

Critical pair: ac=cbdcdb.

Reduce RHS:

Referenced by [16], [20].

Overlap of [4] acbbdc=a with [15] ac=cbdccc:

Critical pair: cbdcccbbdc=a.

Flip LHS and RHS.

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

Overlap of [2] ab=c with [16] a=cbdcccbbdc:

Critical pair: cbdcccbbdcb=c.

Referenced by [24], [25], [27], [30].

Overlap of [3] ca=d with [16] a=cbdcccbbdc:

Critical pair: ccbdcccbbdc=d.

Reduce LHS:

Defines rule #5.

Referenced by [21], [22], [29], [31].

Overlap of [8] acbbd=cbdc with [16] a=cbdcccbbdc:

Critical pair: cbdcccbbdccbbd=cbdc.

Referenced by [26].

Overlap of [15] ac=cbdccc with [16] a=cbdcccbbdc:

Critical pair: cbdcccbbdcc=cbdccc.

Referenced by [26].

Overlap of [18] ccbdcc=d with [18] ccbdcc=d:

Critical pair: ccbdd=dbdcc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [18] ccbdcc=d with [21] ccdcc=ccbdd:

Critical pair: ccbdccbdd=ddcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [10] dcbbd=ccbdc with [5] db=cc:

Critical pair: dcbbcc=ccbdcb.

Defines rule #7.

Overlap of [17] cbdcccbbdcb=c with [10] dcbbd=ccbdc:

Critical pair: cbdcccbbccbdc=cbd.

Referenced by [25].

Overlap of [17] cbdcccbbdcb=c with [13] dcbdcc=ccbdcd:

Critical pair: cbdcccbbccbdcd=cdcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [30].

Overlap of [19] cbdcccbbdccbbd=cbdc with [20] cbdcccbbdcc=cbdccc:

Critical pair: cbdcccbbd=cbdc.

Defines rule #9.

Referenced by [27], [28], [30], [32].

Overlap of [17] cbdcccbbdcb=c with [26] cbdcccbbd=cbdc:

Critical pair: cbdccb=c.

Defines rule #6.

Referenced by [30].

Overlap of [26] cbdcccbbd=cbdc with [5] db=cc:

Critical pair: cbdcccbbcc=cbdcb.

Defines rule #12.

Referenced by [29].

Overlap of [28] cbdcccbbcc=cbdcb with [18] ccbdcc=d:

Critical pair: cbdcccbbcd=cbdcbcbdcc.

Flip LHS and RHS.

Defines rule #13.

Referenced by [30].

Overlap of [17] cbdcccbbdcb=c with [29] cbdcbcbdcc=cbdcccbbcd:

Critical pair: cbdcccbbdcbdcccbbcd=cdcbcbdcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [31].

Overlap of [18] ccbdcc=d with [30] cdcbcbdcc=cbddcbbcd:

Critical pair: ccbdccbddcbbcd=ddcbcbdcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Simplify [16] a=cbdcccbbdc.

Reduce RHS:

Defines rule #14.