Certificate for #4258 ⟨a, b | abaabaaab=ba⟩

Completion settings:

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

Axiom: abaabaaab=ba.

Referenced by [4], [5], [18].

Axiom: baaabaa=c.

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

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

Critical pair: baaac=cabaa.

Referenced by [8], [17].

Overlap of [1] abaabaaab=ba with [2] baaabaa=c:

Critical pair: abaac=baaa.

Flip LHS and RHS.

Referenced by [5], [6], [7], [8], [12], [13].

Overlap of [2] baaabaa=c with [1] abaabaaab=ba:

Critical pair: baaba=cbaaab.

Reduce RHS:

Referenced by [11].

Overlap of [2] baaabaa=c with [4] baaa=abaac:

Critical pair: abaacbaa=c.

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

Overlap of [2] baaabaa=c with [4] baaa=abaac:

Critical pair: baaaabaac=ca.

Reduce LHS:

Referenced by [16].

Overlap of [3] baaac=cabaa with [4] baaa=abaac:

Critical pair: abaacc=cabaa.

Referenced by [10].

Overlap of [2] baaabaa=c with [6] abaacbaa=c:

Critical pair: baac=ccbaa.

Referenced by [10], [11], [12], [14], [15], [16], [17], [20].

Simplify [8] abaacc=cabaa.

Reduce LHS:

Referenced by [12].

Simplify [5] baaba=cabaacb.

Reduce RHS:

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

Overlap of [2] baaabaa=c with [11] baaba=caccbaab:

Critical pair: baaacaccbaab=cba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [14], [15], [16], [17], [18], [19], [20], [21].

Overlap of [11] baaba=caccbaab with [4] baaa=abaac:

Critical pair: baaabaac=caccbaabaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [18].

Overlap of [9] baac=ccbaa with [12] cba=caccb:

Critical pair: baacaccb=ccbaaba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [12] cba=caccb with [9] baac=ccbaa:

Critical pair: cccbaa=caccbac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [17], [19].

Simplify [7] abaacabaac=ca.

Reduce LHS:

Defines rule #2.

Referenced by [17], [19], [22], [23], [24], [25].

Overlap of [3] baaac=cabaa with [16] acccc=ca:

Critical pair: baaca=cabaaccc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [1] abaabaaab=ba with [11] baaba=caccbaab:

Critical pair: acaccbaabaab=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [19], [21], [22], [25].

Overlap of [2] baaabaa=c with [18] ba=accb:

Critical pair: accbaabaa=c.

Reduce LHS:

Defines rule #4.

Referenced by [25].

Simplify [9] baac=ccbaa.

Reduce RHS:

Referenced by [21].

Overlap of [20] baac=ccaccaccb with [18] ba=accb:

Critical pair: accbac=ccaccaccb.

Reduce LHS:

Referenced by [25].

Overlap of [18] ba=accb with [16] acccc=ca:

Critical pair: bca=accbcccc.

Referenced by [23].

Overlap of [22] bca=accbcccc with [16] acccc=ca:

Critical pair: bcca=accbcccccccc.

Referenced by [24].

Overlap of [23] bcca=accbcccccccc with [16] acccc=ca:

Critical pair: bccca=accbcccccccccccc.

Referenced by [25].

Overlap of [18] ba=accb with [19] acccacccaccaccaccbb=c:

Critical pair: bc=accbcccacccaccaccaccbb.

Reduce RHS:

Defines rule #1.