Certificate for #22786 ⟨a, b | aaa=1, abaab=bba⟩

Completion settings:

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

Axiom: aaa=1.

Defines rule #1.

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

Axiom: abaab=bba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [5], [6], [7], [10], [12].

Overlap of [2] bba=abaab with [1] aaa=1:

Critical pair: bb=abaabaa.

Flip LHS and RHS.

Referenced by [4], [5].

Overlap of [1] aaa=1 with [3] abaabaa=bb:

Critical pair: aabb=baabaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [12].

Overlap of [3] abaabaa=bb with [3] abaabaa=bb:

Critical pair: ababb=bbbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [7], [12].

Overlap of [2] bba=abaab with [4] baabaa=aabb:

Critical pair: baabb=abaababaa.

Flip LHS and RHS.

Referenced by [8].

Overlap of [2] bba=abaab with [5] babaaba=ababb:

Critical pair: bababb=abaabbaaba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [1] aaa=1 with [6] abaababaa=baabb:

Critical pair: aabaabb=baababaa.

Flip LHS and RHS.

Defines rule #5.

Overlap of [1] aaa=1 with [7] aabaabababa=bababb:

Critical pair: abababb=baabababa.

Flip LHS and RHS.

Defines rule #6.

Referenced by [10].

Overlap of [2] bba=abaab with [9] baabababa=abababb:

Critical pair: babababb=abaababababa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [1] aaa=1 with [10] aababababaab=babababb:

Critical pair: ababababb=babababaab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [12].

Overlap of [2] bba=abaab with [11] babababaab=ababababb:

Critical pair: bababababb=abaabbababaab.

Reduce RHS:

Defines rule #8.