Certificate for #857 ⟨a, b | abbaaaab=a⟩

Back:⟨a, b | abbaaaab=a⟩

Completion settings:

[1] abbaaaab=a

Axiom: abbaaaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] abaaaab=abbaaaa

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

abbaaa ab abbaaaab

Critical pair: abbaaaa=abaaaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaaaab=abaaaa

Overlap of [1] abbaaaab=a with [2] abaaaab=abbaaaa:

abbaaa ab abaaaab

Critical pair: abbaaaabbaaaa=aaaaab.

Reduce LHS:

[1](abbaaaab)baaaa
⇒ abaaaa

Flip LHS and RHS.

Defines rule #1.