Certificate for #3797 ⟨a, b | abbaaaaaab=a⟩

Back:⟨a, b | abbaaaaaab=a⟩

Completion settings:

[1] abbaaaaaab=a

Axiom: abbaaaaaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] abaaaaaab=abbaaaaaa

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

abbaaaaa ab abbaaaaaab

Critical pair: abbaaaaaa=abaaaaaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaaaaaab=abaaaaaa

Overlap of [1] abbaaaaaab=a with [2] abaaaaaab=abbaaaaaa:

abbaaaaa ab abaaaaaab

Critical pair: abbaaaaaabbaaaaaa=aaaaaaab.

Reduce LHS:

[1](abbaaaaaab)baaaaaa
⇒ abaaaaaa

Flip LHS and RHS.

Defines rule #1.