Certificate for #2525 ⟨a, b | aabbaa=abab⟩

Completion settings:

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

Axiom: aabbaa=abab.

Referenced by [3].

Axiom: abab=c.

Defines rule #1.

Referenced by [3], [4], [7], [9], [20].

Simplify [1] aabbaa=abab.

Reduce RHS:

Defines rule #2.

Referenced by [5], [6], [7], [8], [12], [13], [18], [19].

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

Critical pair: abc=cab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [8], [10], [12], [19].

Overlap of [3] aabbaa=c with [3] aabbaa=c:

Critical pair: aabbc=cbbaa.

Flip LHS and RHS.

Defines rule #5.

Overlap of [3] aabbaa=c with [3] aabbaa=c:

Critical pair: aabbac=cabbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [8], [9], [10], [11], [14], [15], [17], [19].

Overlap of [3] aabbaa=c with [2] abab=c:

Critical pair: aabbac=cbab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [11].

Overlap of [3] aabbaa=c with [6] abcbaa=aabbac:

Critical pair: aabbaaabbac=cbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [16].

Overlap of [2] abab=c with [6] abcbaa=aabbac:

Critical pair: abaabbac=ccbaa.

Defines rule #7.

Referenced by [12], [13], [15], [20], [21].

Overlap of [4] cab=abc with [6] abcbaa=aabbac:

Critical pair: caabbac=abccbaa.

Defines rule #8.

Overlap of [7] cbab=aabbac with [6] abcbaa=aabbac:

Critical pair: cbaabbac=aabbaccbaa.

Defines rule #11.

Referenced by [15], [16].

Overlap of [9] abaabbac=ccbaa with [4] cab=abc:

Critical pair: abaabbaabc=ccbaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [13], [14].

Overlap of [9] abaabbac=ccbaa with [12] ccbaaab=abcbc:

Critical pair: abaabbaabcbc=ccbaacbaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [17].

Overlap of [12] ccbaaab=abcbc with [6] abcbaa=aabbac:

Critical pair: ccbaaaabbac=abcbccbaa.

Defines rule #13.

Overlap of [6] abcbaa=aabbac with [11] cbaabbac=aabbaccbaa:

Critical pair: abaabbaccbaa=aabbacbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

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

Overlap of [8] cbcbaa=abcbac with [11] cbaabbac=aabbaccbaa:

Critical pair: cbaabbaccbaa=abcbacbbac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [20].

Overlap of [13] ccbaacbaaab=abcbcbc with [6] abcbaa=aabbac:

Critical pair: ccbaacbaaaabbac=abcbcbccbaa.

Defines rule #19.

Overlap of [3] aabbaa=c with [15] aabbacbbac=ccbaacbaa:

Critical pair: aabbccbaacbaa=cbbacbbac.

Flip LHS and RHS.

Defines rule #16.

Overlap of [6] abcbaa=aabbac with [15] aabbacbbac=ccbaacbaa:

Critical pair: abcbaccbaacbaa=aabbacabbacbbac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [2] abab=c with [16] abcbacbbac=aabbaccbaacbaa:

Critical pair: abaabbaccbaacbaa=ccbacbbac.

Reduce LHS:

Defines rule #17.

Referenced by [21], [22].

Overlap of [9] abaabbac=ccbaa with [20] ccbaacbaacbaa=ccbacbbac:

Critical pair: abaabbaccbacbbac=ccbaacbaacbaacbaa.

Reduce LHS:

Reduce RHS:

Defines rule #20.

Overlap of [15] aabbacbbac=ccbaacbaa with [20] ccbaacbaacbaa=ccbacbbac:

Critical pair: aabbacbbaccbacbbac=ccbaacbaacbaacbaacbaa.

Reduce LHS:

Reduce RHS:

Defines rule #21.