Certificate for #19276 ⟨a, b | aaa=a, abbab=bb⟩

Completion settings:

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

Axiom: aaa=a.

Defines rule #4.

Referenced by [3].

Axiom: abbab=bb.

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

Overlap of [1] aaa=a with [2] abbab=bb:

Critical pair: aabb=abbab.

Reduce RHS:

Referenced by [4].

Overlap of [3] aabb=bb with [2] abbab=bb:

Critical pair: abb=bbab.

Defines rule #2.

Referenced by [5], [6].

Overlap of [2] abbab=bb with [4] abb=bbab:

Critical pair: bbabab=bb.

Defines rule #3.

Referenced by [6].

Overlap of [2] abbab=bb with [4] abb=bbab:

Critical pair: abbbbab=bbb.

Reduce LHS:

Defines rule #1.