Certificate for #4190 ⟨a, b | aabbbaaab=aa⟩

Back:⟨a, b | aabbbaaab=aa⟩

Completion settings:

[1] aabbbaaab=aa

Axiom: aabbbaaab=aa.

Defines rule #4.

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

[2] aabbaaab=aabbbaaa

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

aabbba aab aabbbaaab

Critical pair: aabbbaaa=aabbaaab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aabaaab=aabbaaa

Overlap of [1] aabbbaaab=aa with [2] aabbaaab=aabbbaaa:

aabbba aab aabbaaab

Critical pair: aabbbaaabbbaaa=aabaaab.

Reduce LHS:

[1](aabbbaaab)bbaaa
⇒ aabbaaa

Flip LHS and RHS.

Defines rule #2.

[4] aaaaab=aabaaa

Overlap of [2] aabbaaab=aabbbaaa with [2] aabbaaab=aabbbaaa:

aabba aab aabbaaab

Critical pair: aabbaaabbbaaa=aabbbaaabaaab.

Reduce LHS:

[2](aabbaaab)bbaaa
[1]⇒ (aabbbaaab)baaa
⇒ aabaaa

Reduce RHS:

[1](aabbbaaab)aaab
⇒ aaaaab

Flip LHS and RHS.

Defines rule #1.