Certificate for #1687 ⟨a, b | aababaaab=a⟩

Back:⟨a, b | aababaaab=a⟩

Completion settings:

[1] aababaaab=a

Axiom: aababaaab=a.

Defines rule #3.

Referenced by [2], [3].

[2] aabaaab=aababaa

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

aababa aab aababaaab

Critical pair: aababaa=aabaaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaaab=aabaa

Overlap of [1] aababaaab=a with [2] aabaaab=aababaa:

aababa aab aabaaab

Critical pair: aababaaababaa=aaaab.

Reduce LHS:

[1](aababaaab)abaa
⇒ aabaa

Flip LHS and RHS.

Defines rule #1.