Certificate for #4637 ⟨a, b | aababaab=aba⟩

Completion settings:

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

Axiom: aababaab=aba.

Referenced by [3].

Axiom: aabab=c.

Referenced by [3], [4].

Overlap of [1] aababaab=aba with [2] aabab=c:

Critical pair: caab=aba.

Flip LHS and RHS.

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

Overlap of [2] aabab=c with [3] aba=caab:

Critical pair: acaabb=c.

Referenced by [6], [8], [9], [10], [11], [17].

Overlap of [3] aba=caab with [3] aba=caab:

Critical pair: abcaab=caabba.

Referenced by [6], [9].

Overlap of [3] aba=caab with [4] acaabb=c:

Critical pair: abc=caabcaabb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [7], [11], [12], [13], [15], [16], [17], [18].

Overlap of [6] ccab=abc with [3] aba=caab:

Critical pair: cccaab=abca.

Flip LHS and RHS.

Referenced by [8], [9].

Overlap of [7] abca=cccaab with [4] acaabb=c:

Critical pair: abcc=cccaabcaabb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [14].

Simplify [5] abcaab=caabba.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [4] acaabb=c with [9] caabba=cccc:

Critical pair: acccc=ca.

Flip LHS and RHS.

Defines rule #1.

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

Overlap of [9] caabba=cccc with [4] acaabb=c:

Critical pair: caabbc=cccccaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [19].

Overlap of [9] caabba=cccc with [10] ca=acccc:

Critical pair: accccabba=cccc.

Reduce LHS:

Defines rule #8.

Referenced by [13], [15].

Overlap of [12] aabccba=cccc with [3] aba=caab:

Critical pair: aabccbcaab=ccccba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [19].

Simplify [8] cccaccccb=abcc.

Reduce LHS:

Referenced by [15].

Overlap of [9] caabba=cccc with [14] accccccccccccccccb=abcc:

Critical pair: caabbabcc=ccccccccccccccccccccb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19].

Simplify [3] aba=caab.

Reduce RHS:

Defines rule #5.

Referenced by [19].

Overlap of [4] acaabb=c with [10] ca=acccc:

Critical pair: aaccccabb=c.

Reduce LHS:

Defines rule #7.

Referenced by [19].

Overlap of [6] ccab=abc with [10] ca=acccc:

Critical pair: caccccb=abc.

Reduce LHS:

Defines rule #3.

Overlap of [13] ccccba=abcccc with [17] aaabccb=c:

Critical pair: ccccbc=abccccaabccb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.