So, I know Church-Rosser has 2 thesis:
CR1: If $ E_1 \leftrightarrow E_2 $, then there exists an Expression E so $ E_1 \rightarrow E $ and $ E_2 \rightarrow E $
CR2: If $ E \rightarrow N $ (with N in normalform), then there exists a reduction row in normalorder (first reduce the left most ouuter most index) from E to N
from CR1 we learn that no expression can be converted to 2 different normalforms, so there is only one result for each function
from CR2 we learn that reduction in normalorder always finds the result (if their is one (no loop))
But i don't understand why these two are so important for basing a programming language on lambda-calculus. So my question is why are they?