Certificate for #194 ⟨a, b | abbaab=a⟩

Back:⟨a, b | abbaab=a⟩

Completion settings:

[1] abbaab=a

Axiom: abbaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] abaab=abbaa

Overlap of [1] abbaab=a with [1] abbaab=a:

abba ab abbaab

Critical pair: abbaa=abaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaab=abaa

Overlap of [1] abbaab=a with [2] abaab=abbaa:

abba ab abaab

Critical pair: abbaabbaa=aaab.

Reduce LHS:

[1](abbaab)baa
⇒ abaa

Flip LHS and RHS.

Defines rule #1.