Certificate for #3809 ⟨a, b | abbaabbaab=a⟩

Back:⟨a, b | abbaabbaab=a⟩

Completion settings:

[1] abbaabbaab=a

Axiom: abbaabbaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] abaab=abbaa

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

abba abbaab abbaabbaab

Critical pair: abbaa=abaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaab=abaa

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

abbaabba ab abaab

Critical pair: abbaabbaabbaa=aaab.

Reduce LHS:

[1](abbaabbaab)baa
⇒ abaa

Flip LHS and RHS.

Defines rule #1.