Certificate for #1693 ⟨a, b | aabababaa=a⟩

Completion settings:

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

Axiom: aabababaa=a.

Referenced by [3].

Axiom: ababa=c.

Referenced by [3], [4], [5], [6], [7], [12], [13].

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

Critical pair: acbaa=a.

Referenced by [5], [6], [9], [14].

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

Critical pair: abc=cba.

Defines rule #3.

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

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

Critical pair: ababa=ccbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [7], [8], [10], [16].

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

Critical pair: acbac=ababa.

Reduce RHS:

Referenced by [9], [10], [11].

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

Critical pair: ccbac=cbaba.

Flip LHS and RHS.

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

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

Critical pair: ccbacba=cbc.

Referenced by [12], [13].

Overlap of [6] acbac=c with [3] acbaa=a:

Critical pair: acba=cbaa.

Defines rule #9.

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

Overlap of [6] acbac=c with [5] ccbaa=c:

Critical pair: acbac=ccbaa.

Reduce LHS:

Reduce RHS:

Defines rule #7.

Referenced by [18].

Overlap of [6] acbac=c with [6] acbac=c:

Critical pair: acbc=cbac.

Defines rule #4.

Referenced by [12], [17].

Overlap of [2] ababa=c with [11] acbc=cbac:

Critical pair: ababcbac=ccbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

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

Critical pair: ababcbaa=ccba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [3] acbaa=a with [9] acba=cbaa:

Critical pair: cbaaa=a.

Defines rule #10.

Referenced by [15], [20].

Overlap of [4] abc=cba with [14] cbaaa=a:

Critical pair: aba=cbabaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [5] ccbaa=c with [13] ccba=cbca:

Critical pair: cbcaa=c.

Referenced by [17].

Overlap of [11] acbc=cbac with [16] cbcaa=c:

Critical pair: ac=cbacaa.

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [9] acba=cbaa with [17] cbacaa=ac:

Critical pair: aac=cbaacaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [20].

Overlap of [13] ccba=cbca with [17] cbacaa=ac:

Critical pair: cac=cbcacaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [20].

Overlap of [4] abc=cba with [18] caa=aac:

Critical pair: abaac=cbaaa.

Reduce LHS:

Reduce RHS:

Defines rule #6.