\section{The Theory {\tt member}}

The theory \ml{member}\index{member, theory@{\ptt member}, theory} contains definitions of
predicates which test for membership of elements and sublists within a list.
The predicate \ml{MEMBER}\index{MEMBER@{\ptt MEMBER}} tests for a given element
being a member of a list.
\ml{LLESS\_LEFT}\index{LLESS\_LEFT@{\ptt LLESS\_LEFT}} tests if a list is an
 initial sublist not
equal to a given list.  \ml{LLEQ\_LEFT}\index{LLEQ\_LEFT@{\ptt LLEQ\_LEFT}} tests
  if a list is an initial proper sublist of a given list.
\ml{LLESS\_RIGHT}\index{LLESS\_RIGHT@{\ptt LLESS\_RIGHT}} tests if a list is a
 final sublist not
equal to a given list.
 \ml{LLEQ\_RIGHT}\index{LLEQ\_RIGHT@{\ptt LLEQ\_RIGHT}} tests
  if a list is a final proper sublist of a given list.

\[ \begin{array}[t]{@{}l@{}l@{}l}
  \ml{MEMBER}\; a_i\; \ml{[}a_1\listsep a_n\ml{]} &  =  T &  (i < n) \\
  \ml{MEMBER}\; b\; \ml{[}a_1\listsep a_n\ml{]} & =  F   &  (otherwise)
 \end{array}
\]

\[ \begin{array}[t]{@{}l@{}l@{}l}
  \ml{LLESS\_LEFT}\ml{[}a_1\listsep a_n\ml{]}\;
           \ml{[}a_1\listsep a_n \lsep b_1\listsep b_m \ml{]} &  =  T \\
  \ml{LLESS\_LEFT}\ml{[}a_1\listsep a_n\ml{]}\;\ml{[}b_1\listsep b_m\ml{]} & = F & (otherwise)
 \end{array}
\]

\[ \begin{array}[t]{@{}l@{}l@{}l}
  \ml{LLEQ\_LEFT}\ml{[}a_1\listsep a_n\ml{]}\;
           \ml{[}a_1\listsep a_n \lsep b_1\listsep b_m \ml{]} & = T \\
  \ml{LLEQ\_LEFT}\ml{[}a_1\listsep a_n\ml{]}\;\ml{[}a_1\listsep a_n\ml{]} & = T \\
  \ml{LLEQ\_LEFT}\ml{[}a_1\listsep a_n\ml{]}\;\ml{[}b_1\listsep b_m\ml{]} & = F &
    (otherwise)
 \end{array}
\]


\[ \begin{array}[t]{@{}l@{}l@{}l}
  \ml{LLESS\_RIGHT}\ml{[}a_1\listsep a_n\ml{]}\;
           \ml{[}b_1\listsep b_m \lsep a_1\listsep a_n \ml{]} &  =  T \\
  \ml{LLESS\_RIGHT}\ml{[}a_1\listsep a_n\ml{]}\;\ml{[}b_1\listsep b_m\ml{]} & = F & (otherwise)
 \end{array}
\]

\[ \begin{array}[t]{@{}l@{}l@{}l}
  \ml{LLEQ\_RIGHT}\ml{[}a_1\listsep a_n\ml{]}\;
           \ml{[}b_1\listsep b_m \lsep a_1\listsep a_n \ml{]} & = T \\
  \ml{LLEQ\_RIGHT}\ml{[}a_1\listsep a_n\ml{]}\;\ml{[}a_1\listsep a_n\ml{]} & = T \\
  \ml{LLEQ\_RIGHT}\ml{[}a_1\listsep a_n\ml{]}\;\ml{[}b_1\listsep b_m\ml{]} & = F &
    (otherwise)
 \end{array}
\]

\noindent They have the following definitions

\begin{hol}
\index{MEMBER@{\ptt MEMBER}}
\index{LLESS\_LEFT@{\ptt LLESS\_LEFT}}
\index{LLEQ\_LEFT@{\ptt LLEQ\_LEFT}}
\index{LLESS\_RIGHT@{\ptt LLESS\_RIGHT}}
\index{LLEQ\_RIGHT@{\ptt LLEQ\_RIGHT}}
\begin{verbatim}
  MEMBER     |- (!x. MEMBER x[] = F) /\
                (!x h t. MEMBER x(CONS h t) = (h = x) \/ MEMBER x t)

  LLESS_LEFT |- (!l. [] LLESS_LEFT l = ~NULL l) /\
                (!a rest l. (CONS a rest) LLESS_LEFT l =
                              ~NULL l /\ (a = HD l) /\ rest LLESS_LEFT (TL l))

  LLEQ_LEFT  |- !l1 l2. l1 LLEQ_LEFT l2 = l1 LLESS_LEFT l2 \/ (l1 = l2)

  LLESS_RIGHT |- (!l. []  LLESS_RIGHT l = ~NULL l) /\
                 (!a rest l. (SNOC a rest) LLESS_RIGHT l =
                              ~(NULL l) /\ (a = LAST l) /\
                              rest LLESS_RIGHT (BUTLAST l))

  LLEQ_RIGHT  |- !l1 l2. l1 LLEQ_RIGHT l2 = l1 LLESS_RIGHT l2 \/ (l1 = l2)
\end{verbatim}\end{hol}

\noindent The theorems pre-proved in this theory include:
\begin{hol}
\index{MEMBER\_SNOC@{\ptt MEMBER\_SNOC}}
\index{NOT\_LLESS\_LEFT\_NIL@{\ptt NOT\_LLESS\_LEFT\_NIL}}
\index{CONS\_LLESS\_LEFT\_TL@{\ptt CONS\_LLESS\_LEFT\_TL}}
\index{CONS\_LLEQ\_LEFT\_TL@{\ptt CONS\_LLEQ\_LEFT\_TL}}
\index{NIL\_LLEQ\_RIGHT@{\ptt NIL\_LLEQ\_RIGHT}}
\index{SNOC\_LLESS\_RIGHT\_BUTLAST@{\ptt SNOC\_LLESS\_RIGHT\_BUTLAST}}
\begin{verbatim}
  MEMBER_SNOC              |- !t x h. MEMBER x(SNOC h t) =
                                                (h = x) \/ MEMBER x t

  NOT_LLESS_LEFT_NIL       |- !l. ~l LLESS_LEFT []

  CONS_LLESS_LEFT_TL       |- !l1 l2. (CONS h l1) LLESS_LEFT l2 ==>
                                                l1 LLESS_LEFT (TL l2)

  CONS_LLEQ_LEFT_TL        |- !l1 l2. (CONS h l1) LLEQ_LEFT l2 ==>
                                                l1 LLEQ_LEFT (TL l2)

  SNOC_LLESS_RIGHT_BUTLAST |-  !l1 l2. (SNOC h l1) LLESS_RIGHT l2 ==>
                                                l1 LLESS_RIGHT (BUTLAST l2)

  NIL_LLEQ_RIGHT           |- !l. [] LLEQ_RIGHT l
\end{verbatim}\end{hol}
