Down below is a Term rewriting system where I am trying to find the critical pairs, decide if it is confluent and find the Normal terms. I think it's difficult to understand all these concepts and I am just mixing everything up, I think.ProblemConsider the $TRS$\begin{equation}\begin{split}(R_1)\quad x\cdot (y + z)&\rightarrow x\cdot y+x\cdot z\\(R_2)\quad(y + z)\cdot x &\rightarrow y\cdot x+z\cdot x\\(R_3)\quad\text{ }\text{ }\text{ }(x\cdot y)\cdot z&\rightarrow x\cdot (y\cdot z)\\(R_4)\quad(x+y)+z&\rightarrow x + (y+z)?\end{split}\end{equation}What are the critical pairs? Is it Confluent? What are the normal terms?SolutionLet us start with the critical pairs:Critical Pair:To find the critical pairs we will, as a start, compute$$(\alpha+\beta)\cdot (y+z)\to_{R_1} (\alpha+\beta)\cdot y + (\alpha + \beta)\cdot z$$$$(\alpha+\beta)\cdot (y+z)\to_{R_2} \alpha\cdot (y+z)+\beta\cdot (y+z)$$Now, we found a critical pair $C_1=((\alpha+\beta)\cdot y + (\alpha + \beta)\cdot z,\alpha\cdot (y+z)+\beta\cdot (y+z))$. So, to find a critical pair We take an expression and apply two different rules and see where we end up? If that's the case I would continue as this:$$((\alpha+\beta)\cdot y)\cdot z\to_{R_2} (\alpha\cdot y+\beta\cdot y)\cdot z$$$$((\alpha+\beta)\cdot y)\cdot z\to_{R_3} (\alpha+\beta)\cdot (y\cdot z)$$So the next critical pair would be $C_2=((\alpha\cdot y+\beta\cdot y)\cdot z,(\alpha+\beta)\cdot (y\cdot z))$. Or should I reduce them as much as possible and that will be my critical pairs? Perhaps I should do both? How do I know if I have found all my critical pairs? I don't even know what I am allowed to do.   $\text{ }$ :(I mean, can I do something like this?$((\alpha_1+\alpha_2)+\alpha_3)\cdot (x+y)$. And this would give me other critical pairs?Confluent:Since by starting with $R_1$ and then apply $R_2$ doesn't yield the same term as when we start with $R_2$ and then apply $R_1$ (when we found the first critical pair), thus, the TRS cannot be confluent. Is this a correct interpretation? It shouldn't matter in which order I apply the rules, it should still end up with the same result.Normal Form:$$(\alpha+\beta)\cdot (y+z)\to_{R_1} (\alpha+\beta)\cdot y + (\alpha + \beta)\cdot z\to_{R_2} (\alpha\cdot y+\beta\cdot y)+(\alpha\cdot z+\beta\cdot z)\to_{R_4} \alpha\cdot y+(\beta\cdot y+(\alpha\cdot z+\beta\cdot z))$$So perhaps $N_F=\alpha\cdot y+(\beta\cdot y+(\alpha\cdot z+\beta\cdot z))$ is a normal form (term?) of $(\alpha+\beta)\cdot (y+z)$, since $N_F$ can't be reduced any further.I really hope someone can help me with this problem. I have been thinking about this for a week now and I cannot get my head around it.Thanks :)The book I am using:Term Rewriting and All That by Franz Baader and Tobias Nipkow
Computing critical pairs, confluence and Normal terms
logic;first order logic;term rewriting