Certificate for #12585 ⟨a, b | abba=ab, bbbb=b⟩

Back:⟨a, b | abba=ab, bbbb=b⟩

Completion settings:

[1] abba=ab

Axiom: abba=ab.

Defines rule #3.

Referenced by [3], [4].

[2] bbbb=b

Axiom: bbbb=b.

Defines rule #1.

Referenced by [4].

[3] abbba=abb

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

abb a abba

Critical pair: abbab=abbba.

Reduce LHS:

[1](abba)b
⇒ abb

Flip LHS and RHS.

Defines rule #4.

Referenced by [4].

[4] aba=abbb

Overlap of [1] abba=ab with [3] abbba=abb:

abb a abbba

Critical pair: abbabb=abbbba.

Reduce LHS:

[1](abba)bb
⇒ abbb

Reduce RHS:

[2]a(bbbb)a
⇒ aba

Flip LHS and RHS.

Defines rule #2.