Certificate for #1637 ⟨a, b | aaabbaaab=a⟩

Back:⟨a, b | aaabbaaab=a⟩

Completion settings:

[1] aaabbaaab=a

Axiom: aaabbaaab=a.

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

[2] aaabba=abaaab

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

aaabb aaab aaabbaaab

Critical pair: aaabba=abaaab.

Defines rule #1.

Referenced by [3], [4].

[3] abaaabaab=a

Overlap of [1] aaabbaaab=a with [2] aaabba=abaaab:

aaabbaaab aaabba

Critical pair: abaaabaab=a.

Defines rule #3.

Referenced by [4].

[4] aaaabaab=abaaabaa

Overlap of [1] aaabbaaab=a with [3] abaaabaab=a:

aaabbaa ab abaaabaab

Critical pair: aaabbaaa=aaaabaab.

Reduce LHS:

[2](aaabba)aa
⇒ abaaabaa

Flip LHS and RHS.

Defines rule #2.