Certificate for #755 ⟨a, b | aaaabbaa=a⟩

Back:⟨a, b | aaaabbaa=a⟩

Completion settings:

[1] aaaabbaa=a

Axiom: aaaabbaa=a.

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

[2] aaabbaa=aaaabba

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

aaaabb aa aaaabbaa

Critical pair: aaaabba=aaabbaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] abbaa=aabba

Overlap of [2] aaabbaa=aaaabba with [2] aaabbaa=aaaabba:

aaabb aa aaabbaa

Critical pair: aaabbaaaabba=aaaabbaabbaa.

Reduce LHS:

[2](aaabbaa)aabba
[1]⇒ (aaaabbaa)abba
⇒ aabba

Reduce RHS:

[1](aaaabbaa)bbaa
⇒ abbaa

Flip LHS and RHS.

Defines rule #1.

[4] aaaaabba=a

Overlap of [1] aaaabbaa=a with [2] aaabbaa=aaaabba:

a aaabbaa aaabbaa

Critical pair: aaaaabba=a.

Defines rule #2.