# Mathematical Foundation of a Functional Implementation of the CNF Algorithm
## 4 Associativity
We distinguish the following cases:  
* \(n=0\); must be \(\alpha\equiv x\in X\) and then \(\mathrm{dak}(\alpha)\equiv\mathrm{dak}(x)\equiv x\equiv\alpha\) and similarly, \(\mathrm{lasc}(\alpha)\equiv\alpha\). It follows that \(Q(0)\) is true. * \(n>0\); let--as the only case of interest-- \(\alpha\equiv K\varphi\psi\), where \(\varphi\in\mathrm{lcnf}(X)\) and \(\psi\in\mathrm{al}(X)\). Then \[-1 =\mathrm{ar}(\alpha)\]7 \[-1 =\mathrm{ar}(\alpha)\]8 \[-1 =\mathrm{ar}(\alpha)\]9 \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]0 Remark 1 and induc. hyp. \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]1 \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]2 \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]3 \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]4 induc. hyp. \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]5 Lemma 10 \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]6 so we know that \(Q(n)\) is true. By the _second principle of finite induction_, for every natural number \(n\) is true \(Q(n)\), hence the validity of assertion 2. If we now assume that 2 is true, that \(\mathrm{alt}(\alpha)=0\) and that \(\alpha\in\mathrm{K}(\mathrm{A}(X))\) is ensured by the Corollary 1. In particular, as a consequence of Theorem 3, we have  
\[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]7 \[=\max\{\mathrm{ar}(\varphi),\mathrm{ar}(\psi)\}\]8  
and therefore, \(\mathrm{ar}(\alpha)\leq 0\) and \(\mathrm{kr}(\alpha)\leq 0\); thus, we have proved 3. Let us finally assume 3 to be true and show that \(\alpha\in\mathrm{lcnf}(X)\). Since \(\mathrm{alt}(\alpha)=0\) and again using Corollary 1, we know that \(\alpha\in\mathrm{K}(\mathrm{A}(X))\). According to Theorem 2, since \(\mathrm{akr}(\alpha)\leq 0\), \(\alpha\in\mathrm{lcnf}(X)\) must necessarily hold and this is what statement 1 establishes. Definition 6: For all \(\alpha\in\mathrm{K}(\mathrm{A}(X))\), \(\mathrm{hre}(\alpha)\) is the natural number defined by the equality:  
\[\mathrm{hre}(\alpha)= \begin{cases}0,&\text{if }\mathrm{akr}(\alpha)\leq 0,\\ \lfloor log_{2}(\mathrm{akr}(\alpha))\rfloor+1,&\text{otherwise.}\end{cases} \]  
Remark 8: _Understanding the evaluation of the expressions from a \"lazy\" point of view, the following equality should be accepted:_  
\[\mathrm{hre}(\alpha)=(1-\chi_{\{-1,0\}}(\mathrm{akr}(\alpha)))(\lfloor log_{2} (\mathrm{akr}(\alpha))\rfloor+1)\]  
_where, of course, \(\chi_{\{-1,0\}}\) is the characteristic function on the set \(\{-1,0\}\). Let it also be noted that in the case where for the formula \(\alpha\) one has \(0<\mathrm{akr}(\alpha)\), then \(\mathrm{hre}(\alpha)\) is the number of digits in the (single) binary expression of \(\mathrm{akr}(\alpha)\) when it is greater than \(0\), and \(0\) otherwise._  
Finally, the next corollary, Corollary 3, informs us that for any formula \(\alpha\) in \(\mathrm{K}(\mathrm{A}(X))\), \(\mathrm{lasc}^{\mathrm{hre}(\alpha)}(\alpha)\) is a formula in left conjunctive normal form (equivalent to \(\alpha\), of course) and that per iteration of lasc, the number \(\mathrm{hre}(\alpha)\) of iterations is the smallest number of those that achieve it. It is based on how many times the function \(\left\lfloor\frac{x}{2}\right\rfloor\) must be iterated to obtain zero, in order to express \(x\) in binary form. This gives us an estimate of the complexity of our algorithm: it is logarithmic, which is fantastic news. The corresponding result, with its complete proof, is given just below. The demonstration of the corollary is simple if we rely on this observation, and it can be carried out by inductive reasoning based on a careful distinction of cases. Corollary 3: _For all \(\alpha\in\operatorname{K}(\operatorname{A}(X))\), \(\operatorname{hre}(\alpha)\) is the smallest of the natural numbers \(m\) satisfying \(\operatorname{lasc}^{m}(\alpha)\in\operatorname{lcnf}(X)\)._