Certificate for #4250 ⟨a, b | abaaabbab=ba⟩

Completion settings:

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

Axiom: abaaabbab=ba.

Referenced by [3].

Axiom: bba=c.

Defines rule #5.

Referenced by [3], [4], [5], [7], [9], [12].

Overlap of [1] abaaabbab=ba with [2] bba=c:

Critical pair: abaaacb=ba.

Defines rule #2.

Referenced by [4], [5], [6], [10], [12], [14].

Overlap of [2] bba=c with [3] abaaacb=ba:

Critical pair: bbba=cbaaacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [7], [8], [11], [15], [16], [18].

Overlap of [3] abaaacb=ba with [2] bba=c:

Critical pair: abaaacc=baba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [9], [10], [11], [12], [13], [17], [19].

Overlap of [3] abaaacb=ba with [4] cbaaacb=bc:

Critical pair: abaaabc=baaaacb.

Defines rule #9.

Overlap of [4] cbaaacb=bc with [2] bba=c:

Critical pair: cbaaacc=bcba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [14], [15], [16], [17].

Overlap of [4] cbaaacb=bc with [4] cbaaacb=bc:

Critical pair: cbaaabc=bcaaacb.

Defines rule #10.

Overlap of [2] bba=c with [5] baba=abaaacc:

Critical pair: babaaacc=cba.

Reduce LHS:

Defines rule #1.

Overlap of [3] abaaacb=ba with [5] baba=abaaacc:

Critical pair: abaaacabaaacc=baaba.

Defines rule #14.

Overlap of [4] cbaaacb=bc with [5] baba=abaaacc:

Critical pair: cbaaacabaaacc=bcaba.

Defines rule #15.

Overlap of [5] baba=abaaacc with [3] abaaacb=ba:

Critical pair: bba=abaaaccaacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [18], [19].

Overlap of [5] baba=abaaacc with [5] baba=abaaacc:

Critical pair: baabaaacc=abaaaccba.

Defines rule #12.

Overlap of [3] abaaacb=ba with [7] bcba=cbaaacc:

Critical pair: abaaaccbaaacc=bacba.

Defines rule #16.

Overlap of [4] cbaaacb=bc with [7] bcba=cbaaacc:

Critical pair: cbaaaccbaaacc=bccba.

Defines rule #17.

Overlap of [7] bcba=cbaaacc with [4] cbaaacb=bc:

Critical pair: bbc=cbaaaccaacb.

Defines rule #8.

Overlap of [7] bcba=cbaaacc with [5] baba=abaaacc:

Critical pair: bcabaaacc=cbaaaccba.

Defines rule #13.

Overlap of [12] abaaaccaacb=c with [4] cbaaacb=bc:

Critical pair: abaaaccaabc=caaacb.

Defines rule #11.

Overlap of [12] abaaaccaacb=c with [5] baba=abaaacc:

Critical pair: abaaaccaacabaaacc=caba.

Defines rule #18.