Certificate for #3927 ⟨a, b | aaaabbaaa=aa⟩

Back:⟨a, b | aaaabbaaa=aa⟩

Completion settings:

[1] aaaabbaaa=aa

Axiom: aaaabbaaa=aa.

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

[2] aaabbaaa=aaaabbaa

Overlap of [1] aaaabbaaa=aa with [1] aaaabbaaa=aa:

aaaabb aaa aaaabbaaa

Critical pair: aaaabbaa=aaabbaaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] aabbaaa=aaabbaa

Overlap of [1] aaaabbaaa=aa with [2] aaabbaaa=aaaabbaa:

aaaabb aaa aaabbaaa

Critical pair: aaaabbaaaabbaa=aabbaaa.

Reduce LHS:

[1](aaaabbaaa)abbaa
⇒ aaabbaa

Flip LHS and RHS.

Defines rule #1.

[4] aaaaabbaa=aa

Overlap of [1] aaaabbaaa=aa with [2] aaabbaaa=aaaabbaa:

aaaabbaa a aaabbaaa

Critical pair: aaaabbaaaaaabbaa=aaaabbaaa.

Reduce LHS:

[1](aaaabbaaa)aaabbaa
⇒ aaaaabbaa

Reduce RHS:

[1](aaaabbaaa)
⇒ aa

Defines rule #2.