Certificate for #12500 ⟨a, b | abab=aa, abbb=a⟩

Completion settings:

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

Axiom: abab=aa.

Referenced by [3], [4].

Axiom: abbb=a.

Defines rule #1.

Referenced by [4].

Overlap of [1] abab=aa with [1] abab=aa:

Critical pair: abaa=aaab.

Referenced by [5].

Overlap of [1] abab=aa with [2] abbb=a:

Critical pair: aba=aabb.

Defines rule #2.

Referenced by [5].

Simplify [3] abaa=aaab.

Reduce LHS:

Defines rule #3.