Certificate for #4105 ⟨a, b | aabaabbba=ab⟩

Completion settings:

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

Axiom: aabaabbba=ab.

Referenced by [3].

Axiom: abbb=c.

Defines rule #3.

Referenced by [3], [4], [8], [9], [10], [13].

Overlap of [1] aabaabbba=ab with [2] abbb=c:

Critical pair: aabaca=ab.

Defines rule #7.

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

Overlap of [3] aabaca=ab with [2] abbb=c:

Critical pair: aabacc=abbbb.

Reduce RHS:

Defines rule #1.

Referenced by [6], [7], [12], [15].

Overlap of [3] aabaca=ab with [3] aabaca=ab:

Critical pair: aabacab=ababaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

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

Overlap of [3] aabaca=ab with [4] aabacc=cb:

Critical pair: aabaccb=ababacc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [7], [10], [14], [16], [20].

Overlap of [3] aabaca=ab with [6] ababacc=cbb:

Critical pair: aabaccbb=abbabacc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] aabaca=ab with [5] ababaca=abb:

Critical pair: aabacabb=abbabaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [18], [19].

Overlap of [5] ababaca=abb with [5] ababaca=abb:

Critical pair: ababacabb=abbbabaca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [11], [12], [13], [14], [15], [16], [17], [18], [19], [21], [22].

Overlap of [5] ababaca=abb with [6] ababacc=cbb:

Critical pair: ababaccbb=abbbabacc.

Reduce LHS:

Reduce RHS:

Defines rule #6.

Overlap of [3] aabaca=ab with [9] cabaca=cb:

Critical pair: aabacb=abbaca.

Flip LHS and RHS.

Defines rule #9.

Overlap of [4] aabacc=cb with [9] cabaca=cb:

Critical pair: aabaccb=cbabaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [20], [21], [23].

Overlap of [5] ababaca=abb with [9] cabaca=cb:

Critical pair: ababacb=abbbaca.

Reduce RHS:

Defines rule #14.

Referenced by [22], [23].

Overlap of [6] ababacc=cbb with [9] cabaca=cb:

Critical pair: ababaccb=cbbabaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [9] cabaca=cb with [4] aabacc=cb:

Critical pair: cabaccb=cbabacc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [20], [23].

Overlap of [9] cabaca=cb with [6] ababacc=cbb:

Critical pair: cabaccbb=cbbabacc.

Flip LHS and RHS.

Defines rule #11.

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

Critical pair: cabacb=cbbaca.

Flip LHS and RHS.

Defines rule #5.

Overlap of [8] abbabaca=c with [9] cabaca=cb:

Critical pair: abbabacb=cbaca.

Defines rule #20.

Overlap of [9] cabaca=cb with [8] abbabaca=c:

Critical pair: cabacc=cbbbabaca.

Flip LHS and RHS.

Defines rule #21.

Overlap of [12] cbabaca=cbb with [6] ababacc=cbb:

Critical pair: cbabaccbb=cbbbabacc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [12] cbabaca=cbb with [9] cabaca=cb:

Critical pair: cbabacb=cbbbaca.

Flip LHS and RHS.

Defines rule #12.

Overlap of [9] cabaca=cb with [13] ababacb=caca:

Critical pair: cabaccaca=cbbabacb.

Flip LHS and RHS.

Defines rule #17.

Overlap of [12] cbabaca=cbb with [13] ababacb=caca:

Critical pair: cbabaccaca=cbbbabacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.