Certificate for #4007 ⟨a, b | aaababbba=ab⟩

Completion settings:

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

Axiom: aaababbba=ab.

Referenced by [3].

Axiom: bbba=c.

Defines rule #15.

Referenced by [3], [4], [9], [10], [11], [12], [13], [14], [23], [24], [25], [26].

Overlap of [1] aaababbba=ab with [2] bbba=c:

Critical pair: aaabac=ab.

Defines rule #1.

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

Overlap of [2] bbba=c with [3] aaabac=ab:

Critical pair: bbbab=caabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [6], [7], [8], [16], [19], [21].

Overlap of [3] aaabac=ab with [4] caabac=cb:

Critical pair: aaabacb=abaabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

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

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

Critical pair: caabacb=cbaabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

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

Overlap of [5] abaabac=abb with [4] caabac=cb:

Critical pair: abaabacb=abbaabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [25].

Overlap of [4] caabac=cb with [6] cbaabac=cbb:

Critical pair: caabacbb=cbbaabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [26].

Overlap of [5] abaabac=abb with [6] cbaabac=cbb:

Critical pair: abaabacbb=abbbaabac.

Reduce LHS:

Reduce RHS:

Defines rule #22.

Referenced by [11], [12], [13].

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

Critical pair: cbaabacbb=cbbbaabac.

Reduce LHS:

Reduce RHS:

Defines rule #23.

Referenced by [23], [24].

Overlap of [9] abbbb=acabac with [2] bbba=c:

Critical pair: abc=acabaca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [14], [15], [16], [17], [18], [19], [20], [22], [25], [26].

Overlap of [9] abbbb=acabac with [2] bbba=c:

Critical pair: abbc=acabacba.

Defines rule #5.

Overlap of [9] abbbb=acabac with [2] bbba=c:

Critical pair: abbbc=acabacbba.

Defines rule #16.

Overlap of [2] bbba=c with [11] acabaca=abc:

Critical pair: bbbabc=ccabaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [21], [22].

Overlap of [3] aaabac=ab with [11] acabaca=abc:

Critical pair: aaababc=ababaca.

Flip LHS and RHS.

Defines rule #11.

Overlap of [4] caabac=cb with [11] acabaca=abc:

Critical pair: caababc=cbabaca.

Flip LHS and RHS.

Defines rule #12.

Overlap of [5] abaabac=abb with [11] acabaca=abc:

Critical pair: abaababc=abbabaca.

Flip LHS and RHS.

Defines rule #20.

Overlap of [6] cbaabac=cbb with [11] acabaca=abc:

Critical pair: cbaababc=cbbabaca.

Flip LHS and RHS.

Defines rule #21.

Overlap of [11] acabaca=abc with [4] caabac=cb:

Critical pair: acabacb=abcabac.

Flip LHS and RHS.

Defines rule #9.

Overlap of [11] acabaca=abc with [11] acabaca=abc:

Critical pair: acababc=abcbaca.

Flip LHS and RHS.

Defines rule #13.

Overlap of [14] ccabaca=cbc with [4] caabac=cb:

Critical pair: ccabacb=cbcabac.

Flip LHS and RHS.

Defines rule #10.

Overlap of [14] ccabaca=cbc with [11] acabaca=abc:

Critical pair: ccababc=cbcbaca.

Flip LHS and RHS.

Defines rule #14.

Overlap of [10] cbbbb=ccabac with [2] bbba=c:

Critical pair: cbbc=ccabacba.

Defines rule #6.

Overlap of [10] cbbbb=ccabac with [2] bbba=c:

Critical pair: cbbbc=ccabacbba.

Defines rule #17.

Overlap of [7] abbaabac=abbb with [11] acabaca=abc:

Critical pair: abbaababc=abbbabaca.

Reduce RHS:

Defines rule #24.

Overlap of [8] cbbaabac=cbbb with [11] acabaca=abc:

Critical pair: cbbaababc=cbbbabaca.

Reduce RHS:

Defines rule #25.