Certificate for #407 ⟨a, b | abbaaab=a⟩

Back:⟨a, b | abbaaab=a⟩

Completion settings:

[1] abbaaab=a

Axiom: abbaaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] abaaab=abbaaa

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

abbaa ab abbaaab

Critical pair: abbaaa=abaaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaaab=abaaa

Overlap of [1] abbaaab=a with [2] abaaab=abbaaa:

abbaa ab abaaab

Critical pair: abbaaabbaaa=aaaab.

Reduce LHS:

[1](abbaaab)baaa
⇒ abaaa

Flip LHS and RHS.

Defines rule #1.