Certificate for #5922 ⟨a, b | abbaab=baaba⟩

Completion settings:

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

Axiom: abbaab=baaba.

Defines rule #4.

Referenced by [4], [5], [6], [7], [8], [9], [11], [12].

Axiom: baabaa=c.

Defines rule #6.

Referenced by [3], [5], [6], [9], [10], [11], [12].

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

Critical pair: baac=cbaa.

Defines rule #2.

Overlap of [1] abbaab=baaba with [1] abbaab=baaba:

Critical pair: abbabaaba=baababaab.

Flip LHS and RHS.

Defines rule #9.

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

Overlap of [1] abbaab=baaba with [2] baabaa=c:

Critical pair: abc=baabaaa.

Reduce RHS:

Defines rule #1.

Referenced by [7].

Overlap of [2] baabaa=c with [1] abbaab=baaba:

Critical pair: baababaaba=cbbaab.

Reduce LHS:

Defines rule #3.

Referenced by [7], [8].

Overlap of [1] abbaab=baaba with [5] abc=ca:

Critical pair: abbaca=baabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [1] abbaab=baaba with [6] abbac=cbbaab:

Critical pair: abbacbbaab=baababac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Overlap of [1] abbaab=baaba with [4] baababaab=abbabaaba:

Critical pair: ababbabaaba=baabaabaab.

Reduce RHS:

Defines rule #11.

Referenced by [11].

Overlap of [2] baabaa=c with [4] baababaab=abbabaaba:

Critical pair: baaabbabaaba=cbabaab.

Defines rule #12.

Referenced by [12].

Overlap of [9] ababbabaaba=cbaab with [1] abbaab=baaba:

Critical pair: ababbabaabbaaba=cbaabbbaab.

Reduce LHS:

Defines rule #8.

Overlap of [10] baaabbabaaba=cbabaab with [1] abbaab=baaba:

Critical pair: baaabbabaabbaaba=cbabaabbbaab.

Reduce LHS:

Defines rule #10.