Certificate for #861 ⟨a, b | abbabaab=a⟩

Completion settings:

• Auxiliary generators:
  1. c = ababaa
  2. d = bbcb
• Reduction order:
  • Right-to-left recursive path with deg(d) = deg(b) = 0, d < b; deg(c) = deg(a) = 1, c < a

Axiom: abbabaab=a.

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

Axiom: ababaa=c.

Referenced by [5], [6], [8], [9], [14], [17].

Axiom: bbcb=d.

Defines rule #7.

Referenced by [4], [7], [10], [14], [15], [16], [17], [18], [19], [20], [21], [22], [23], [24], [25], [26].

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

Critical pair: bbcd=dbcb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [14], [15], [16], [17], [18], [19], [21], [22], [24].

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

Critical pair: ababac=cbabaa.

Flip LHS and RHS.

Referenced by [11], [15].

Overlap of [1] abbabaab=a with [1] abbabaab=a:

Critical pair: abbabaa=ababaab.

Reduce RHS:

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

Overlap of [1] abbabaab=a with [3] bbcb=d:

Critical pair: abbabaad=abcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [9], [12].

Overlap of [2] ababaa=c with [1] abbabaab=a:

Critical pair: ababaa=cbbabaab.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [2] ababaa=c with [7] abcb=cbd:

Critical pair: ababacbd=cbcb.

Referenced by [18].

Overlap of [3] bbcb=d with [8] cbbabaab=c:

Critical pair: bbc=dbabaab.

Flip LHS and RHS.

Referenced by [16].

Overlap of [8] cbbabaab=c with [1] abbabaab=a:

Critical pair: cbbabaa=cbabaab.

Reduce RHS:

Referenced by [14].

Overlap of [8] cbbabaab=c with [7] abcb=cbd:

Critical pair: cbbabacbd=ccb.

Referenced by [19].

Overlap of [1] abbabaab=a with [6] abbabaa=cb:

Critical pair: cbb=a.

Flip LHS and RHS.

Defines rule #8.

Referenced by [14], [15], [16], [17], [18], [19].

Overlap of [6] abbabaa=cb with [2] ababaa=c:

Critical pair: abbabac=cbbabaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [17], [18], [24].

Overlap of [8] cbbabaab=c with [6] abbabaa=cb:

Critical pair: cbbabacb=cbabaa.

Reduce LHS:

Reduce RHS:

Defines rule #12.

Referenced by [16], [19], [22], [23], [24], [25], [26].

Simplify [10] dbabaab=bbc.

Reduce LHS:

Referenced by [22], [23].

Overlap of [2] ababaa=c with [13] a=cbb:

Critical pair: cbbbabaa=c.

Reduce LHS:

Defines rule #14.

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

Overlap of [9] ababacbd=cbcb with [13] a=cbb:

Critical pair: cbbbabacbd=cbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [12] cbbabacbd=ccb with [13] a=cbb:

Critical pair: cbbcbbbacbd=ccb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [3] bbcb=d with [17] cbbdbbcd=c:

Critical pair: bbc=dbdbbcd.

Flip LHS and RHS.

Defines rule #4.

Referenced by [21], [22], [26].

Overlap of [20] dbdbbcd=bbc with [4] dbcb=bbcd:

Critical pair: dbdbbcbbcd=bbcbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [20] dbdbbcd=bbc with [16] ddbbcdb=bbc:

Critical pair: dbdbbcbbc=bbcdbbcdb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [16] ddbbcdb=bbc with [15] cdbbcd=cbddbc:

Critical pair: ddbbcbddbc=bbcbcd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [15] cdbbcd=cbddbc with [15] cdbbcd=cbddbc:

Critical pair: cdbbcbddbc=cbddbcbbcd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [17] cbbdbbcd=c with [15] cdbbcd=cbddbc:

Critical pair: cbbdbbcbddbc=cbbcd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [20] dbdbbcd=bbc with [15] cdbbcd=cbddbc:

Critical pair: dbdbbcbddbc=bbcbbcd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [17] cbbdbbcd=c with [26] dbcd=dbddddbc:

Critical pair: cbbdbbcdbddddbc=cbcd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Simplify [18] cbcb=cbbddbcd.

Reduce RHS:

Defines rule #16.

Simplify [19] ccb=cbddbcd.

Reduce RHS:

Defines rule #15.

Simplify [21] dcb=dbddbcd.

Reduce RHS:

Defines rule #5.