Uniqueness of the result of rewritting an algebraic expression using distributivity rule Let $expr$ be an algebraic expression involving natural numbers, addition operator and multiplication operator, e.g.,
$$(1+2)\cdot(3+4 \cdot 5)+6.$$
By iteratively applying the distributivity of multiplication over addition to $expr$, that is, transforming subexpressions of the form $(expr_1 + expr_2)\cdot expr_3$ into the form 
$(expr_1\cdot expr_3) + (expr_2 \cdot expr_3)$, until it is no longer possible, at each iteration applying the distribituvity rule to the first (the "leftmost" one) subexpression that it can be applied to, one obtains a sum of products. No other rules are applied, no addition and no multiplication is actually performed. For the above example, the result would be
$$1\cdot 3 + 1\cdot 4 \cdot 5 + 2 \cdot 3 + 2\cdot 4 \cdot 5 + 6.$$
Is the obtained sum of products unique?
If yes (as I believe is the case), is there a general result that this fact follows from?
$\textbf{Edit:}$


*

*the distributivity rule $expr_1 \cdot (expr_2+ expr_3) \rightarrow (expr_1 \cdot expr_2 )+ (expr_1 \cdot expr_3)$ can also be applied


$\textbf{Solution:}$
By formalizing properly the reduction rules that I had in mind, I got a reduction system that is both locally confluent and terminating. Now the uniqueness of the normal form follows from the Newman's lemma.
 A: Let $N$ be a language for natural numbers. The set $E$ of algebraic expressions is inductively defined by the following rules:


*

*If $n \in N$, then $n \in E$.

*If $e, e' \in E$, then $(e + e') \in E$.

*If $e, e' \in E$, then $(e \cdot e') \in E$.


In order to define a function $f \colon E \to E$ transforming an expression $e$ into another expression $f(e)$, one just needs to use structural recursion. In your case, the function $f$ is defined by the following rules:


*
 
* If $n \in N$, then $f(n) = n$.
 
* If $e, e' \in E$, then $f((e + e')) = (f(e) + f(e'))$.
 
* If $e \in E$, then:
      
* 
      
* If $n \in E$, then $f((n \cdot e)) = (f(n) \cdot f(e))$.
      
* If $e', e'' \in E$, then $f(((e' + e'') \cdot e)) = ((f(e') \cdot f(e)) + (f(e'') \cdot f(e)))$.
      
* If $e', e'' \in E$, then $f(((e' \cdot e'') \cdot e)) = ((f(e') \cdot f(e'')) \cdot f(e))$.
      


With these rules the function $f$ is well-defined, so for a given expression $e$ the rewritten expression $f(e)$ is clearly unique.
Now, if you only allow expressions of the form $((e' + e'') \cdot e)$ to be transformed into $((e' \cdot e) + (e'' \cdot e))$, then an expression such as $(2 \cdot (3 + 4))$ won't be transformed into a sum of products. In order to apply left-distributivity as well, you need to adjust the definition of $f$. (Hint: in rule 3, instead of three cases there will be nine cases to handle). 
