# Mathematical Foundation of a Functional Implementation of the CNF Algorithm
## 4 Associativity
In principle, the following are possible:  
* there exist \(\varphi,\psi\in\mathrm{P}(\mathbf{L})\), such that \(\alpha\equiv K\varphi\psi\); then \[-1 =\mathrm{ar}(\alpha)\] \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\] \[\Rightarrow\mathrm{ar}(\varphi)=-1=\mathrm{ar}(\psi)\] \[\Rightarrow\varphi,\psi\in\mathrm{K}(X)\]there exist \(\varphi,\psi\in\mathrm{P}(\mathbf{L})\), such that \(\alpha\equiv A\varphi\psi\); then \[-1 =\mathrm{ar}(\alpha)\] \[=\mathrm{max}\{\mathrm{ar}(\varphi),1+\mathrm{ar}(\psi)\}\] \[\mathrm{ar}(\alpha) =\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\} \text{Definition \ref{definition:def}}\]0 \[\mathrm{ar}(\alpha) =\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\} \text{Definition \ref{definition:def}}\]1 so that \(Q(n)\) is true. By the _second principle of finite induction_, for any natural number \(n\), \(Q(n)\) holds and hence the implication. Statement 2 can be proved with the same scheme as above. Suppose now that \(\mathrm{kr}(\alpha)=-1=\mathrm{ar}(\alpha)\). Since \(\mathrm{ar}(\alpha)=-1\), we have that \(\alpha\in\mathrm{K}(X)\) and if there exist \(\varphi,\psi\in\mathrm{P}(\mathbf{L})\), such that \(\alpha\equiv K\varphi\psi\), then one would have \[\mathrm{ar}(\alpha) =\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\} \text{Definition \ref{definition:def}}\]2 hypothesis \[\mathrm{ar}(\alpha) =\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\} \text{Definition \ref{definition:def}}\]3 Definition 4 \[\mathrm{ar}(\alpha) =\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\} \text{Definition \ref{definition:def}}\]4 which is absurd, so \(\alpha\in X\). The reciprocal statement is obviously true and it follows that \(\mathrm{K}(X)\cap\mathrm{A}(X)=X\). The proof of Lemma 5 is straightforward from Lemma 4. For all \(\alpha\in\mathrm{P}(\mathbf{L})\):  
1. If \(\alpha\in\mathrm{K}(X)\setminus X\) then \(0\leq\mathrm{kr}(\alpha)\). 2. If \(\alpha\in\mathrm{A}(X)\setminus X\) then \(0\leq\mathrm{ar}(\alpha)\). 3. \(\mathrm{ar}(\alpha)=-1\) and \(\mathrm{kr}(\alpha)=-1\) if, and only if, \(\alpha\in X\). The respective reciprocal statements of the first two sentences of Lemma 5 are not true. Indeed, \(\mathrm{kr}(AKxyx)=0\) (resp. \(\mathrm{ar}(KAxyx)=0\)), and yet \(AKxyx\
otin\mathrm{K}(X)\setminus X\) (resp. \(KAxyx\
otin\mathrm{A}(X)\setminus X\)). Lemma 6.1 characterises the elements of \(\mathrm{kl}(X)\setminus X\) and \(\mathrm{al}(X)\setminus X\). Its proof can be carried out by induction by making a careful distinction of cases. For all \(\alpha\in\mathrm{P}(\mathbf{L})\),  
1. \(\mathrm{ar}(\alpha)=-1\) and \(\mathrm{kr}(\alpha)=0\) if, and only if, \(\alpha\in\mathrm{kl}(X)\setminus X\). 2. \(\mathrm{ar}(\alpha)=0\) and \(\mathrm{kr}(\alpha)=-1\) if, and only if, \(\alpha\in\mathrm{al}(X)\setminus X\). For all \(\alpha\in\mathrm{K}(\mathrm{A}(X))\), the following statements are equivalent:  
1. \(\mathrm{ar}(\alpha)=0\) and \(\mathrm{kr}(\alpha)=0\). 2. \(\alpha\in\mathrm{lcnf}(X)\setminus(\mathrm{al}(X)\cup\mathrm{kl}(X))\). The formula \(\alpha\equiv AKxyx\) satisfies \(\mathrm{ar}(\alpha)=0=\mathrm{kr}(\alpha)\), but \(\alpha\
ot\in\mathrm{lcnf}(X)\); hence the need for the restriction in the statement of Lemma 7. By means of akr, the above technical lemmas make it possible to characterise in Theorem 4 the set \(\mathrm{lcnf}(X)\) of formulas in left conjunctive normal form. Note how \(\leq\) appears in the statement, again highlighting the subtle role played by \(-1\) in the definition of akr. For all \(\alpha\in\mathrm{K}(\mathrm{A}(X))\), the following statements are equivalent:  
1. \(\mathrm{akr}(\alpha)\leq 0\). 2. \(\alpha\in\mathrm{lcnf}(X)\). Proof. : Let us first show that statement 1 is a sufficient condition for 2. to be fulfilled. The following cases are possible:  
1. \(\operatorname{ar}(\alpha)=-1=\operatorname{kr}(\alpha)\); as stated in Lemma 5, \(\alpha\in X\). 2. \(\operatorname{ar}(\alpha)=-1\) and \(\operatorname{kr}(\alpha)=0\); as stated in Lemma 6, \(\alpha\in\operatorname{kl}(X)\setminus X\). 3.