Certificate for #20135 ⟨a, b | aab=b, baba=bbb⟩

Completion settings:

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

Axiom: aab=b.

Defines rule #1.

Referenced by [4], [5], [6], [7].

Axiom: baba=bbb.

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [2] bbb=baba with [2] bbb=baba:

Critical pair: bbaba=babab.

Flip LHS and RHS.

Defines rule #5.

Referenced by [4], [5], [6], [7].

Overlap of [2] bbb=baba with [3] babab=bbaba:

Critical pair: bbbbaba=babaabab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [5], [7].

Overlap of [3] babab=bbaba with [3] babab=bbaba:

Critical pair: babbaba=bbabaab.

Reduce LHS:

Reduce RHS:

Defines rule #6.

Referenced by [6].

Overlap of [2] bbb=baba with [5] bbabbaa=bbabb:

Critical pair: bbbabb=babaabbaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [2] bbb=baba with [4] babbab=bbabba:

Critical pair: bbbbabba=babaabbab.

Reduce LHS:

Reduce RHS:

Defines rule #4.