Certificate for #365 ⟨a, b | aaabbaa=a⟩

Back:⟨a, b | aaabbaa=a⟩

Completion settings:

[1] aaabbaa=a

Axiom: aaabbaa=a.

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

[2] aabbaa=aaabba

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

aaabb aa aaabbaa

Critical pair: aaabba=aabbaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] abbaa=aabba

Overlap of [1] aaabbaa=a with [2] aabbaa=aaabba:

aaabb aa aabbaa

Critical pair: aaabbaaabba=abbaa.

Reduce LHS:

[1](aaabbaa)abba
⇒ aabba

Flip LHS and RHS.

Defines rule #1.

[4] aaaabba=a

Overlap of [1] aaabbaa=a with [2] aabbaa=aaabba:

a aabbaa aabbaa

Critical pair: aaaabba=a.

Defines rule #2.