Some proofs by structural induction on lists


Ivan Stojmenović, Vojislav Stojković




In the paper, the sets $\Omega$ and $\omega$ are defined in the following way: a) $\Omega$ is the set of the lists of the form: \[ [e_1,e_2,\dots,e_n,\dots],\quad noıfty. \] Each element of the list can be: an atom, a finite list, an element of the set $\Omega$ and an element of the set $\omega$. b) $\omega$ is the set of lists which satisfy one of the following conditions: \begin{itemize} ıem[-] descriptionthey are the elements of the set $\Omega$ ıem[-] some of its sublist is the element of the set $\Omega$ ıem[-] they contain an infinite number of sublist. \end{itemize} The functions length and len are defined in the following way: \begin{itemize} ıem[] length [ ]=0 ıem[] length $(a:x)=1$ + length $x$ ıem[] len $[\ ]=0$ ıem[] len $a=0$; atom $a$ ıem[] len $(a:x)=1$ + len $a$ + len $x$. \end{itemize} The main results are: \begin{itemize} ıem[] length $x\to\infty \Leftrightarrow x\in\Omega$ and ıem[] len $x\to\infty\Leftrightarrow x\in\omega$ \end{itemize} The functions lenght(len) is used for the examination: the value of the function, whose arguments are the elements of the set $\Omega(\omega)$, is the element of the set $\Omega(\omega)$.