Certificate for #3461 ⟨a, b | aaabababaa=a⟩

Completion settings:

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

Axiom: aaabababaa=a.

Referenced by [3].

Axiom: ababa=c.

Referenced by [3], [4], [5], [6], [8], [13], [15], [16].

Overlap of [1] aaabababaa=a with [2] ababa=c:

Critical pair: aacbaa=a.

Referenced by [5], [6], [7], [9], [12], [17].

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

Critical pair: abc=cba.

Defines rule #3.

Referenced by [10], [13], [21], [25].

Overlap of [2] ababa=c with [3] aacbaa=a:

Critical pair: ababa=cacbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9], [10], [18].

Overlap of [3] aacbaa=a with [2] ababa=c:

Critical pair: aacbac=ababa.

Reduce RHS:

Referenced by [11].

Overlap of [3] aacbaa=a with [3] aacbaa=a:

Critical pair: aacba=acbaa.

Referenced by [10], [11], [13], [17].

Overlap of [5] cacbaa=c with [2] ababa=c:

Critical pair: cacbac=cbaba.

Flip LHS and RHS.

Referenced by [13], [19].

Overlap of [5] cacbaa=c with [3] aacbaa=a:

Critical pair: cacba=ccbaa.

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

Overlap of [5] cacbaa=c with [4] abc=cba:

Critical pair: cacbacba=cbc.

Reduce LHS:

Referenced by [13].

Simplify [6] aacbac=c.

Reduce LHS:

Referenced by [12], [14].

Overlap of [11] acbaac=c with [3] aacbaa=a:

Critical pair: acba=cbaa.

Defines rule #6.

Referenced by [13], [14], [15], [17], [22], [23].

Overlap of [2] ababa=c with [12] acba=cbaa:

Critical pair: ababcbaa=ccba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [11] acbaac=c with [12] acba=cbaa:

Critical pair: cbaaac=c.

Defines rule #8.

Referenced by [23].

Overlap of [12] acba=cbaa with [2] ababa=c:

Critical pair: acbc=cbaababa.

Reduce RHS:

Defines rule #4.

Referenced by [20].

Overlap of [13] ccba=cbca with [2] ababa=c:

Critical pair: ccbc=cbcababa.

Reduce RHS:

Defines rule #1.

Overlap of [3] aacbaa=a with [7] aacba=acbaa:

Critical pair: acbaaa=a.

Reduce LHS:

Defines rule #10.

Referenced by [21], [25].

Overlap of [5] cacbaa=c with [9] cacba=ccbaa:

Critical pair: ccbaaa=c.

Reduce LHS:

Referenced by [20].

Simplify [8] cbaba=cacbac.

Reduce RHS:

Referenced by [21].

Overlap of [15] acbc=cbac with [18] cbcaaa=c:

Critical pair: ac=cbacaaa.

Flip LHS and RHS.

Referenced by [22].

Overlap of [4] abc=cba with [17] cbaaaa=a:

Critical pair: aba=cbabaaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [12] acba=cbaa with [20] cbacaaa=ac:

Critical pair: aac=cbaacaaa.

Flip LHS and RHS.

Referenced by [23], [24].

Overlap of [12] acba=cbaa with [22] cbaacaaa=aac:

Critical pair: aaac=cbaaacaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [25].

Overlap of [13] ccba=cbca with [22] cbaacaaa=aac:

Critical pair: caac=cbcaacaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [25].

Overlap of [4] abc=cba with [23] caaa=aaac:

Critical pair: abaaac=cbaaaa.

Reduce LHS:

Reduce RHS:

Defines rule #9.