Certificate for #1615 ⟨a, b | aaabaabaa=a⟩

Completion settings:

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

Axiom: aaabaabaa=a.

Referenced by [3].

Axiom: aa=c.

Defines rule #8.

Referenced by [3], [4], [5], [6], [8], [9], [10].

Overlap of [1] aaabaabaa=a with [2] aa=c:

Critical pair: cabaabaa=a.

Reduce LHS:

Referenced by [5], [6], [7], [8], [9], [10], [11], [13].

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

Critical pair: ac=ca.

Defines rule #5.

Referenced by [6], [10].

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

Critical pair: cabcba=aabcbc.

Reduce RHS:

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

Overlap of [4] ac=ca with [3] cabcbc=a:

Critical pair: aa=caabcbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [7], [12], [14].

Overlap of [6] ccbcbc=c with [3] cabcbc=a:

Critical pair: ccbcba=cabcbc.

Reduce RHS:

Defines rule #4.

Overlap of [3] cabcbc=a with [5] cabcba=cbcbc:

Critical pair: cabcbcbcbc=aabcba.

Reduce LHS:

Reduce RHS:

Defines rule #7.

Overlap of [5] cabcba=cbcbc with [2] aa=c:

Critical pair: cabcbc=cbcbca.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [5] cabcba=cbcbc with [4] ac=ca:

Critical pair: cabcbca=cbcbcc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11], [12].

Overlap of [3] cabcbc=a with [10] cbcbcc=c:

Critical pair: cabc=abcc.

Flip LHS and RHS.

Defines rule #6.

Overlap of [6] ccbcbc=c with [10] cbcbcc=c:

Critical pair: ccbc=cbcc.

Flip LHS and RHS.

Defines rule #1.

Overlap of [3] cabcbc=a with [9] cbcbca=a:

Critical pair: caba=abca.

Flip LHS and RHS.

Defines rule #9.

Overlap of [6] ccbcbc=c with [9] cbcbca=a:

Critical pair: ccba=cbca.

Flip LHS and RHS.

Defines rule #3.

Overlap of [9] cbcbca=a with [5] cabcba=cbcbc:

Critical pair: cbcbcbcbc=abcba.

Flip LHS and RHS.

Defines rule #10.