Certificate for #1603 ⟨a, b | aaaabbbaa=a⟩

Back:⟨a, b | aaaabbbaa=a⟩

Completion settings:

[1] aaaabbbaa=a

Axiom: aaaabbbaa=a.

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

[2] aaabbbaa=aaaabbba

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

aaaabbb aa aaaabbbaa

Critical pair: aaaabbba=aaabbbaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] abbbaa=aabbba

Overlap of [2] aaabbbaa=aaaabbba with [2] aaabbbaa=aaaabbba:

aaabbb aa aaabbbaa

Critical pair: aaabbbaaaabbba=aaaabbbaabbbaa.

Reduce LHS:

[2](aaabbbaa)aabbba
[1]⇒ (aaaabbbaa)abbba
⇒ aabbba

Reduce RHS:

[1](aaaabbbaa)bbbaa
⇒ abbbaa

Flip LHS and RHS.

Defines rule #1.

[4] aaaaabbba=a

Overlap of [1] aaaabbbaa=a with [2] aaabbbaa=aaaabbba:

a aaabbbaa aaabbbaa

Critical pair: aaaaabbba=a.

Defines rule #2.