Certificate for #5228 ⟨a, b | aabbaba=abab⟩

Completion settings:

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

Axiom: aabbaba=abab.

Referenced by [3].

Axiom: abba=c.

Defines rule #3.

Referenced by [3], [4], [5], [6], [8].

Overlap of [1] aabbaba=abab with [2] abba=c:

Critical pair: acba=abab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6], [7], [9], [18], [20], [22].

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

Critical pair: abbc=cbba.

Flip LHS and RHS.

Defines rule #5.

Overlap of [2] abba=c with [3] abab=acba:

Critical pair: abbacba=cbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [6], [8], [9], [12], [14], [15], [17], [19], [21], [23].

Overlap of [3] abab=acba with [2] abba=c:

Critical pair: abc=acbaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [10], [13], [16].

Overlap of [3] abab=acba with [3] abab=acba:

Critical pair: abacba=acbaab.

Flip LHS and RHS.

Defines rule #7.

Overlap of [5] cbab=ccba with [2] abba=c:

Critical pair: cbc=ccbaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [11].

Overlap of [5] cbab=ccba with [3] abab=acba:

Critical pair: cbacba=ccbaab.

Flip LHS and RHS.

Defines rule #9.

Referenced by [10], [11].

Overlap of [6] accbaa=abc with [9] ccbaab=cbacba:

Critical pair: acbacba=abcb.

Defines rule #8.

Referenced by [12], [13], [14], [17].

Overlap of [8] cccbaa=cbc with [9] ccbaab=cbacba:

Critical pair: ccbacba=cbcb.

Defines rule #10.

Referenced by [15], [16], [17].

Overlap of [10] acbacba=abcb with [5] cbab=ccba:

Critical pair: acbaccba=abcbb.

Flip LHS and RHS.

Defines rule #11.

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

Overlap of [10] acbacba=abcb with [6] accbaa=abc:

Critical pair: acbacbabc=abcbccbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [22], [23].

Overlap of [10] acbacba=abcb with [10] acbacba=abcb:

Critical pair: acbabcb=abcbcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [20], [21].

Overlap of [11] ccbacba=cbcb with [5] cbab=ccba:

Critical pair: ccbaccba=cbcbb.

Flip LHS and RHS.

Defines rule #14.

Referenced by [16].

Overlap of [11] ccbacba=cbcb with [6] accbaa=abc:

Critical pair: ccbacbabc=cbcbccbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [11] ccbacba=cbcb with [10] acbacba=abcb:

Critical pair: ccbabcb=cbcbcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [3] abab=acba with [12] abcbb=acbaccba:

Critical pair: abacbaccba=acbacbb.

Flip LHS and RHS.

Defines rule #17.

Overlap of [5] cbab=ccba with [12] abcbb=acbaccba:

Critical pair: cbacbaccba=ccbacbb.

Flip LHS and RHS.

Defines rule #20.

Overlap of [3] abab=acba with [14] abcbcba=accbacb:

Critical pair: abaccbacb=acbacbcba.

Flip LHS and RHS.

Defines rule #18.

Overlap of [5] cbab=ccba with [14] abcbcba=accbacb:

Critical pair: cbaccbacb=ccbacbcba.

Flip LHS and RHS.

Defines rule #21.

Overlap of [3] abab=acba with [13] abcbccbaa=acbaccbac:

Critical pair: abacbaccbac=acbacbccbaa.

Flip LHS and RHS.

Defines rule #19.

Overlap of [5] cbab=ccba with [13] abcbccbaa=acbaccbac:

Critical pair: cbacbaccbac=ccbacbccbaa.

Flip LHS and RHS.

Defines rule #22.