Certificate for #1799 ⟨a, b | abbaaaaab=a⟩

Back:⟨a, b | abbaaaaab=a⟩

Completion settings:

[1] abbaaaaab=a

Axiom: abbaaaaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] abaaaaab=abbaaaaa

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

abbaaaa ab abbaaaaab

Critical pair: abbaaaaa=abaaaaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaaaaab=abaaaaa

Overlap of [1] abbaaaaab=a with [2] abaaaaab=abbaaaaa:

abbaaaa ab abaaaaab

Critical pair: abbaaaaabbaaaaa=aaaaaab.

Reduce LHS:

[1](abbaaaaab)baaaaa
⇒ abaaaaa

Flip LHS and RHS.

Defines rule #1.