Certificate for #3801 ⟨a, b | abbaaabaab=a⟩

Back:⟨a, b | abbaaabaab=a⟩

Completion settings:

[1] abbaaabaab=a

Axiom: abbaaabaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] abaaabaab=abbaaabaa

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

abbaaaba ab abbaaabaab

Critical pair: abbaaabaa=abaaabaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaaabaab=abaaabaa

Overlap of [1] abbaaabaab=a with [2] abaaabaab=abbaaabaa:

abbaaaba ab abaaabaab

Critical pair: abbaaabaabbaaabaa=aaaabaab.

Reduce LHS:

[1](abbaaabaab)baaabaa
⇒ abaaabaa

Flip LHS and RHS.

Defines rule #1.