Certificate for #5606 ⟨a, b | aaabba=abaab⟩

Completion settings:

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

Axiom: aaabba=abaab.

Referenced by [3].

Axiom: aba=c.

Defines rule #1.

Referenced by [3], [4], [5], [6], [7], [9], [10], [11], [13], [14], [15], [16], [17].

Simplify [1] aaabba=abaab.

Reduce RHS:

Defines rule #3.

Referenced by [5], [6], [7], [9], [13], [14], [16].

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

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #2.

Overlap of [3] aaabba=cab with [3] aaabba=cab:

Critical pair: aaabbcab=cabaabba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [8].

Overlap of [3] aaabba=cab with [2] aba=c:

Critical pair: aaabbc=cabba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

Overlap of [2] aba=c with [3] aaabba=cab:

Critical pair: abcab=caabba.

Flip LHS and RHS.

Defines rule #5.

Simplify [5] ccabba=aaabbcab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

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

Overlap of [3] aaabba=cab with [8] aaabbcab=caaabbc:

Critical pair: aaabbcaaabbc=cabaabbcab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [2] aba=c with [8] aaabbcab=caaabbc:

Critical pair: abcaaabbc=caabbcab.

Flip LHS and RHS.

Defines rule #9.

Overlap of [8] aaabbcab=caaabbc with [2] aba=c:

Critical pair: aaabbcc=caaabbca.

Flip LHS and RHS.

Defines rule #6.

Referenced by [12], [13].

Overlap of [11] caaabbca=aaabbcc with [8] aaabbcab=caaabbc:

Critical pair: ccaaabbc=aaabbccb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [14], [15].

Overlap of [11] caaabbca=aaabbcc with [11] caaabbca=aaabbcc:

Critical pair: caaabbaaabbcc=aaabbccaabbca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [16], [17].

Overlap of [3] aaabba=cab with [12] aaabbccb=ccaaabbc:

Critical pair: aaabbccaaabbc=cabaabbccb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [2] aba=c with [12] aaabbccb=ccaaabbc:

Critical pair: abccaaabbc=caabbccb.

Flip LHS and RHS.

Defines rule #10.

Overlap of [3] aaabba=cab with [13] aaabbccaabbca=cccabbcc:

Critical pair: aaabbcccabbcc=cabaabbccaabbca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [2] aba=c with [13] aaabbccaabbca=cccabbcc:

Critical pair: abcccabbcc=caabbccaabbca.

Flip LHS and RHS.

Defines rule #14.