Certificate for #13115 ⟨a, b | bbb=aaa, aaba=b⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(b) = 0; deg(a) = 1

Axiom: bbb=aaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5], [6], [10], [11].

Axiom: aaba=b.

Referenced by [3], [5], [6], [10], [11], [13].

Overlap of [2] aaba=b with [2] aaba=b:

Critical pair: aabb=baba.

Flip LHS and RHS.

Referenced by [9].

Overlap of [1] aaa=bbb with [1] aaa=bbb:

Critical pair: abbb=bbba.

Flip LHS and RHS.

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

Overlap of [1] aaa=bbb with [2] aaba=b:

Critical pair: ab=bbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [7], [8], [9].

Overlap of [2] aaba=b with [1] aaa=bbb:

Critical pair: aabbbb=baa.

Flip LHS and RHS.

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

Overlap of [5] babbb=ab with [5] babbb=ab:

Critical pair: babbab=ababbb.

Reduce RHS:

Referenced by [12].

Overlap of [5] babbb=ab with [4] bbba=abbb:

Critical pair: baabbb=aba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

Overlap of [5] babbb=ab with [4] bbba=abbb:

Critical pair: bababbb=abba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11], [12].

Overlap of [2] aaba=b with [6] baa=aabbbb:

Critical pair: aaaabbbb=ba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [12].

Overlap of [6] baa=aabbbb with [2] aaba=b:

Critical pair: bb=aabbbbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12].

Simplify [7] babbab=aab.

Reduce LHS:

Referenced by [13].

Overlap of [12] aabbbbbbbbbb=aab with [4] bbba=abbb:

Critical pair: aabbbbbbbabbb=aaba.

Reduce LHS:

Reduce RHS:

Defines rule #1.