Certificate for #4148 ⟨a, b | aababbbba=ab⟩

Completion settings:

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

Axiom: aababbbba=ab.

Referenced by [3].

Axiom: bbbba=c.

Defines rule #19.

Referenced by [3], [4], [11], [12], [13], [14], [15], [16], [17], [22], [23].

Overlap of [1] aababbbba=ab with [2] bbbba=c:

Critical pair: aabac=ab.

Defines rule #1.

Referenced by [4], [5], [18].

Overlap of [2] bbbba=c with [3] aabac=ab:

Critical pair: bbbbab=cabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6], [7], [8], [19], [24], [25], [28].

Overlap of [3] aabac=ab with [4] cabac=cb:

Critical pair: aabacb=ababac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [7], [9], [20].

Overlap of [4] cabac=cb with [4] cabac=cb:

Critical pair: cabacb=cbabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [8], [9], [10], [11], [12], [21], [26], [30].

Overlap of [5] ababac=abb with [4] cabac=cb:

Critical pair: ababacb=abbabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [11], [22], [32].

Overlap of [4] cabac=cb with [6] cbabac=cbb:

Critical pair: cabacbb=cbbabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [12], [23], [27], [31], [33].

Overlap of [5] ababac=abb with [6] cbabac=cbb:

Critical pair: ababacbb=abbbabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [6] cbabac=cbb with [6] cbabac=cbb:

Critical pair: cbabacbb=cbbbabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [7] abbabac=abbb with [6] cbabac=cbb:

Critical pair: abbabacbb=abbbbabac.

Reduce LHS:

Reduce RHS:

Defines rule #26.

Referenced by [13], [14], [15], [16], [32].

Overlap of [6] cbabac=cbb with [8] cbbabac=cbbb:

Critical pair: cbabacbbb=cbbbbabac.

Reduce LHS:

Reduce RHS:

Defines rule #27.

Referenced by [33].

Overlap of [11] abbbbb=acbac with [2] bbbba=c:

Critical pair: abc=acbaca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [17], [18], [19], [20], [21], [22], [23], [24], [32].

Overlap of [11] abbbbb=acbac with [2] bbbba=c:

Critical pair: abbc=acbacba.

Defines rule #5.

Overlap of [11] abbbbb=acbac with [2] bbbba=c:

Critical pair: abbbc=acbacbba.

Defines rule #13.

Overlap of [11] abbbbb=acbac with [2] bbbba=c:

Critical pair: abbbbc=acbacbbba.

Defines rule #20.

Overlap of [2] bbbba=c with [13] acbaca=abc:

Critical pair: bbbbabc=ccbaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [25], [26], [27], [28], [33].

Overlap of [3] aabac=ab with [13] acbaca=abc:

Critical pair: aababc=abbaca.

Flip LHS and RHS.

Defines rule #11.

Overlap of [4] cabac=cb with [13] acbaca=abc:

Critical pair: cababc=cbbaca.

Flip LHS and RHS.

Defines rule #12.

Referenced by [32], [33].

Overlap of [5] ababac=abb with [13] acbaca=abc:

Critical pair: abababc=abbbaca.

Flip LHS and RHS.

Defines rule #17.

Overlap of [6] cbabac=cbb with [13] acbaca=abc:

Critical pair: cbababc=cbbbaca.

Flip LHS and RHS.

Defines rule #18.

Overlap of [7] abbabac=abbb with [13] acbaca=abc:

Critical pair: abbababc=abbbbaca.

Reduce RHS:

Defines rule #22.

Overlap of [8] cbbabac=cbbb with [13] acbaca=abc:

Critical pair: cbbababc=cbbbbaca.

Reduce RHS:

Defines rule #23.

Overlap of [13] acbaca=abc with [4] cabac=cb:

Critical pair: acbacb=abcbac.

Flip LHS and RHS.

Defines rule #9.

Overlap of [4] cabac=cb with [17] ccbaca=cbc:

Critical pair: cabacbc=cbcbaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [6] cbabac=cbb with [17] ccbaca=cbc:

Critical pair: cbabacbc=cbbcbaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [8] cbbabac=cbbb with [17] ccbaca=cbc:

Critical pair: cbbabacbc=cbbbcbaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [17] ccbaca=cbc with [4] cabac=cb:

Critical pair: ccbacb=cbcbac.

Flip LHS and RHS.

Defines rule #10.

Referenced by [29].

Overlap of [25] cbcbaca=cbbc with [28] cbcbac=ccbacb:

Critical pair: ccbacba=cbbc.

Flip LHS and RHS.

Defines rule #6.

Referenced by [30].

Overlap of [26] cbbcbaca=cbbbc with [29] cbbc=ccbacba:

Critical pair: ccbacbabaca=cbbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [31].

Overlap of [27] cbbbcbaca=cbbbbc with [30] cbbbc=ccbacbba:

Critical pair: ccbacbbabaca=cbbbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [7] abbabac=abbb with [19] cbbaca=cababc:

Critical pair: abbabacababc=abbbbbaca.

Reduce LHS:

Reduce RHS:

Defines rule #28.

Overlap of [8] cbbabac=cbbb with [19] cbbaca=cababc:

Critical pair: cbbabacababc=cbbbbbaca.

Reduce LHS:

Reduce RHS:

Defines rule #29.