Certificate for #3999 ⟨a, b | aaababbaa=ab⟩

Completion settings:

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

Axiom: aaababbaa=ab.

Referenced by [3].

Axiom: abb=c.

Defines rule #4.

Referenced by [3], [4], [6], [7], [9], [13], [14].

Overlap of [1] aaababbaa=ab with [2] abb=c:

Critical pair: aaabcaa=ab.

Defines rule #1.

Referenced by [4], [5], [6], [7], [8], [9], [11], [12], [14], [19], [20], [21].

Overlap of [3] aaabcaa=ab with [2] abb=c:

Critical pair: aaabcac=abbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

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

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

Critical pair: aaabcab=ababcaa.

Defines rule #7.

Referenced by [13], [16].

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

Critical pair: aaabcaab=abaabcaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [7], [8], [10], [22], [23].

Overlap of [3] aaabcaa=ab with [6] abaabcaa=c:

Critical pair: aaabcac=abbaabcaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [6] abaabcaa=c with [3] aaabcaa=ab:

Critical pair: abaabcab=cabcaa.

Defines rule #15.

Referenced by [18].

Overlap of [3] aaabcaa=ab with [7] caabcaa=aaabcac:

Critical pair: aaabaaabcac=abbcaa.

Reduce RHS:

Defines rule #6.

Referenced by [19].

Overlap of [6] abaabcaa=c with [7] caabcaa=aaabcac:

Critical pair: abaabaaabcac=cbcaa.

Reduce RHS:

Defines rule #14.

Overlap of [7] caabcaa=aaabcac with [3] aaabcaa=ab:

Critical pair: caabcab=aaabcacabcaa.

Defines rule #11.

Referenced by [24].

Overlap of [7] caabcaa=aaabcac with [7] caabcaa=aaabcac:

Critical pair: caabaaabcac=aaabcacbcaa.

Reduce RHS:

Defines rule #10.

Overlap of [5] aaabcab=ababcaa with [2] abb=c:

Critical pair: aaabcc=ababcaab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [14], [15].

Overlap of [3] aaabcaa=ab with [13] ababcaab=aaabcc:

Critical pair: aaabcaaaabcc=abbabcaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [16], [17], [18], [24].

Overlap of [13] ababcaab=aaabcc with [7] caabcaa=aaabcac:

Critical pair: ababaaabcac=aaabcccaa.

Defines rule #12.

Overlap of [5] aaabcab=ababcaa with [14] cabcaab=abaabcc:

Critical pair: aaababaabcc=ababcaacaab.

Defines rule #16.

Overlap of [14] cabcaab=abaabcc with [7] caabcaa=aaabcac:

Critical pair: cabaaabcac=abaabcccaa.

Defines rule #8.

Overlap of [8] abaabcab=cabcaa with [14] cabcaab=abaabcc:

Critical pair: abaababaabcc=cabcaacaab.

Defines rule #22.

Overlap of [9] aaabaaabcac=ccaa with [4] cb=aaabcac:

Critical pair: aaabaaabcaaaabcac=ccaab.

Reduce LHS:

Defines rule #17.

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

Overlap of [3] aaabcaa=ab with [19] aaababaabcac=ccaab:

Critical pair: aaabcccaab=abababaabcac.

Flip LHS and RHS.

Defines rule #21.

Overlap of [3] aaabcaa=ab with [19] aaababaabcac=ccaab:

Critical pair: aaabcaccaab=abaababaabcac.

Flip LHS and RHS.

Defines rule #23.

Overlap of [6] abaabcaa=c with [19] aaababaabcac=ccaab:

Critical pair: abaabcccaab=cababaabcac.

Flip LHS and RHS.

Defines rule #18.

Overlap of [6] abaabcaa=c with [19] aaababaabcac=ccaab:

Critical pair: abaabcaccaab=caababaabcac.

Flip LHS and RHS.

Defines rule #20.

Overlap of [11] caabcab=aaabcacabcaa with [14] cabcaab=abaabcc:

Critical pair: caababaabcc=aaabcacabcaacaab.

Defines rule #19.