Certificate for #3864 ⟨a, b | aaaaabaaa=aa⟩

Back:⟨a, b | aaaaabaaa=aa⟩

Completion settings:

[1] aaaaabaaa=aa

Axiom: aaaaabaaa=aa.

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

[2] aaaabaaa=aaaaabaa

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

aaaaab aaa aaaaabaaa

Critical pair: aaaaabaa=aaaabaaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] aaaaaabaa=aa

Overlap of [1] aaaaabaaa=aa with [2] aaaabaaa=aaaaabaa:

aaaaabaa a aaaabaaa

Critical pair: aaaaabaaaaaaabaa=aaaaabaaa.

Reduce LHS:

[1](aaaaabaaa)aaaabaa
⇒ aaaaaabaa

Reduce RHS:

[1](aaaaabaaa)
⇒ aa

Defines rule #2.

[4] aabaaa=aaabaa

Overlap of [2] aaaabaaa=aaaaabaa with [2] aaaabaaa=aaaaabaa:

aaaab aaa aaaabaaa

Critical pair: aaaabaaaaabaa=aaaaabaaabaaa.

Reduce LHS:

[2](aaaabaaa)aabaa
[1]⇒ (aaaaabaaa)abaa
⇒ aaabaa

Reduce RHS:

[1](aaaaabaaa)baaa
⇒ aabaaa

Flip LHS and RHS.

Defines rule #1.