\section{The Theory {\tt ell}}

The theory \ml{ell}\index{ell, theory@{\ptt ell}, theory} is concerned with
selecting elements from a list, indexing from the end. 
The function \ml{ELL}\index{ELL@{\ptt ELL}} is defined here. It
chooses an element from a list indexing from 0 starting at the end of the list.


\begin{hol}
\[
  \ml{ELL}\; k \ml{[}a_n\listsep a_0\ml{]} = a_k
\]\end{hol}

\noindent It is defined as follows:

\begin{hol}
\index{ELL@{\ptt ELL}}
\begin{verbatim}
  ELL          |- (!l. ELL 0 l = LAST l) /\
                  (!n l. ELL(SUC n)l = ELL n(BUTLAST l))
\end{verbatim}\end{hol}

\noindent Following are some of the theorems pre-proved in this theory.

\begin{hol}
\index{ELL\_CONS@{\ptt ELL\_CONS}}
\index{ELL\_LAST@{\ptt ELL\_LAST}}
\index{EL\_ELL@{\ptt EL\_ELL}}
\index{ELL\_APPEND\_1@{\ptt ELL\_APPEND\_1}}
\begin{verbatim}
  ELL_CONS     |- !l x k. k < (LENGTH l) ==> (ELL k(CONS x l) = ELL k l)

  ELL_LAST     |- !l. ~NULL l ==> (ELL 0 l = LAST l)

  EL_ELL
        |- !l k. k < (LENGTH l) ==> (EL k l = ELL(PRE((LENGTH l) - k))l)

  ELL_APPEND_1
       |- !l1 l2 k. k < (LENGTH l2) ==> (ELL k(APPEND l1 l2) = ELL k l2)
\end{verbatim}\end{hol}
