Certificate for #5919 ⟨a, b | abbaab=abbaa⟩

Back:⟨a, b | abbaab=abbaa⟩

Completion settings:

[1] abbaab=abbaa

Axiom: abbaab=abbaa.

Referenced by [3].

[2] abbaa=c

Axiom: abbaa=c.

Defines rule #3.

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

[3] abbaab=c

Simplify [1] abbaab=abbaa.

Reduce RHS:

[2](abbaa)
⇒ c

Referenced by [4].

[4] cb=c

Overlap of [3] abbaab=c with [2] abbaa=c:

abbaab abbaa

Critical pair: cb=c.

Defines rule #1.

Referenced by [5].

[5] caa=abbac

Overlap of [2] abbaa=c with [2] abbaa=c:

abba a abbaa

Critical pair: abbac=cbbaa.

Reduce RHS:

[4](cb)baa
[4]⇒ (cb)aa
⇒ caa

Flip LHS and RHS.

Defines rule #2.