Certificate for #14514 ⟨a, b | aaab=b, babaa=b⟩

Completion settings:

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

Axiom: aaab=b.

Defines rule #2.

Referenced by [3], [4], [7], [8].

Axiom: babaa=b.

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

Overlap of [2] babaa=b with [1] aaab=b:

Critical pair: babb=bab.

Referenced by [5], [8].

Overlap of [2] babaa=b with [1] aaab=b:

Critical pair: babab=baab.

Referenced by [5], [6].

Overlap of [3] babb=bab with [2] babaa=b:

Critical pair: babb=bababaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [2] babaa=b with [5] baabaa=bab:

Critical pair: babab=bbaa.

Reduce LHS:

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

Overlap of [5] baabaa=bab with [1] aaab=b:

Critical pair: baabab=babaab.

Reduce LHS:

Reduce RHS:

Referenced by [8].

Overlap of [5] baabaa=bab with [5] baabaa=bab:

Critical pair: baabab=babbaa.

Reduce LHS:

Reduce RHS:

Defines rule #3.

Referenced by [9], [11].

Overlap of [8] bb=b with [5] baabaa=bab:

Critical pair: bbab=baabaa.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [10].

Overlap of [2] babaa=b with [9] bab=baaaa:

Critical pair: baaaaaa=b.

Defines rule #1.

Simplify [6] baab=bbaa.

Reduce RHS:

Defines rule #5.