Certificate for #14647 ⟨a, b | aaba=b, babbb=a⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with a < b

Axiom: aaba=b.

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

Axiom: babbb=a.

Referenced by [4], [13].

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

Critical pair: aabb=baba.

Flip LHS and RHS.

Referenced by [10].

Overlap of [1] aaba=b with [2] babbb=a:

Critical pair: aaa=bbbb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [10], [13].

Overlap of [4] bbbb=aaa with [4] bbbb=aaa:

Critical pair: baaa=aaab.

Referenced by [6], [7], [11].

Overlap of [1] aaba=b with [5] baaa=aaab:

Critical pair: aaaaab=baa.

Referenced by [10].

Overlap of [5] baaa=aaab with [1] aaba=b:

Critical pair: baab=aaababa.

Reduce RHS:

Referenced by [8].

Overlap of [7] baab=abba with [1] aaba=b:

Critical pair: bb=abbaa.

Flip LHS and RHS.

Referenced by [9].

Overlap of [1] aaba=b with [8] abbaa=bb:

Critical pair: aabbb=bbbaa.

Flip LHS and RHS.

Referenced by [10].

Overlap of [4] bbbb=aaa with [3] baba=aabb:

Critical pair: bbbaabb=aaaaba.

Reduce LHS:

Reduce RHS:

Referenced by [11].

Overlap of [5] baaa=aaab with [10] baa=aab:

Critical pair: aaba=aaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [12].

Overlap of [11] aaab=b with [1] aaba=b:

Critical pair: ab=ba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [13].

Overlap of [2] babbb=a with [12] ba=ab:

Critical pair: abbbb=a.

Reduce LHS:

Defines rule #2.