# Mathematical Foundation of a Functional Implementation of the CNF Algorithm
## 4 Associativity  
By iterating \(\mathrm{dak}\) from any formula, we obtain, as we have seen, a formula equivalent to it that is in conjunctive normal form. However, for certain formulas in conjunctive normal form, there are several others also in conjunctive normal form that are equivalent to it, but such that they are all distinct from each other. In this section, we intend to provide an algorithm to select among all those formulas, one of which we will consider in canonical form. For practical reasons, we will consider the set \(\mathrm{lcnf}(X)\), the set of formulas in conjunctive left normal form, as the one that gathers exactly all the formulas in canonical form. **Definition 4**. : _Let \(\mathrm{ar}\colon\mathrm{P}(\mathbf{L})\longrightarrow\mathbb{Z}\) be defined as follows:_  
\[\mathrm{ar}(\alpha)= \begin{cases}-1,&\text{if $\alpha\in X$;}\\ \max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\},&\text{if $\alpha=\mathrm{K} \,\varphi\psi$;}\\ \max\{\mathrm{ar}(\varphi),1+\mathrm{ar}(\psi)\},&\text{if $\alpha=\mathrm{A} \,\varphi\psi$.}\end{cases} \]_and let \(\mathrm{kr}\colon\,\mathrm{P}(\mathbf{L})\longrightarrow\mathbb{Z}\) be defined as follows:_  
\[\mathrm{kr}(\alpha)= \begin{cases}-1,&\text{if $\alpha\in X$;}\\ \max\{\mathrm{kr}(\varphi),1+\mathrm{kr}(\varphi)\},&\text{if $\alpha=\mathrm{K} \varphi\psi$;}\\ \max\{\mathrm{kr}(\varphi),\mathrm{kr}(\psi)\},&\text{if $\alpha=\mathrm{A} \varphi\psi$.}\end{cases} \]  
_Also let \(\mathrm{akr}\colon\,\mathrm{P}(\mathbf{L})\longrightarrow\mathbb{Z}\) be defined as follows:_  
\[\mathrm{akr}(\alpha)=\max\{\mathrm{ar}(\alpha),\mathrm{kr}(\alpha)\}\]  
**Remark 4**. : _The maps \(\mathrm{ar}\) and \(\mathrm{kr}\) have the properties given in Lemma 4. This Lemma characterises the elements of \(\mathrm{K}(X)\), \(\mathrm{A}(X)\), and \(X\). The particular assignation in both functions of the value \(-1\) to the elements of \(X\) is just in order to adjust the final computations accordingly._  
**Lemma 4**. : _For all \(\alpha\in\mathrm{P}(\mathbf{L})\):_  
1. \(\alpha\in\mathrm{K}(X)\) _if, and only if,_ \(\mathrm{ar}(\alpha)=-1\)_._
2. \(\alpha\in\mathrm{A}(X)\) _if, and only if,_ \(\mathrm{kr}(\alpha)=-1\)_._
3. \(\alpha\in X\) _if, and only if,_ \(\mathrm{kr}(\alpha)=-1=\mathrm{ar}(\alpha)\)_._
4. \(\mathrm{K}(X)\cap\mathrm{A}(X)=X\)_._  
Proof. : Let us prove statement 1. First we will reason by induction according to the complexity of \(\alpha\) and according to the predicate \(Q(n)\) of the literal content:  
\"for all \(\alpha\in\mathrm{P}(\mathbf{L})\), if \(\alpha\in\mathrm{K}(X)\) and \(\mathrm{comp}(\alpha)=n\), then \(\mathrm{ar}(\alpha)=-1\)\"  
Suppose, as an induction hypothesis, that \(n\) is a natural number and that for any natural number \(k\) such that \(k<n\), \(Q(k)\) holds. We have the following cases:  
* \(n=0\); then let --as the only case of interest-- \(\alpha\equiv x\in X\). By Definition 4, \(\mathrm{ar}(\alpha)=-1\), so \(Q(0)\) is true. * \(n>0\); if \(\alpha\in\mathrm{K}(X)\) and \(n>0\), there must exist \(\varphi,\psi\in\mathrm{K}(X)\) such that \(\alpha\equiv K\varphi\psi\). Then \[\mathrm{ar}(\alpha) =\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\} \text{Definition \ref{definition:def}}\] \[=\max\{-1,-1\} \text{induc. hyp.}\] \[=-1\] so \(Q(n)\) is true in this case. By the _second principle of finite induction_, for any natural number \(n\) is true \(Q(n)\) and hence the implication. Reciprocally, let us now consider the predicate \(Q(n)\): \"for all \(\alpha\in\mathrm{P}(\mathbf{L})\), if \(\mathrm{comp}(\alpha)=n\) and \(\mathrm{ar}(\alpha)=-1\), then \(\alpha\in\mathrm{K}(X)\)\"  
Suppose, as an induction hypothesis, that \(n\) is a natural number and that for any natural number \(k\), such that \(k<n\), \(Q(k)\) holds. We have the following cases:  
* \(n=0\); then let --as the only case of interest-- \(\alpha\equiv x\in X\). Since \(X\subseteq\mathrm{K}(X)\) it follows that \(Q(0)\) is true. * \(n>0\); let \(\alpha\in\mathrm{P}(\mathbf{L})\) such that \(\mathrm{comp}(\alpha)=n\) and \(\mathrm{ar}(\alpha)=-1\).