Certificate for #4187 ⟨a, b | aabbabbba=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: aabbabbba=ab.

Referenced by [3].

Axiom: abbb=c.

Defines rule #3.

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

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

Critical pair: aabbca=ab.

Defines rule #7.

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

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

Critical pair: aabbcc=abbbb.

Reduce RHS:

Defines rule #1.

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

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

Critical pair: aabbcab=ababbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

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

Overlap of [3] aabbca=ab with [4] aabbcc=cb:

Critical pair: aabbccb=ababbcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [7], [10], [14], [16], [18], [21].

Overlap of [3] aabbca=ab with [6] ababbcc=cbb:

Critical pair: aabbccbb=abbabbcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] aabbca=ab with [5] ababbca=abb:

Critical pair: aabbcabb=abbabbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [20].

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

Critical pair: ababbcabb=abbbabbca.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [11], [12], [13], [14], [15], [16], [17], [19], [20].

Overlap of [5] ababbca=abb with [6] ababbcc=cbb:

Critical pair: ababbccbb=abbbabbcc.

Reduce LHS:

Reduce RHS:

Defines rule #6.

Overlap of [3] aabbca=ab with [9] cabbca=cb:

Critical pair: aabbcb=abbbca.

Reduce RHS:

Defines rule #8.

Referenced by [18], [19], [22].

Overlap of [4] aabbcc=cb with [9] cabbca=cb:

Critical pair: aabbccb=cbabbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

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

Overlap of [5] ababbca=abb with [9] cabbca=cb:

Critical pair: ababbcb=abbbbca.

Reduce RHS:

Defines rule #14.

Referenced by [23].

Overlap of [6] ababbcc=cbb with [9] cabbca=cb:

Critical pair: ababbccb=cbbabbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [9] cabbca=cb with [4] aabbcc=cb:

Critical pair: cabbccb=cbabbcc.

Flip LHS and RHS.

Defines rule #4.

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

Overlap of [9] cabbca=cb with [6] ababbcc=cbb:

Critical pair: cabbccbb=cbbabbcc.

Flip LHS and RHS.

Defines rule #12.

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

Critical pair: cabbcb=cbbbca.

Flip LHS and RHS.

Defines rule #5.

Overlap of [5] ababbca=abb with [11] aabbcb=cca:

Critical pair: ababbccca=abbabbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [9] cabbca=cb with [11] aabbcb=cca:

Critical pair: cabbccca=cbabbcb.

Flip LHS and RHS.

Defines rule #11.

Overlap of [9] cabbca=cb with [8] abbabbca=c:

Critical pair: cabbcc=cbbbabbca.

Flip LHS and RHS.

Defines rule #21.

Overlap of [12] cbabbca=cbb with [6] ababbcc=cbb:

Critical pair: cbabbccbb=cbbbabbcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [12] cbabbca=cbb with [11] aabbcb=cca:

Critical pair: cbabbccca=cbbabbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [12] cbabbca=cbb with [13] ababbcb=cbca:

Critical pair: cbabbccbca=cbbbabbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.