Certificate for #169 ⟨a, b | aaabaa=a⟩

Back:⟨a, b | aaabaa=a⟩

Completion settings:

[1] aaabaa=a

Axiom: aaabaa=a.

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

[2] aabaa=aaaba

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

aaab aa aaabaa

Critical pair: aaaba=aabaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] abaa=aaba

Overlap of [1] aaabaa=a with [2] aabaa=aaaba:

aaab aa aabaa

Critical pair: aaabaaaba=abaa.

Reduce LHS:

[1](aaabaa)aba
⇒ aaba

Flip LHS and RHS.

Defines rule #1.

[4] aaaaba=a

Overlap of [1] aaabaa=a with [2] aabaa=aaaba:

a aabaa aabaa

Critical pair: aaaaba=a.

Defines rule #2.