(related to Lemma: LOOP-Computable Functions are Total)
Let \(f : \mathbb N^k \to \mathbb N\) be a \(L O O P\)-computable function. We have to show that \(f\) is total, i.e. that \(f(n_1,\ldots,n_k)\) is defined for every input \((n_1,\ldots,n_k)\in\mathbb N^k\).
By definition of \(L O O P\)-computability, there exists a finite \(L O O P\) program \(P\), which computes \(f\). Any LOOP command \(\mathtt{LOOP~r_i~DO~P_1~END}\) is repeated for a finite number of times, i.e. the natural number contained in the register \(r_i\). Therefore, \(P\) must terminate for any input \((n_1,\ldots,n_k)\in\mathbb N^k\). Therefore, \(f\) is total.
