Certificate for #383 ⟨a, b | aabbaab=a⟩

Back:⟨a, b | aabbaab=a⟩

Completion settings:

[1] aabbaab=a

Axiom: aabbaab=a.

Referenced by [2], [3], [4].

[2] aabba=abaab

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

aabb aab aabbaab

Critical pair: aabba=abaab.

Defines rule #1.

Referenced by [3], [4].

[3] abaabab=a

Overlap of [1] aabbaab=a with [2] aabba=abaab:

aabbaab aabba

Critical pair: abaabab=a.

Defines rule #3.

Referenced by [4].

[4] aaabab=abaaba

Overlap of [1] aabbaab=a with [3] abaabab=a:

aabba ab abaabab

Critical pair: aabbaa=aaabab.

Reduce LHS:

[2](aabba)a
⇒ abaaba

Flip LHS and RHS.

Defines rule #2.