Certificate for #12186 ⟨a, b | aaaa=ab, babb=a⟩

Completion settings:

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

Axiom: aaaa=ab.

Defines rule #2.

Referenced by [3], [5].

Axiom: babb=a.

Referenced by [4], [6], [7], [8].

Overlap of [1] aaaa=ab with [1] aaaa=ab:

Critical pair: aab=aba.

Flip LHS and RHS.

Referenced by [4].

Overlap of [3] aba=aab with [2] babb=a:

Critical pair: aa=aabbb.

Flip LHS and RHS.

Referenced by [5].

Overlap of [1] aaaa=ab with [4] aabbb=aa:

Critical pair: aaaa=abbbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [6].

Overlap of [2] babb=a with [5] abbbb=ab:

Critical pair: bab=abb.

Referenced by [7].

Overlap of [2] babb=a with [6] bab=abb:

Critical pair: abbb=a.

Defines rule #3.

Referenced by [8].

Overlap of [2] babb=a with [7] abbb=a:

Critical pair: ba=ab.

Defines rule #1.