\chapter{Pre-proved Theorems}\label{thms}
\input{theorems-intro}
\section{General List Theorems}
\THEOREM CONS\_ONE\_ONE general\_lists
|- !h t h' t'. (CONS h t = CONS h' t') ==> (h = h') /\ (t = t')
\ENDTHEOREM
\THEOREM LENGTH1\_CONS\_HD general\_lists
|- !l. (LENGTH l = 1) = ([HD l] = l)
\ENDTHEOREM

\THEOREM LENGTH\_EQ general\_lists
|- !x y. (x = y) ==> (LENGTH x = LENGTH y)
\ENDTHEOREM
\THEOREM LENGTH\_EQ\_SUC\_IMP\_NOT\_NIL general\_lists
|- !l k. (LENGTH l = SUC k) ==> ~(l = [])
\ENDTHEOREM
\THEOREM LENGTH\_EQ\_SUC\_IMP\_NOT\_NULL general\_lists
|- !l k. (LENGTH l = SUC k) ==> ~NULL l
\ENDTHEOREM
\THEOREM LENGTH\_GR\_0\_NOT\_NIL general\_lists
|- !l. 0 < (LENGTH l) ==> ~(l = [])
\ENDTHEOREM
\THEOREM LENGTH\_LESS\_EQ general\_lists
|- !l1 l2.
    (LENGTH l1) <= (LENGTH l2) ==>
    (!a. (LENGTH l1) < (LENGTH(CONS a l2)))
\ENDTHEOREM
\THEOREM LENGTH\_LESS\_EQ\_EQ general\_lists
|- !l1 l2 a.
    (LENGTH l1) <= (LENGTH l2) = (LENGTH l1) < (LENGTH(CONS a l2))
\ENDTHEOREM
\THEOREM LENGTH\_LESS\_IMP\_NOT\_EQ general\_lists
|- !l1 l2. (LENGTH l1) < (LENGTH l2) ==> ~(l1 = l2)
\ENDTHEOREM
\THEOREM LENGTH\_NOT\_NULL general\_lists
|- !l. 0 < (LENGTH l) = ~NULL l
\ENDTHEOREM
\THEOREM LENGTH\_NULL general\_lists
|- !l. (LENGTH l = 0) = NULL l
\ENDTHEOREM
\THEOREM LENGTH\_TL\_SUB general\_lists
|- !l. ~NULL l ==> (LENGTH(TL l) = (LENGTH l) - 1)
\ENDTHEOREM
\THEOREM list\_NULL\_CASES general\_lists
|- !l. NULL l \/ (?t h. l = CONS h t)
\ENDTHEOREM
\THEOREM L\_EQ\_NIL general\_lists
|- !l. (l = []) = NULL l
\ENDTHEOREM
\THEOREM NIL\_EQ\_L general\_lists
|- !l. ([] = l) = NULL l
\ENDTHEOREM
\THEOREM NOT\_LENGTH\_EQ general\_lists
|- !l2 l1. ~(LENGTH l1 = LENGTH l2) ==> ~(l1 = l2)
\ENDTHEOREM
\THEOREM NULL\_EQ\_EMPTY general\_lists
|- !l. NULL l = (l = [])
\ENDTHEOREM
\THEOREM TL\_NIL general\_lists
|- !l. (LENGTH l = 1) ==> (TL l = [])
\ENDTHEOREM
\THEOREM TL\_NULL general\_lists
|- !l. (LENGTH l = 1) ==> NULL(TL l)
\ENDTHEOREM
\section{Theorems about the Tail End of a List}
\THEOREM BUTLAST snoc
|- !h t. BUTLAST(SNOC h t) = t
\ENDTHEOREM
\THEOREM BUTLAST\_CONS snoc
|- !h t. BUTLAST(CONS h t) = (NULL t => [] | CONS h(BUTLAST t))
\ENDTHEOREM
\THEOREM BUTLAST\_CONS\_NOT\_NULL snoc
|- !h l. ~NULL l ==> (BUTLAST(CONS h l) = CONS h(BUTLAST l))
\ENDTHEOREM
\THEOREM BUTLAST\_DEF snoc
|- !l. BUTLAST l = (@t. SNOC(LAST l)t = l)
\ENDTHEOREM
\THEOREM BUTLAST\_EL snoc
|- !a. BUTLAST[a] = []
\ENDTHEOREM
\THEOREM BUTLAST\_NIL snoc
|- !l. (LENGTH l = 1) ==> (BUTLAST l = [])
\ENDTHEOREM
\THEOREM BUTLAST\_NULL snoc
|- !l. (LENGTH l = 1) ==> NULL(BUTLAST l)
\ENDTHEOREM
\THEOREM BUTLAST\_REVERSE\_EQ\_REVERSE\_TL snoc
|- !l. ~NULL l ==> (BUTLAST(REVERSE l) = REVERSE(TL l))
\ENDTHEOREM
\THEOREM BUTLAST\_TL snoc
|- !l. 1 < (LENGTH l) ==> (BUTLAST(TL l) = TL(BUTLAST l))
\ENDTHEOREM
\THEOREM HD\_BUTLAST snoc
|- !l. 1 < (LENGTH l) ==> (HD(BUTLAST l) = HD l)
\ENDTHEOREM
\THEOREM HD\_SNOC snoc
|- !h t. HD(SNOC h t) = (NULL t => h | HD t)
\ENDTHEOREM
\THEOREM ISO\_REVERSE snoc
|- ISO REVERSE
\ENDTHEOREM
\THEOREM LAST snoc
|- !h t. LAST(SNOC h t) = h
\ENDTHEOREM
\THEOREM LAST\_BUTLAST\_exist snoc
|- !l. ~NULL l ==> (?h t. SNOC h t = l)
\ENDTHEOREM
\THEOREM LAST\_CONS snoc
|- !h t. LAST(CONS h t) = (NULL t => h | LAST t)
\ENDTHEOREM
\THEOREM LAST\_CONS\_NOT\_NULL snoc
|- !h l. ~NULL l ==> (LAST(CONS h l) = LAST l)
\ENDTHEOREM
\THEOREM LAST\_DEF snoc
|- !l. LAST l = (@h. ?t. SNOC h t = l)
\ENDTHEOREM
\THEOREM LAST\_EL snoc
|- !a. LAST[a] = a
\ENDTHEOREM
\THEOREM LAST\_REVERSE\_EQ\_HD snoc
|- !l. ~NULL l ==> (LAST(REVERSE l) = HD l)
\ENDTHEOREM
\THEOREM LAST\_TL snoc
|- !l. 1 < (LENGTH l) ==> (LAST(TL l) = LAST l)
\ENDTHEOREM
\THEOREM LENGTH\_BUTLAST snoc
|- !l. ~NULL l ==> (LENGTH(BUTLAST l) = PRE(LENGTH l))
\ENDTHEOREM
\THEOREM LENGTH\_SNOC snoc
|- !l n.
    (LENGTH l = SUC n) = (?h l'. (LENGTH l' = n) /\ (l = SNOC h l'))
\ENDTHEOREM
\THEOREM LENGTH\_TL snoc
|- !l. ~NULL l ==> (LENGTH(TL l) = PRE(LENGTH l))
\ENDTHEOREM
\THEOREM NOT\_NIL\_SNOC snoc
|- !h t. ~([] = SNOC h t)
\ENDTHEOREM
\THEOREM NOT\_SNOC\_NIL snoc
|- !h t. ~(SNOC h t = [])
\ENDTHEOREM
\THEOREM REVERSE\_CLAUSES snoc
|- (REVERSE[] = []) /\
   (!h l. REVERSE(CONS h l) = SNOC h(REVERSE l)) /\
   (!d l. REVERSE(SNOC d l) = CONS d(REVERSE l)) /\
   (!l. REVERSE(REVERSE l) = l)
\ENDTHEOREM
\THEOREM REVERSE\_DEF snoc
|- (REVERSE[] = []) /\ (!h l. REVERSE(CONS h l) = SNOC h(REVERSE l))
\ENDTHEOREM
\THEOREM REVERSE\_EQ\_NIL snoc
|- !l. (REVERSE l = []) = (l = [])
\ENDTHEOREM
\THEOREM REVERSE\_EXISTS snoc
|- !s. ?t. t = REVERSE s
\ENDTHEOREM
\THEOREM REVERSE\_NULL snoc
|- !l. NULL(REVERSE l) = NULL l
\ENDTHEOREM
\THEOREM REVERSE\_REVERSE snoc
|- !l. REVERSE(REVERSE l) = l
\ENDTHEOREM
\THEOREM REVERSE\_SINGLE snoc
|- !h. REVERSE[h] = [h]
\ENDTHEOREM
\THEOREM SAME\_LENGTH\_SNOC snoc
|- !l a b.
    (LENGTH l = LENGTH(SNOC a b)) =
    (?a' b'. (LENGTH b' = LENGTH b) /\ (l = SNOC a' b'))
\ENDTHEOREM
\THEOREM SNOC snoc
|- !l. ~NULL l ==> (SNOC(LAST l)(BUTLAST l) = l)
\ENDTHEOREM
\THEOREM SNOC\_11 snoc
|- !h t h' t'. (SNOC h t = SNOC h' t') = (h = h') /\ (t = t')
\ENDTHEOREM
\THEOREM SNOC\_Axiom snoc
|- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(SNOC h t) = f(fn t)h t)
\ENDTHEOREM
\THEOREM SNOC\_CASES snoc
|- !l. (l = []) \/ (?t h. l = SNOC h t)
\ENDTHEOREM
\THEOREM SNOC\_DEF snoc
|- (!d. SNOC d[] = [d]) /\ (!d h t. SNOC d(CONS h t) = CONS h(SNOC d t))
\ENDTHEOREM
\THEOREM SNOC\_EQ\_LENGTH\_EQ snoc
|- !l1 y1 l2 y2. (SNOC y1 l1 = SNOC y2 l2) ==> (LENGTH l1 = LENGTH l2)
\ENDTHEOREM
\THEOREM SNOC\_INDUCT snoc
|- !P. P[] /\ (!t. P t ==> (!h. P(SNOC h t))) ==> (!l. P l)
\ENDTHEOREM
\THEOREM SNOC\_NOT\_NULL snoc
|- !d l. ~NULL(SNOC d l)
\ENDTHEOREM
\THEOREM SNOC\_NULL\_CASES snoc
|- !l. NULL l \/ (?t h. l = SNOC h t)
\ENDTHEOREM
\THEOREM SNOC\_ONE\_ONE snoc
|- !h t h' t'. (SNOC h t = SNOC h' t') ==> (h = h') /\ (t = t')
\ENDTHEOREM
\THEOREM SNOC\_REVERSE\_CONS snoc
|- !d l. SNOC d l = REVERSE(CONS d(REVERSE l))
\ENDTHEOREM
\THEOREM TL\_SNOC snoc
|- !h t. TL(SNOC h t) = (NULL t => [] | SNOC h(TL t))
\ENDTHEOREM
\section{Theorems about {\tt TAIL}}
\THEOREM CON tail
|- !l. ~NULL l ==> (CONS(HD l)(TAIL l) = l)
\ENDTHEOREM
\THEOREM LENGTH\_TAIL tail
|- !l. ~NULL l ==> (LENGTH(TAIL l) = (LENGTH l) - 1)
\ENDTHEOREM
\THEOREM list\_CASES2 tail
|- !l. (l = []) \/ (l = CONS(HD l)(TAIL l))
\ENDTHEOREM
\THEOREM list\_NULL\_CASES2 tail
|- !l. NULL l \/ (l = CONS(HD l)(TAIL l))
\ENDTHEOREM
\THEOREM NOT\_NULL\_TAIL tail
|- !l. ~NULL(TAIL l) ==> ~NULL l
\ENDTHEOREM
\THEOREM TAIL tail
|- (TAIL[] = []) /\ (!h t. TAIL(CONS h t) = t)
\ENDTHEOREM
\THEOREM TAIL\_APPEND tail
|- !x y. TAIL(APPEND x y) = ((x = []) => TAIL y | APPEND(TAIL x)y)
\ENDTHEOREM
\THEOREM TL\_TAIL tail
|- !l. ~NULL l ==> (TL l = TAIL l)
\ENDTHEOREM
\section{Theorems about {\tt APPEND} and Related Operators}
\THEOREM APPEND\_11 append
|- !x y z. (APPEND x y = APPEND x z) = (y = z)
\ENDTHEOREM
\THEOREM APPEND\_BUTLAST\_LAST append
|- !l. ~NULL l ==> (APPEND(BUTLAST l)[LAST l] = l)
\ENDTHEOREM
\THEOREM APPEND\_CLAUSES append
|- (!l. APPEND[]l = l) /\
   (!l1. APPEND l1[] = l1) /\
   (!l1 l2 h. APPEND(CONS h l1)l2 = CONS h(APPEND l1 l2)) /\
   (!d l1 l2. APPEND l1(SNOC d l2) = SNOC d(APPEND l1 l2))
\ENDTHEOREM
\THEOREM APPEND\_CONS append
|- !l1 l2 h. APPEND(CONS h l1)l2 = APPEND[h](APPEND l1 l2)
\ENDTHEOREM
\THEOREM APPEND\_CONS\_EQ\_APPEND append
|- !l1 l2 h. APPEND l1(CONS h l2) = APPEND(APPEND l1[h])l2
\ENDTHEOREM
\THEOREM APPEND\_CONS\_EQ\_APPEND\_SNOC append
|- !l1 l2 h. APPEND l1(CONS h l2) = APPEND(SNOC h l1)l2
\ENDTHEOREM
\THEOREM APPEND\_EL\_11 append
|- !l1 y1 l2 y2.
    (APPEND l1[y1] = APPEND l2[y2]) = (l1 = l2) /\ ([y1] = [y2])
\ENDTHEOREM
\THEOREM APPEND\_EL\_REVERSE\_CONS append
|- !t h. APPEND t[h] = REVERSE(CONS h(REVERSE t))
\ENDTHEOREM
\THEOREM APPEND\_ID append
|- !l l'. (l = APPEND l l') = (l' = [])
\ENDTHEOREM
\THEOREM APPEND\_ID\_NULL append
|- !l l'. (l = APPEND l l') = NULL l'
\ENDTHEOREM
\THEOREM APPEND\_IS\_NIL append
|- !l1 l2. (APPEND l1 l2 = []) = (l1 = []) /\ (l2 = [])
\ENDTHEOREM
\THEOREM APPEND\_IS\_NULL append
|- !l1 l2. NULL(APPEND l1 l2) = NULL l1 /\ NULL l2
\ENDTHEOREM
\THEOREM APPEND\_JOIN append
|- !l1 l2.
    ~NULL l1 /\ ~NULL l2 ==>
    (APPEND l1 l2 = APPEND(BUTLAST l1)(APPEND[LAST l1;HD l2](TL l2)))
\ENDTHEOREM
\THEOREM APPEND\_LENGTH\_EQ append
|- !l1 l1'.
    (LENGTH l1 = LENGTH l1') ==>
    (!l2 l2'.
      (LENGTH l2 = LENGTH l2') ==>
      ((APPEND l1 l2 = APPEND l1' l2') = (l1 = l1') /\ (l2 = l2')))
\ENDTHEOREM
\THEOREM APPEND\_NIL append
|- (!l. APPEND l[] = l) /\ (!l. APPEND[]l = l)
\ENDTHEOREM
\THEOREM BUTLAST1 append
|- !l y. BUTLAST(APPEND l[y]) = l
\ENDTHEOREM
\THEOREM BUTLAST\_APPEND append
|- !l2.
    ~NULL l2 ==> (!l1. BUTLAST(APPEND l1 l2) = APPEND l1(BUTLAST l2))
\ENDTHEOREM
\THEOREM CONS\_APPEND\_CONS append
|- !a l. CONS a l = APPEND[a]l
\ENDTHEOREM
\THEOREM CONS\_MEMBER\_LIST append
|- !s s' t a.
    (APPEND s t = CONS a s') ==>
    (s = []) \/ (?r. (s = CONS a r) /\ (s' = APPEND r t))
\ENDTHEOREM
\THEOREM CONS\_MEMBER\_LIST\_NULL append
|- !s s' t a.
    (APPEND s t = CONS a s') ==>
    NULL s \/ (?r. (s = CONS a r) /\ (s' = APPEND r t))
\ENDTHEOREM
\THEOREM HD\_APPEND append
|- !l1. ~(l1 = []) ==> (!l2. HD(APPEND l1 l2) = HD l1)
\ENDTHEOREM
\THEOREM HD\_APPEND\_NULL append
|- !l1. ~NULL l1 ==> (!l2. HD(APPEND l1 l2) = HD l1)
\ENDTHEOREM
\THEOREM HEAD\_APPEND append
|- !x y. HD(APPEND x y) = ((x = []) => HD y | HD x)
\ENDTHEOREM
\THEOREM HEAD\_APPEND\_NULL append
|- !x y. HD(APPEND x y) = (NULL x => HD y | HD x)
\ENDTHEOREM
\THEOREM IMP\_APPEND\_NOT\_NIL append
|- !l1 l2. ~(l1 = []) \/ ~(l2 = []) ==> ~(APPEND l1 l2 = [])
\ENDTHEOREM
\THEOREM IMP\_APPEND\_NOT\_NULL append
|- !l1 l2. ~NULL l1 \/ ~NULL l2 ==> ~NULL(APPEND l1 l2)
\ENDTHEOREM
\THEOREM ITERATED append
|- (!s. ITERATED 0 s = []) /\
   (!n s. ITERATED(SUC n)s = APPEND s(ITERATED n s))
\ENDTHEOREM
\THEOREM ITERATED\_EMPTY append
|- !n. ITERATED n[] = []
\ENDTHEOREM
\THEOREM LAST1 append
|- !l y. LAST(APPEND l[y]) = y
\ENDTHEOREM
\THEOREM LAST\_APPEND append
|- !l2. ~NULL l2 ==> (!l1. LAST(APPEND l1 l2) = LAST l2)
\ENDTHEOREM
\THEOREM LENGTH\_APPEND\_EL append
|- !l1 y1 l2 y2.
    (APPEND l1[y1] = APPEND l2[y2]) ==> (LENGTH l1 = LENGTH l2)
\ENDTHEOREM
\THEOREM LENGTH\_CLAUSES append
|- (LENGTH[] = 0) /\
   (!h t. LENGTH(CONS h t) = SUC(LENGTH t)) /\
   (!d l. LENGTH(SNOC d l) = SUC(LENGTH l)) /\
   (!l1 l2. LENGTH(APPEND l1 l2) = (LENGTH l1) + (LENGTH l2)) /\
   (!l. LENGTH(REVERSE l) = LENGTH l)
\ENDTHEOREM
\THEOREM LENGTH\_REPLICATE append
|- !x n. LENGTH(REPLICATE n x) = n
\ENDTHEOREM
\THEOREM list\_APPEND\_Axiom append
|- !x f. ?! fa. (fa[] = x) /\ (!h t. fa(APPEND t[h]) = f(fa t)h t)
\ENDTHEOREM
\THEOREM list\_APPEND\_CASES append
|- !l. (l = []) \/ (?t h. l = APPEND t[h])
\ENDTHEOREM
\THEOREM list\_APPEND\_INDUCT append
|- !P. P[] /\ (!t. P t ==> (!h. P(APPEND t[h]))) ==> (!l. P l)
\ENDTHEOREM
\THEOREM list\_APPEND\_NULL\_CASES append
|- !l. NULL l \/ (?t h. l = APPEND t[h])
\ENDTHEOREM
\THEOREM NIL\_NOT\_APPEND\_CONS2 append
|- !l1 l2. (l2 = CONS h t) ==> ~([] = APPEND l1 l2)
\ENDTHEOREM
\THEOREM NOT\_NIL\_APPEND\_EL append
|- !l h. ~([] = APPEND l[h])
\ENDTHEOREM
\THEOREM NULL\_ITERATED append
|- !n. NULL(ITERATED n[])
\ENDTHEOREM
\THEOREM NULL\_NOT\_APPEND\_CONS append
|- !l1 l2. (l2 = CONS h t) ==> ~([] = APPEND l1 l2)
\ENDTHEOREM
\THEOREM ONE\_MEMBER\_LIST append
|- !s t a. (APPEND s t = [a]) ==> (s = []) \/ (s = [a])
\ENDTHEOREM
\THEOREM ONE\_MEMBER\_LIST\_NULL append
|- !s t a. (APPEND s t = [a]) ==> NULL s \/ (s = [a])
\ENDTHEOREM
\THEOREM REPLICATE append
|- (!in. REPLICATE 0 in = []) /\
   (!n in. REPLICATE(SUC n)in = CONS in(REPLICATE n in))
\ENDTHEOREM
\THEOREM REVERSE append
|- (REVERSE[] = []) /\ (!h t. REVERSE(CONS h t) = APPEND(REVERSE t)[h])
\ENDTHEOREM
\THEOREM REVERSE\_APPEND append
|- !l1 l2. REVERSE(APPEND l2 l1) = APPEND(REVERSE l1)(REVERSE l2)
\ENDTHEOREM
\THEOREM REVERSE\_APPEND\_EL\_CONS append
|- !h t. REVERSE(APPEND t[h]) = CONS h(REVERSE t)
\ENDTHEOREM
\THEOREM SNOC\_APPEND\_CONS append
|- !l h. SNOC h l = APPEND l[h]
\ENDTHEOREM
\THEOREM SUBSEQUENCE\_EXISTS append
|- !s. ?a b. s = APPEND a b
\ENDTHEOREM
\THEOREM TL\_APPEND append
|- !l1. ~(l1 = []) ==> (!l2. TL(APPEND l1 l2) = APPEND(TL l1)l2)
\ENDTHEOREM
\THEOREM TL\_APPEND\_NULL append
|- !l1. ~NULL l1 ==> (!l2. TL(APPEND l1 l2) = APPEND(TL l1)l2)
\ENDTHEOREM
\section{Theorems about Higher Order Functions}
\THEOREM EVERY\_APPEND map
|- !l1 l2 P. EVERY P(APPEND l1 l2) = EVERY P l1 /\ EVERY P l2
\ENDTHEOREM
\THEOREM EVERY\_MAP map
|- !f P l. EVERY P(MAP f l) = EVERY(P o f)l
\ENDTHEOREM
\THEOREM EVERY\_SNOC snoc
|- !P h l. EVERY P(SNOC h l) = EVERY P l /\ P 
\ENDTHEOREM
\THEOREM HD\_MAP map
|- !f l. ~NULL l ==> (HD(MAP f l) = f(HD l))
\ENDTHEOREM
\THEOREM ITLIST map
|- (!f x. ITLIST f[]x = x) /\
   (!f hd tl x. ITLIST f(CONS hd tl)x = f hd(ITLIST f tl x))
\ENDTHEOREM
\THEOREM ITLIST\_MAP\_EQ map
|- !f g l. ITLIST $/\(MAP(\x. f x = g x)l)T = (MAP f l = MAP g l)
\ENDTHEOREM
\THEOREM MAP2\_SNOC map
|- !f h1 h2 l1 l2.
    (LENGTH l1 = LENGTH l2) ==>
    (MAP2 f(SNOC h1 l1)(SNOC h2 l2) = SNOC(f h1 h2)(MAP2 f l1 l2))
\ENDTHEOREM
\THEOREM MAP\_MAP\_o map
|- !f g l. MAP f(MAP g l) = MAP(f o g)l
\ENDTHEOREM
\THEOREM MAP\_SNOC map
|- !f h t. MAP f(SNOC h t) = SNOC(f h)(MAP f t)
\ENDTHEOREM
\THEOREM NULL\_MAP map
|- !f l. NULL(MAP f l) = NULL l
\ENDTHEOREM
\THEOREM TAIL\_MAP map
|- !f l. TAIL(MAP f l) = MAP f(TAIL l)
\ENDTHEOREM
\THEOREM TL\_MAP map
|- !f l. ~NULL l ==> (TL(MAP f l) = MAP f(TL l))
\ENDTHEOREM
\section{Theorems about {\tt EL} and {\tt EL1}}
\THEOREM EL1 el
|- !n l. EL1(SUC n)l = EL n l
\ENDTHEOREM
\THEOREM EL1\_HD el
|- !l. ~NULL l ==> (EL1 1 l = HD l)
\ENDTHEOREM
\THEOREM EL1\_SUC\_CONS el
|- !n h l. 0 < n ==> (EL1(SUC n)(CONS h l) = EL1 n l)
\ENDTHEOREM
\THEOREM EL\_0\_REVERSE el
|- !l. ~NULL l ==> (EL 0(REVERSE l) = EL(PRE(LENGTH l))l)
\ENDTHEOREM
\THEOREM EL\_APPEND\_1 el
|- !l1 l2 k. k < (LENGTH l1) ==> (EL k(APPEND l1 l2) = EL k l1)
\ENDTHEOREM
\THEOREM EL\_APPEND\_2 el
|- !l1 l2 k.
    (LENGTH l1) <= k ==> (EL k(APPEND l1 l2) = EL(k - (LENGTH l1))l2)
\ENDTHEOREM
\THEOREM EL\_APPEND\_EL el
|- !l y k. k < (LENGTH l) ==> (EL k(APPEND l[y]) = EL k l)
\ENDTHEOREM
\THEOREM EL\_BUTLAST el
|- !l x. ~NULL l ==> (SUC x) < (LENGTH l) ==> (EL x(BUTLAST l) = EL x l)
\ENDTHEOREM
\THEOREM EL\_CONS el
|- !k l y. 0 < k ==> (EL k(CONS y l) = EL(PRE k)l)
\ENDTHEOREM
\THEOREM EL\_CONS\_SUB1 el
|- !n h l. ~(n = 0) ==> (EL n(CONS h l) = EL(n - 1)l)
\ENDTHEOREM
\THEOREM EL\_HD el
|- !l. ~NULL l ==> (EL 0 l = HD l)
\ENDTHEOREM
\THEOREM EL\_LENGTH\_APPEND el
|- !l1 l2. ~NULL l2 ==> (EL(LENGTH l1)(APPEND l1 l2) = HD l2)
\ENDTHEOREM
\THEOREM EL\_MAP el
|- !f l n. n < (LENGTH l) ==> (EL n(MAP f l) = f(EL n l))
\ENDTHEOREM
\THEOREM EL\_MAP2 el
|- !f l l' n.
    (LENGTH l = LENGTH l') ==>
    n < (LENGTH l) \/ n < (LENGTH l') ==>
    (EL n(MAP2 f l l') = f(EL n l)(EL n l'))
\ENDTHEOREM
\THEOREM EL\_REPLICATE el
|- !x n m. m < n ==> (EL m(REPLICATE n x) = x)
\ENDTHEOREM
\THEOREM EL\_REVERSE el
|- !l k.
    k < (PRE(LENGTH l)) ==> (EL k(REVERSE l) = EL((PRE(LENGTH l)) - k)l)
\ENDTHEOREM
\THEOREM EL\_SNOC el
|- !l y k. k < (LENGTH l) ==> (EL k(SNOC y l) = EL k l)
\ENDTHEOREM
\THEOREM EXISTS\_EL el
|- !n a. ?l. EL n l = a
\ENDTHEOREM
\THEOREM LAST\_EL\_LENGTH el
|- !l. ~NULL l ==> (LAST l = EL(PRE(LENGTH l))l)
\ENDTHEOREM
\THEOREM MAP2\_EL el
|- !f l l' n.
    (LENGTH l = LENGTH l') ==>
    n < (LENGTH l) \/ n < (LENGTH l') ==>
    (MAP2 f[EL n l][EL n l'] = [f(EL n l)(EL n l')])
\ENDTHEOREM
\THEOREM MAP\_EL el
|- !f l n. n < (LENGTH l) ==> (MAP f[EL n l] = [f(EL n l)])
\ENDTHEOREM
\THEOREM MAP\_EL1\_SUC\_CONS el
|- !l l' h'.
    EVERY(\n. 0 < n)l ==>
    (MAP(\n. EL1(SUC n)(CONS h' l'))l = MAP(\n. EL1 n l')l)
\ENDTHEOREM
\section{Theorems about {\tt ELL}}
\THEOREM ELL ell
|- (!l. ELL 0 l = LAST l) /\ (!n l. ELL(SUC n)l = ELL n(BUTLAST l))
\ENDTHEOREM
\THEOREM ELL\_APPEND\_1 ell
|- !l1 l2 k. k < (LENGTH l2) ==> (ELL k(APPEND l1 l2) = ELL k l2)
\ENDTHEOREM
\THEOREM ELL\_APPEND\_2 ell
|- !l1 l2 k.
    (LENGTH l2) <= k ==> (ELL k(APPEND l1 l2) = ELL(k - (LENGTH l2))l1)
\ENDTHEOREM
\THEOREM ELL\_CONS ell
|- !l x k. k < (LENGTH l) ==> (ELL k(CONS x l) = ELL k l)
\ENDTHEOREM
\THEOREM ELL\_EL ell
|- !l k. k < (LENGTH l) ==> (ELL k l = EL(PRE((LENGTH l) - k))l)
\ENDTHEOREM
\THEOREM ELL\_LAST ell
|- !l. ~NULL l ==> (ELL 0 l = LAST l)
\ENDTHEOREM
\THEOREM ELL\_LENGTH\_APPEND ell
|- !l1 l2. ~NULL l1 ==> (ELL(LENGTH l2)(APPEND l1 l2) = LAST l1)
\ENDTHEOREM
\THEOREM ELL\_MAP ell
|- !f l n. n < (LENGTH l) ==> (ELL n(MAP f l) = f(ELL n l))
\ENDTHEOREM
\THEOREM ELL\_MAP2 ell
|- !f l l' n.
    (LENGTH l = LENGTH l') ==>
    n < (LENGTH l) \/ n < (LENGTH l') ==>
    (ELL n(MAP2 f l l') = f(ELL n l)(ELL n l'))
\ENDTHEOREM
\THEOREM ELL\_SNOC ell
|- !l x k. 0 < k ==> (ELL k(SNOC x l) = ELL(PRE k)l)
\ENDTHEOREM
\THEOREM ELL\_SNOC0 ell
|- !l x. ELL 0(SNOC x l) = x
\ENDTHEOREM
\THEOREM ELL\_SUC\_SNOC ell
|- !k x l. ELL(SUC k)(SNOC x l) = ELL k l
\ENDTHEOREM
\THEOREM EL\_ELL ell
|- !l k. k < (LENGTH l) ==> (EL k l = ELL(PRE((LENGTH l) - k))l)
\ENDTHEOREM
\THEOREM HD\_ELL\_LENGTH\_CONS ell
|- !l x. ELL(LENGTH l)(CONS x l) = x
\ENDTHEOREM
\THEOREM HD\_ELL\_LENGTH\_SNOC ell
|- !l x. ELL(LENGTH l)(SNOC x l) = (NULL l => x | HD l)
\ENDTHEOREM
\THEOREM HD\_ELL\_PRE\_LENGTH ell
|- !l. ~NULL l ==> (ELL(PRE(LENGTH l))l = HD l)
\ENDTHEOREM
\THEOREM MAP2\_ELL ell
|- !f l l' n.
    (LENGTH l = LENGTH l') ==>
    n < (LENGTH l) \/ n < (LENGTH l') ==>
    (MAP2 f[ELL n l][ELL n l'] = [f(ELL n l)(ELL n l')])
\ENDTHEOREM
\THEOREM MAP\_ELL ell
|- !f l n. n < (LENGTH l) ==> (MAP f[ELL n l] = [f(ELL n l)])
\ENDTHEOREM
\section{Theorems about Accessing Subsequences of Lists from the Front}
\THEOREM APPEND\_FIRSTN\_NTL subseq
|- !X n. n <= (LENGTH X) ==> (APPEND(FIRSTN n X)(NTL n X) = X)
\ENDTHEOREM
\THEOREM APPEND\_SUBSEQ subseq
|- !r x y. (?n. r = APPEND x(SUBSEQ n y)) ==> (?a. r = APPEND x a)
\ENDTHEOREM
\THEOREM APPEND\_SUBSEQ2 subseq
|- !r s x y.
    (APPEND r s = APPEND x y) /\ (LENGTH x) <= (LENGTH r) ==>
    (?a. r = APPEND x a)
\ENDTHEOREM
\THEOREM EL\_HD\_NTAIL subseq
|- !x l. ~NULL(NTAIL x l) ==> (EL x l = HD(NTAIL x l))
\ENDTHEOREM
\THEOREM EL\_NTAIL\_1 subseq
|- !x l.
    ~NULL(NTAIL x l) ==> (APPEND[EL x l](NTAIL(x + 1)l) = NTAIL x l)
\ENDTHEOREM
\THEOREM FIRSTN subseq
|- (!X. FIRSTN 0 X = []) /\
   (!n X. FIRSTN(SUC n)X = CONS(HD X)(FIRSTN n(TL X)))
\ENDTHEOREM
\THEOREM FIRSTN\_APPEND1 subseq
|- !x X n. n <= (LENGTH X) ==> (FIRSTN n(APPEND X[x]) = FIRSTN n X)
\ENDTHEOREM
\THEOREM FIRSTN\_FIRSTN subseq
|- !X n m.
    m <= (LENGTH X) ==> n <= m ==> (FIRSTN n(FIRSTN m X) = FIRSTN n X)
\ENDTHEOREM
\THEOREM FIRSTN\_LENGTH\_ID subseq
|- !X. FIRSTN(LENGTH X)X = X
\ENDTHEOREM
\THEOREM FIRSTN\_NIL subseq
|- !n X. (FIRSTN n X = []) ==> (n = 0)
\ENDTHEOREM
\THEOREM FIRSTN\_NULL subseq
|- !n X. NULL(FIRSTN n X) ==> (n = 0)
\ENDTHEOREM
\THEOREM LENGTH\_FIRSTN subseq
|- !n X. n <= (LENGTH X) ==> (LENGTH(FIRSTN n X) = n)
\ENDTHEOREM
\THEOREM LENGTH\_NTAIL subseq
|- !x l. LENGTH(NTAIL x l) = (LENGTH l) - x
\ENDTHEOREM
\THEOREM LENGTH\_NTAIL\_LESS subseq
|- !l1 l2 x.
    ~NULL l2 /\ (l1 = NTAIL x l2) /\ 0 < x ==> (LENGTH l1) < (LENGTH l2)
\ENDTHEOREM
\THEOREM NOT\_NULL\_NTAIL subseq
|- !x l. ~NULL(NTAIL x l) ==> ~NULL l
\ENDTHEOREM
\THEOREM NOT\_NULL\_NTAIL\_TL subseq
|- !x l. ~NULL(TAIL(NTAIL x l)) ==> ~NULL(NTAIL x(TL l))
\ENDTHEOREM
\THEOREM NTAIL subseq
|- (!l. NTAIL 0 l = l) /\ (!n l. NTAIL(SUC n)l = TAIL(NTAIL n l))
\ENDTHEOREM
\THEOREM NTAIL\_NIL subseq
|- !n. NTAIL n[] = []
\ENDTHEOREM
\THEOREM NTAIL\_NTAIL subseq
|- !x y l. NTAIL x(NTAIL y l) = NTAIL(x + y)l
\ENDTHEOREM
\THEOREM NTAIL\_TAIL subseq
|- !x l. NTAIL x(TAIL l) = NTAIL(SUC x)l
\ENDTHEOREM
\THEOREM NTL subseq
|- (!X. NTL 0 X = X) /\ (!n X. NTL(SUC n)X = NTL n(TL X))
\ENDTHEOREM
\THEOREM NTL\_APPEND subseq
|- !X Y n. n <= (LENGTH X) ==> (NTL n(APPEND X Y) = APPEND(NTL n X)Y)
\ENDTHEOREM
\THEOREM NTL\_LENGTH subseq
|- !n X. n <= (LENGTH X) ==> (LENGTH(NTL n X) = (LENGTH X) - n)
\ENDTHEOREM
\THEOREM NTL\_LENGTH\_APPEND subseq
|- !l1 l2. NTL(LENGTH l1)(APPEND l1 l2) = l2
\ENDTHEOREM

\THEOREM NTL\_LENGTH\_NIL subseq
|- !X. NTL(LENGTH X)X = []
\ENDTHEOREM
\THEOREM NTL\_LENGTH\_NULL subseq
|- !X. NULL(NTL(LENGTH X)X)
\ENDTHEOREM
\THEOREM NTL\_NTL subseq
|- !X n m. (n + m) <= (LENGTH X) ==> (NTL n(NTL m X) = NTL(n + m)X)
\ENDTHEOREM
\THEOREM NTL\_SIMP\_REC subseq
|- !n X. NTL n X = SIMP_REC X TL n
\ENDTHEOREM
\THEOREM NTL\_TL\_SYM subseq
|- !n X. NTL n(TL X) = TL(NTL n X)
\ENDTHEOREM
\THEOREM NULL\_NTAIL subseq
|- !n. NULL(NTAIL n[])
\ENDTHEOREM
\THEOREM NULL\_SUBSEQ subseq
|- !n. NULL(SUBSEQ n[])
\ENDTHEOREM
\THEOREM SUBSEQ subseq
|- (!x. SUBSEQ 0 x = []) /\
   (!n x.
     SUBSEQ(SUC n)x = (NULL x => [] | CONS(HD x)(SUBSEQ n(TAIL x))))
\ENDTHEOREM
\THEOREM SUBSEQ2 subseq
|- !n x y. CONS x(SUBSEQ n y) = SUBSEQ(SUC n)(CONS x y)
\ENDTHEOREM
\THEOREM SUBSEQUENCES subseq
|- !r s x y.
    (APPEND r s = APPEND x y) ==>
    (?a. r = APPEND x a) \/ (?a. x = APPEND r a)
\ENDTHEOREM
\THEOREM SUBSEQ\_APPEND subseq
|- !x y n. SUBSEQ((LENGTH x) + n)(APPEND x y) = APPEND x(SUBSEQ n y)
\ENDTHEOREM
\THEOREM SUBSEQ\_APPEND2 subseq
|- !x y. SUBSEQ(LENGTH x)(APPEND x y) = x
\ENDTHEOREM
\THEOREM SUBSEQ\_EMPTY\_LIST subseq
|- !n. SUBSEQ n[] = []
\ENDTHEOREM
\THEOREM SUBSEQ\_EQ subseq
|- !x y n. (x = y) ==> (SUBSEQ n x = SUBSEQ n y)
\ENDTHEOREM
\THEOREM SUBSEQ\_EXISTS subseq
|- !s n. ?a. s = APPEND(SUBSEQ n s)a
\ENDTHEOREM
\THEOREM SUBSEQ\_MAP subseq
|- !n s f. SUBSEQ n(MAP f s) = MAP f(SUBSEQ n s)
\ENDTHEOREM
\THEOREM SUBSEQ\_SUBSEQ subseq
|- !n x. SUBSEQ n(SUBSEQ n x) = SUBSEQ n x
\ENDTHEOREM
\THEOREM TAIL\_NTAIL subseq
|- !x l. TAIL(NTAIL x l) = NTAIL x(TAIL l)
\ENDTHEOREM
\section{Theorems about  Accessing Subsequences of Lists from the Tail End}
\THEOREM APPEND\_FIRSTN\_LASTN last\_subseq
|- !X m n. (LENGTH X = m + n) ==> (APPEND(FIRSTN n X)(LASTN m X) = X)
\ENDTHEOREM
\THEOREM APPEND\_LASTN\_LASTN last\_subseq
|- !l m1 m2.
    (m1 + m2) <= (LENGTH l) ==>
    (APPEND(LASTN m2(NBUTLAST m1 l))(LASTN m1 l) = LASTN(m1 + m2)l)
\ENDTHEOREM
\THEOREM APPEND\_NBUTLAST\_LASTN last\_subseq
|- !n X. n <= (LENGTH X) ==> (APPEND(NBUTLAST n X)(LASTN n X) = X)
\ENDTHEOREM
\THEOREM APPEND\_NBUTLAST\_NTL last\_subseq
|- !X m n. (LENGTH X = m + n) ==> (APPEND(NBUTLAST n X)(NTL m X) = X)
\ENDTHEOREM
\THEOREM BUTLAST\_TO\_NBUTLAST last\_subseq
|- !l. ~NULL l ==> (BUTLAST l = NBUTLAST 1 l)
\ENDTHEOREM
\THEOREM ELL\_LASTN last\_subseq
|- !l m j. m <= (LENGTH l) ==> j < m ==> (ELL j(LASTN m l) = ELL j l)
\ENDTHEOREM
\THEOREM ELL\_NBUTLAST last\_subseq
|- !l k j. (j + k) <= (LENGTH l) ==> (ELL j(NBUTLAST k l) = ELL(j + k)l)
\ENDTHEOREM
\THEOREM EL\_NBUTLAST last\_subseq
|- !l x k.
    k < (LENGTH l) /\ x < ((LENGTH l) - k) ==>
    (EL x(NBUTLAST k l) = EL x l)
\ENDTHEOREM
\THEOREM EVERY\_LASTN last\_subseq
|- !P l. EVERY P l ==> (!m. m <= (LENGTH l) ==> EVERY P(LASTN m l))
\ENDTHEOREM
\THEOREM LASTN last\_subseq
|- (!X. LASTN 0 X = []) /\
   (!n X. LASTN(SUC n)X = APPEND(LASTN n(BUTLAST X))[LAST X])
\ENDTHEOREM
\THEOREM LASTN\_APPEND last\_subseq
|- !l1 l2 n. n <= (LENGTH l2) ==> (LASTN n(APPEND l1 l2) = LASTN n l2)
\ENDTHEOREM
\THEOREM LASTN\_APPEND2 last\_subseq
|- !l1 l2 n.
    (LENGTH l2) <= n ==>
    (LASTN n(APPEND l1 l2) = APPEND(LASTN(n - (LENGTH l2))l1)l2)
\ENDTHEOREM
\THEOREM LASTN\_CONS last\_subseq
|- !x X n. n <= (LENGTH X) ==> (LASTN n(CONS x X) = LASTN n X)
\ENDTHEOREM
\THEOREM LASTN\_LASTN last\_subseq
|- !X n m.
    m <= (LENGTH X) ==> n <= m ==> (LASTN n(LASTN m X) = LASTN n X)
\ENDTHEOREM
\THEOREM LASTN\_LENGTH\_APPEND last\_subseq
|- !l1 l2. LASTN(LENGTH l2)(APPEND l1 l2) = l2
\ENDTHEOREM
\THEOREM LASTN\_LENGTH\_ID last\_subseq
|- !X. LASTN(LENGTH X)X = X
\ENDTHEOREM
\THEOREM LASTN\_MAP last\_subseq
|- !f l n. n <= (LENGTH l) ==> (LASTN n(MAP f l) = MAP f(LASTN n l))
\ENDTHEOREM
\THEOREM LASTN\_MAP2 last\_subseq
|- !f l1 l2 n.
    (LENGTH l1 = LENGTH l2) ==>
    n <= (LENGTH l1) ==>
    (LASTN n(MAP2 f l1 l2) = MAP2 f(LASTN n l1)(LASTN n l2))
\ENDTHEOREM
\THEOREM LASTN\_NBUTLAST last\_subseq
|- !l i k.
    (i + k) < (LENGTH l) ==>
    (LASTN k(NBUTLAST i l) = NBUTLAST i(LASTN(i + k)l))
\ENDTHEOREM
\THEOREM LASTN\_NBUTLAST\_APPEND last\_subseq
|- !l1 l2 m k.
    (m + k) <= ((LENGTH l1) + (LENGTH l2)) /\
    k < (LENGTH l2) /\
    (LENGTH l2) <= (m + k) ==>
    (LASTN m(NBUTLAST k(APPEND l1 l2)) =
     APPEND
     (LASTN((m + k) - (LENGTH l2))l1)
     (LASTN((LENGTH l2) - k)(NBUTLAST k l2)))
\ENDTHEOREM
\THEOREM LASTN\_NBUTLAST\_TL\_SPLIT last\_subseq
|- !l m k.
    0 < m /\ (k + m) < (LENGTH l) ==>
    (LASTN m(NBUTLAST k l) =
     APPEND(LASTN(m - 1)(NBUTLAST(k + 1)l))(LASTN 1(NBUTLAST k l)))
\ENDTHEOREM
\THEOREM LASTN\_NIL last\_subseq
|- !n X. (LASTN n X = []) ==> (n = 0)
\ENDTHEOREM
\THEOREM LASTN\_NULL last\_subseq
|- !n X. NULL(LASTN n X) ==> (n = 0)
\ENDTHEOREM
\THEOREM LASTN\_SUC\_SNOC last\_subseq
|- !l x i. LASTN(SUC i)(SNOC x l) = SNOC x(LASTN i l)
\ENDTHEOREM
\THEOREM LAST\_LASTN last\_subseq
|- !l m. m <= (LENGTH l) ==> 0 < m ==> (LAST(LASTN m l) = LAST l)
\ENDTHEOREM
\THEOREM LAST\_NBUTLAST\_EL last\_subseq
|- !k l.
    k < (LENGTH l) ==> (LAST(NBUTLAST k l) = EL(PRE((LENGTH l) - k))l)
\ENDTHEOREM
\THEOREM LAST\_NBUTLAST\_ELL last\_subseq
|- !k l. k < (LENGTH l) ==> (LAST(NBUTLAST k l) = ELL k l)
\ENDTHEOREM
\THEOREM LAST\_TO\_LASTN last\_subseq
|- !l. ~NULL l ==> ([LAST l] = LASTN 1 l)
\ENDTHEOREM
\THEOREM LENGTH\_LASTN last\_subseq
|- !n X. n <= (LENGTH X) ==> (LENGTH(LASTN n X) = n)
\ENDTHEOREM
\THEOREM NBUTLAST last\_subseq
|- (!X. NBUTLAST 0 X = X) /\
   (!n X. NBUTLAST(SUC n)X = NBUTLAST n(BUTLAST X))
\ENDTHEOREM
\THEOREM NBUTLAST\_APPEND last\_subseq
|- !l1 l2 n.
    n <= (LENGTH l2) ==>
    (NBUTLAST n(APPEND l1 l2) = APPEND l1(NBUTLAST n l2))
\ENDTHEOREM
\THEOREM NBUTLAST\_APPEND1 last\_subseq
|- !l1 l2 k.
    (LENGTH l2) <= k ==>
    (NBUTLAST k(APPEND l1 l2) = NBUTLAST(k - (LENGTH l2))l1)
\ENDTHEOREM
\THEOREM NBUTLAST\_BUTLAST\_SYM last\_subseq
|- !n X. NBUTLAST n(BUTLAST X) = BUTLAST(NBUTLAST n X)
\ENDTHEOREM
\THEOREM NBUTLAST\_CONS last\_subseq
|- !h l2 n.
    n <= (LENGTH l2) ==> (NBUTLAST n(CONS h l2) = CONS h(NBUTLAST n l2))
\ENDTHEOREM
\THEOREM NBUTLAST\_LASTN last\_subseq
|- !l i k.
    i <= k /\ k <= (LENGTH l) ==>
    (NBUTLAST i(LASTN k l) = LASTN(k - i)(NBUTLAST i l))
\ENDTHEOREM
\THEOREM NBUTLAST\_LASTN\_NIL last\_subseq
|- !l i. i <= (LENGTH l) ==> (NBUTLAST i(LASTN i l) = [])
\ENDTHEOREM
\THEOREM NBUTLAST\_LENGTH last\_subseq
|- !n X. n <= (LENGTH X) ==> (LENGTH(NBUTLAST n X) = (LENGTH X) - n)
\ENDTHEOREM
\THEOREM NBUTLAST\_LENGTH\_APPEND last\_subseq
|- !l2 l1. NBUTLAST(LENGTH l2)(APPEND l1 l2) = APPEND l1[]
\ENDTHEOREM
\THEOREM NBUTLAST\_LENGTH\_CONS last\_subseq
|- !l h. NBUTLAST(LENGTH l)(CONS h l) = [h]
\ENDTHEOREM
\THEOREM NBUTLAST\_LENGTH\_NIL last\_subseq
|- !X. NBUTLAST(LENGTH X)X = []
\ENDTHEOREM
\THEOREM NBUTLAST\_LENGTH\_NULL last\_subseq
|- !X. NULL(NBUTLAST(LENGTH X)X)
\ENDTHEOREM
\THEOREM NBUTLAST\_MAP last\_subseq
|- !f l n.
    n <= (LENGTH l) ==> (NBUTLAST n(MAP f l) = MAP f(NBUTLAST n l))
\ENDTHEOREM
\THEOREM NBUTLAST\_MAP2 last\_subseq
|- !f l1 l2 n.
    (LENGTH l1 = LENGTH l2) ==>
    n <= (LENGTH l1) ==>
    (NBUTLAST n(MAP2 f l1 l2) = MAP2 f(NBUTLAST n l1)(NBUTLAST n l2))
\ENDTHEOREM
\THEOREM NBUTLAST\_NBUTLAST last\_subseq
|- !X n m.
    (n + m) <= (LENGTH X) ==>
    (NBUTLAST n(NBUTLAST m X) = NBUTLAST(n + m)X)
\ENDTHEOREM
\THEOREM NBUTLAST\_SIMP\_REC last\_subseq
|- !n X. NBUTLAST n X = SIMP_REC X BUTLAST n
\ENDTHEOREM
\THEOREM NBUTLAST\_SUC\_SNOC last\_subseq
|- !l x i. NBUTLAST(SUC i)(SNOC x l) = NBUTLAST i l
\ENDTHEOREM
\THEOREM NOT\_NULL\_NBUTLAST last\_subseq
|- !k l. k < (LENGTH l) ==> ~NULL(NBUTLAST k l)
\ENDTHEOREM
\section{Theorems about List Membership}
\THEOREM CONS\_LLEQ\_LEFT\_TL member
|- !l1 l2. (CONS h l1) LLEQ_LEFT l2 ==> l1 LLEQ_LEFT (TL l2)
\ENDTHEOREM
\THEOREM CONS\_LLESS\_LEFT\_APPEND\_HD member
|- !l l1 l2.
    ~NULL l1 /\ (CONS h l) LLESS_LEFT (APPEND l1 l2) ==> (h = HD l1)
\ENDTHEOREM
\THEOREM CONS\_LLESS\_LEFT\_HD member
|- !h l1 l2. (CONS h l1) LLESS_LEFT l2 ==> (h = HD l2)
\ENDTHEOREM
\THEOREM CONS\_LLESS\_LEFT\_TL member
|- !l1 l2. (CONS h l1) LLESS_LEFT l2 ==> l1 LLESS_LEFT (TL l2)
\ENDTHEOREM
\THEOREM LLEQ\_LEFT member
|- !l1 l2. l1 LLEQ_LEFT l2 = l1 LLESS_LEFT l2 \/ (l1 = l2)
\ENDTHEOREM
\THEOREM LLEQ\_RIGHT member
|- !l1 l2. l1 LLEQ_RIGHT l2 = l1 LLESS_RIGHT l2 \/ (l1 = l2)
\ENDTHEOREM
\THEOREM LLESS\_LEFT member
|- (!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))
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_APPEND member
|- !l l1 l2. l LLESS_LEFT l1 ==> l LLESS_LEFT (APPEND l1 l2)
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_APPEND\_LLEQ\_LEFT member
|- !l l1 l2.
    ~l LLESS_LEFT l1 /\ l LLESS_LEFT (APPEND l1 l2) ==> l1 LLEQ_LEFT l
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_CONS member
|- !l1 l2 h.
    (TL l1) LLESS_LEFT l2 /\ (h = HD l1) /\ ~NULL l1 ==>
    l1 LLESS_LEFT (CONS h l2)
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_CONS\_HD member
|- !l h t. l LLESS_LEFT (CONS h t) /\ ~NULL l ==> (h = HD l)
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_CONS\_TL\_LLESS\_LEFT member
|- !l h t. l LLESS_LEFT (CONS h t) /\ ~NULL l ==> (TL l) LLESS_LEFT t
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_EXISTS\_APPEND member
|- !l1 l2. l1 LLESS_LEFT l2 ==> (?l. l2 = APPEND l1 l)
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_LENGTH1\_NULL member
|- !l1 l2. l2 LLESS_LEFT l1 /\ (LENGTH l1 = 1) ==> NULL l2
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_NULL member
|- !l1 l2. l1 LLESS_LEFT l2 ==> ~NULL l2
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_SINGLE\_NULL member
|- !l h. l LLESS_LEFT [h] = NULL l
\ENDTHEOREM
\THEOREM LLESS\_RIGHT member
|- (!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))
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_APPEND member
|- !l l1 l2. l LLESS_RIGHT l2 ==> l LLESS_RIGHT (APPEND l1 l2)
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_APPEND\_LLEQ\_RIGHT member
|- !l l1 l2.
    ~l LLESS_RIGHT l2 /\ l LLESS_RIGHT (APPEND l1 l2) ==>
    l2 LLEQ_RIGHT l
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_EXISTS\_APPEND member
|- !l1 l2. l1 LLESS_RIGHT l2 ==> (?l. l2 = APPEND l l1)
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_LENGTH1\_NULL member
|- !l1 l2. l2 LLESS_RIGHT l1 /\ (LENGTH l1 = 1) ==> NULL l2
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_NULL member
|- !l1 l2. l1 LLESS_RIGHT l2 ==> ~NULL l2
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_SINGLE\_NULL member
|- !l h. l LLESS_RIGHT [h] = NULL l
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_SNOC member
|- !l1 l2 h.
    (BUTLAST l1) LLESS_RIGHT l2 /\ (h = LAST l1) /\ ~NULL l1 ==>
    l1 LLESS_RIGHT (SNOC h l2)
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_SNOC\_BUTLAST\_LLESS\_RIGHT member
|- !l h t.
    l LLESS_RIGHT (SNOC h t) /\ ~NULL l ==> (BUTLAST l) LLESS_RIGHT t
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_SNOC\_LAST member
|- !l h t. l LLESS_RIGHT (SNOC h t) /\ ~NULL l ==> (h = LAST l)
\ENDTHEOREM
\THEOREM MEMBER member
|- (!x. MEMBER x[] = F) /\
   (!x h t. MEMBER x(CONS h t) = (h = x) \/ MEMBER x t)
\ENDTHEOREM
\THEOREM MEMBER\_SNOC member
|- !t x h. MEMBER x(SNOC h t) = (h = x) \/ MEMBER x t
\ENDTHEOREM
\THEOREM NIL\_LLEQ\_LEFT member
|- !l. [] LLEQ_LEFT l
\ENDTHEOREM
\THEOREM NIL\_LLEQ\_RIGHT member
|- !l. [] LLEQ_RIGHT l
\ENDTHEOREM
\THEOREM NOT\_LLESS\_LEFT\_CONS\_NOT\_NULL member
|- !l h t. ~l LLESS_LEFT (CONS h t) ==> ~NULL l
\ENDTHEOREM
\THEOREM NOT\_LLESS\_LEFT\_CONS\_NOT\_TL\_LLESS\_LEFT member
|- !l h t.
    ~l LLESS_LEFT (CONS h t) /\ ~NULL l /\ (h = HD l) ==>
    ~(TL l) LLESS_LEFT t
\ENDTHEOREM
\THEOREM NOT\_LLESS\_LEFT\_NIL member
|- !l. ~l LLESS_LEFT []
\ENDTHEOREM
\THEOREM NOT\_LLESS\_LEFT\_NOT\_NULL member
|- !l1 l2. ~l1 LLESS_LEFT l2 /\ ~NULL l2 ==> ~NULL l1
\ENDTHEOREM
\THEOREM NOT\_LLESS\_LEFT\_TL member
|- !l1 l2 h.
    ~(CONS h l1) LLESS_LEFT l2 /\ (h = HD l2) /\ ~NULL l2 ==>
    ~l1 LLESS_LEFT (TL l2)
\ENDTHEOREM
\THEOREM NOT\_LLESS\_RIGHT\_BUTLAST member
|- !l1 l2 h.
    ~(SNOC h l1) LLESS_RIGHT l2 /\ (h = LAST l2) /\ ~NULL l2 ==>
    ~l1 LLESS_RIGHT (BUTLAST l2)
\ENDTHEOREM
\THEOREM NOT\_LLESS\_RIGHT\_NIL member
|- !l. ~l LLESS_RIGHT []
\ENDTHEOREM
\THEOREM NOT\_LLESS\_RIGHT\_NOT\_NULL member
|- !l1 l2. ~l1 LLESS_RIGHT l2 /\ ~NULL l2 ==> ~NULL l1
\ENDTHEOREM
\THEOREM NOT\_LLESS\_RIGHT\_SNOC\_NOT\_BUTLAST\_LLESS\_RIGHT member
|- !l h t.
    ~l LLESS_RIGHT (SNOC h t) /\ ~NULL l /\ (h = LAST l) ==>
    ~(BUTLAST l) LLESS_RIGHT t
\ENDTHEOREM
\THEOREM NOT\_LLESS\_RIGHT\_SNOC\_NOT\_NULL member
|- !l h t. ~l LLESS_RIGHT (SNOC h t) ==> ~NULL l
\ENDTHEOREM
\THEOREM NOT\_NIL\_LLESS\_LEFT member
|- !l. ~[] LLESS_LEFT l ==> NULL l
\ENDTHEOREM
\THEOREM NOT\_NIL\_LLESS\_RIGHT member
|- !l. ~[] LLESS_RIGHT l ==> NULL l
\ENDTHEOREM
\THEOREM SNOC\_LLEQ\_RIGHT\_BUTLAST member
|- !l1 l2. (SNOC h l1) LLEQ_RIGHT l2 ==> l1 LLEQ_RIGHT (BUTLAST l2)
\ENDTHEOREM
\THEOREM SNOC\_LLESS\_RIGHT\_APPEND\_LAST member
|- !l l1 l2.
    ~NULL l2 /\ (SNOC h l) LLESS_RIGHT (APPEND l1 l2) ==> (h = LAST l2)
\ENDTHEOREM
\THEOREM SNOC\_LLESS\_RIGHT\_BUTLAST member
|- !l1 l2. (SNOC h l1) LLESS_RIGHT l2 ==> l1 LLESS_RIGHT (BUTLAST l2)
\ENDTHEOREM
\THEOREM SNOC\_LLESS\_RIGHT\_LAST member
|- !h l1 l2. (SNOC h l1) LLESS_RIGHT l2 ==> (h = LAST l2)
\ENDTHEOREM
\section{Theorems about {\tt UNAPPEND}}
\THEOREM APPEND\_UNAPPEND\_LEFT\_ID unappend
|- !l. l = APPEND l(UNAPPEND_LEFT l l)
\ENDTHEOREM
\THEOREM APPEND\_UNAPPEND\_RIGHT\_ID unappend
|- !l. l = APPEND l(UNAPPEND_RIGHT l l)
\ENDTHEOREM
\THEOREM EXISTS\_UNAPPEND\_LEFT unappend
|- ?f. !l1 l2. f l1(APPEND l1 l2) = l2
\ENDTHEOREM
\THEOREM EXISTS\_UNAPPEND\_RIGHT unappend
|- ?f. !l1 l2. f l2(APPEND l1 l2) = l1
\ENDTHEOREM
\THEOREM LLEQ\_LEFT\_APPEND\_UNAPPEND\_LEFT unappend
|- !l1 l2. l1 LLEQ_LEFT l2 ==> (l2 = APPEND l1(UNAPPEND_LEFT l1 l2))
\ENDTHEOREM
\THEOREM LLEQ\_LEFT\_UNAPPEND\_LEFT\_CONS unappend
|- !h l1 l2.
    l1 LLEQ_LEFT l2 ==>
    (UNAPPEND_LEFT(CONS h l1)(CONS h l2) = UNAPPEND_LEFT l1 l2)
\ENDTHEOREM
\THEOREM LLEQ\_RIGHT\_APPEND\_UNAPPEND\_RIGHT unappend
|- !l1 l2. l1 LLEQ_RIGHT l2 ==> (l2 = APPEND(UNAPPEND_RIGHT l1 l2)l1)
\ENDTHEOREM
\THEOREM LLEQ\_RIGHT\_UNAPPEND\_RIGHT\_SNOC unappend
|- !h l1 l2.
    l1 LLEQ_RIGHT l2 ==>
    (UNAPPEND_RIGHT(SNOC h l1)(SNOC h l2) = UNAPPEND_RIGHT l1 l2)
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_APPEND\_UNAPPEND\_LEFT unappend
|- !l1 l2. l1 LLESS_LEFT l2 ==> (l2 = APPEND l1(UNAPPEND_LEFT l1 l2))
\ENDTHEOREM
\THEOREM LLESS\_LEFT\_APPEND\_UNAPPEND\_LEFT\_LLESS\_LEFT unappend
|- !l1 l2 l.
    ~l LLESS_LEFT l1 /\ l LLESS_LEFT (APPEND l1 l2) ==>
    (UNAPPEND_LEFT l1 l) LLESS_LEFT l2
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_APPEND\_UNAPPEND\_RIGHT unappend
|- !l1 l2. l1 LLESS_RIGHT l2 ==> (l2 = APPEND(UNAPPEND_RIGHT l1 l2)l1)
\ENDTHEOREM
\THEOREM LLESS\_RIGHT\_APPEND\_UNAPPEND\_RIGHT\_LLESS\_RIGHT unappend
|- !l1 l2 l.
    ~l LLESS_RIGHT l2 /\ l LLESS_RIGHT (APPEND l1 l2) ==>
    (UNAPPEND_RIGHT l2 l) LLESS_RIGHT l1
\ENDTHEOREM
\THEOREM NULL\_UNAPPEND\_LEFT unappend
|- !l. NULL(UNAPPEND_LEFT l l)
\ENDTHEOREM
\THEOREM NULL\_UNAPPEND\_RIGHT unappend
|- !l. NULL(UNAPPEND_RIGHT l l)
\ENDTHEOREM
\THEOREM UNAPPEND\_LEFT unappend
|- !l1 l2. UNAPPEND_LEFT l1(APPEND l1 l2) = l2
\ENDTHEOREM
\THEOREM UNAPPEND\_LEFT\_CONS unappend
|- !h l1 l2.
    l1 LLESS_LEFT l2 ==>
    (UNAPPEND_LEFT(CONS h l1)(CONS h l2) = UNAPPEND_LEFT l1 l2)
\ENDTHEOREM
\THEOREM UNAPPEND\_LEFT\_EQ\_NIL unappend
|- !l. UNAPPEND_LEFT l l = []
\ENDTHEOREM
\THEOREM UNAPPEND\_LEFT\_NIL unappend
|- !l. UNAPPEND_LEFT[]l = l
\ENDTHEOREM
\THEOREM UNAPPEND\_LEFT\_UNAPPEND\_RIGHT unappend
|- !l1 l2.
    l2 LLESS_RIGHT l1 ==> (UNAPPEND_LEFT(UNAPPEND_RIGHT l2 l1)l1 = l2)
\ENDTHEOREM
\THEOREM UNAPPEND\_RIGHT unappend
|- !l1 l2. UNAPPEND_RIGHT l2(APPEND l1 l2) = l1
\ENDTHEOREM
\THEOREM UNAPPEND\_RIGHT\_EQ\_NIL unappend
|- !l. UNAPPEND_RIGHT l l = []
\ENDTHEOREM
\THEOREM UNAPPEND\_RIGHT\_NIL unappend
|- !l. UNAPPEND_RIGHT[]l = l
\ENDTHEOREM
\THEOREM UNAPPEND\_RIGHT\_SNOC unappend
|- !h l1 l2.
    l1 LLESS_RIGHT l2 ==>
    (UNAPPEND_RIGHT(SNOC h l1)(SNOC h l2) = UNAPPEND_RIGHT l1 l2)
\ENDTHEOREM
\THEOREM UNAPPEND\_RIGHT\_UNAPPEND\_LEFT unappend
|- !l1 l2.
    l2 LLESS_LEFT l1 ==> (UNAPPEND_RIGHT(UNAPPEND_LEFT l2 l1)l1 = l2)
\ENDTHEOREM
\section{Theorems about Shifting and Rotating Lists}
\THEOREM LENGTH\_PAD\_LEFT shift
|- !l n x. LENGTH(PAD_LEFT x n l) = (LENGTH l) + n
\ENDTHEOREM
\THEOREM LENGTH\_PAD\_RIGHT shift
|- !l n x. LENGTH(PAD_RIGHT x n l) = (LENGTH l) + n
\ENDTHEOREM
\THEOREM LENGTH\_ROTATE1\_LEFT shift
|- !l. ~NULL l ==> (LENGTH(ROTATE1_LEFT l) = LENGTH l)
\ENDTHEOREM
\THEOREM LENGTH\_ROTATE1\_RIGHT shift
|- !l. ~NULL l ==> (LENGTH(ROTATE1_RIGHT l) = LENGTH l)
\ENDTHEOREM
\THEOREM PAD\_LEFT shift
|- (!x l. PAD_LEFT x 0 l = l) /\
   (!x n l. PAD_LEFT x(SUC n)l = CONS x(PAD_LEFT x n l))
\ENDTHEOREM
\THEOREM PAD\_RIGHT shift
|- (!x l. PAD_RIGHT x 0 l = l) /\
   (!x n l. PAD_RIGHT x(SUC n)l = SNOC x(PAD_RIGHT x n l))
\ENDTHEOREM
\THEOREM ROTATE1\_LEFT shift
|- !l. ROTATE1_LEFT l = SNOC(HD l)(TL l)
\ENDTHEOREM
\THEOREM ROTATE1\_LEFT\_CONS shift
|- !x l. ROTATE1_LEFT(CONS x l) = SNOC x l
\ENDTHEOREM
\THEOREM ROTATE1\_LEFT\_NIL shift
|- !l. ~NULL l ==> ~NULL(ROTATE1_LEFT l)
\ENDTHEOREM
\THEOREM ROTATE1\_LEFT\_ROTATE1\_RIGHT shift
|- !l. ~NULL l ==> (ROTATE1_LEFT(ROTATE1_RIGHT l) = l)
\ENDTHEOREM
\THEOREM ROTATE1\_RIGHT shift
|- !l. ROTATE1_RIGHT l = CONS(LAST l)(BUTLAST l)
\ENDTHEOREM
\THEOREM ROTATE1\_RIGHT\_NIL shift
|- !l. ~NULL l ==> ~NULL(ROTATE1_RIGHT l)
\ENDTHEOREM
\THEOREM ROTATE1\_RIGHT\_ROTATE1\_LEFT shift
|- !l. ~NULL l ==> (ROTATE1_RIGHT(ROTATE1_LEFT l) = l)
\ENDTHEOREM
\THEOREM ROTATE1\_RIGHT\_SNOC shift
|- !x l. ROTATE1_RIGHT(SNOC x l) = CONS x l
\ENDTHEOREM
\THEOREM ROTATE\_LEFT shift
|- (!l. ROTATE_LEFT 0 l = l) /\
   (!n l. ROTATE_LEFT(SUC n)l = ROTATE1_LEFT(ROTATE_LEFT n l))
\ENDTHEOREM
\THEOREM ROTATE\_LEFT\_EL shift
|- !n x. ROTATE_LEFT n[x] = [x]
\ENDTHEOREM
\THEOREM ROTATE\_LEFT\_ROTATE1\_LEFT shift
|- !l n.
    ~NULL l ==> (ROTATE_LEFT(SUC n)l = ROTATE_LEFT n(ROTATE1_LEFT l))
\ENDTHEOREM
\THEOREM ROTATE\_LEFT\_ROTATE\_RIGHT shift
|- !n l. ~NULL l ==> (ROTATE_LEFT n(ROTATE_RIGHT n l) = l)
\ENDTHEOREM
\THEOREM ROTATE\_LEFT\_SUC\_CONS shift
|- !l x n. ROTATE_LEFT(SUC n)(CONS x l) = ROTATE_LEFT n(SNOC x l)
\ENDTHEOREM
\THEOREM ROTATE\_RIGHT shift
|- (!l. ROTATE_RIGHT 0 l = l) /\
   (!n l. ROTATE_RIGHT(SUC n)l = ROTATE1_RIGHT(ROTATE_RIGHT n l))
\ENDTHEOREM
\THEOREM ROTATE\_RIGHT\_EL shift
|- !n x. ROTATE_RIGHT n[x] = [x]
\ENDTHEOREM
\THEOREM ROTATE\_RIGHT\_ROTATE1\_RIGHT shift
|- !l n.
    ~NULL l ==> (ROTATE_RIGHT(SUC n)l = ROTATE_RIGHT n(ROTATE1_RIGHT l))
\ENDTHEOREM
\THEOREM ROTATE\_RIGHT\_ROTATE\_LEFT shift
|- !n l. ~NULL l ==> (ROTATE_RIGHT n(ROTATE_LEFT n l) = l)
\ENDTHEOREM
\THEOREM ROTATE\_RIGHT\_SUC\_SNOC shift
|- !l x n. ROTATE_RIGHT(SUC n)(SNOC x l) = ROTATE_RIGHT n(CONS x l)
\ENDTHEOREM
\section{Theorems about Pairing Lists}
\THEOREM FST\_SND\_UNZIP\_ZIP zip
|- !l1 l2.
    (LENGTH l1 = LENGTH l2) =
    (UNZIP_FST(ZIP l1 l2) = l1) /\ (UNZIP_SND(ZIP l1 l2) = l2)
\ENDTHEOREM
\THEOREM UNZIP\_FST zip
|- (UNZIP_FST[] = []) /\
   (!h t. UNZIP_FST(CONS h t) = CONS(FST h)(UNZIP_FST t))
\ENDTHEOREM
\THEOREM UNZIP\_FST\_ZIP zip
|- !l1 l2. (LENGTH l1) <= (LENGTH l2) = (UNZIP_FST(ZIP l1 l2) = l1)
\ENDTHEOREM
\THEOREM UNZIP\_SND zip
|- (UNZIP_SND[] = []) /\
   (!h t. UNZIP_SND(CONS h t) = CONS(SND h)(UNZIP_SND t))
\ENDTHEOREM
\THEOREM UNZIP\_SND\_ZIP zip
|- !l1 l2. (LENGTH l2) <= (LENGTH l1) = (UNZIP_SND(ZIP l1 l2) = l2)
\ENDTHEOREM
\THEOREM ZIP zip
|- (ZIP[][] = []) /\
   (!h1 t1. ZIP(CONS h1 t1)[] = []) /\
   (!h2 t2. ZIP[](CONS h2 t2) = []) /\
   (!h1 t1 h2 t2. ZIP(CONS h1 t1)(CONS h2 t2) = CONS(h1,h2)(ZIP t1 t2))
\ENDTHEOREM
\THEOREM ZIP\_CLAUSES zip
|- (!l. ZIP[]l = []) /\
   (!l. ZIP l[] = []) /\
   (!h1 t1 h2 t2. ZIP(CONS h1 t1)(CONS h2 t2) = CONS(h1,h2)(ZIP t1 t2))
\ENDTHEOREM
\THEOREM ZIP\_DEF zip
|- (!l. ZIP l[] = []) /\
   (!l h t. ZIP l(CONS h t) = (NULL l => [] | CONS(HD l,h)(ZIP(TL l)t)))
\ENDTHEOREM
\THEOREM ZIP\_UNZIP\_FST\_SND zip
|- !l. ZIP(UNZIP_FST l)(UNZIP_SND l) = l
\ENDTHEOREM
\section{Theorems about {\tt num} Lists}
\THEOREM EL1\_TL num\_lists
|- !l. ~NULL l ==> (MAP(\n. EL1 n l)(2 UPTO (LENGTH l)) = TL l)
\ENDTHEOREM
\THEOREM EL\_FROM0 num\_lists
|- !n m. m <= n ==> (EL m(FROM0 n) = m)
\ENDTHEOREM
\THEOREM EL\_MAP\_FROM0 num\_lists
|- !f m n. m <= n ==> (EL m(MAP f(FROM0 n)) = f(EL m(FROM0 n)))
\ENDTHEOREM
\THEOREM EVERY\_FROM0 num\_lists
|- !n. EVERY(\m. m <= n)(FROM0 n)
\ENDTHEOREM
\THEOREM EVERY\_UPTO num\_lists
|- !m n. EVERY(\p. m <= p /\ p <= n)(m UPTO n)
\ENDTHEOREM
\THEOREM FROM0 num\_lists
|- (FROM0 0 = [0]) /\ (!n. FROM0(SUC n) = CONS 0(MAP SUC(FROM0 n)))
\ENDTHEOREM
\THEOREM FROM0\_APPEND num\_lists
|- !n. FROM0(SUC n) = APPEND(FROM0 n)[SUC n]
\ENDTHEOREM
\THEOREM FROM0\_PRE num\_lists
|- !n. 0 < n ==> (FROM0 n = CONS 0(MAP SUC(FROM0(PRE n))))
\ENDTHEOREM
\THEOREM FROM0\_SUB num\_lists
|- !m n. m < n ==> (FROM0(n - m) = CONS 0(MAP SUC(FROM0(n - (SUC m)))))
\ENDTHEOREM
\THEOREM INTERVAL num\_lists
|- (!m. m UPTO 0 = (m > 0 => [] | [0])) /\
   (!m n. m UPTO (SUC n) = (m > (SUC n) => [] | SNOC(SUC n)(m UPTO n)))
\ENDTHEOREM
\THEOREM LENGTH\_FROM0 num\_lists
|- !n. LENGTH(FROM0 n) = SUC n
\ENDTHEOREM
\THEOREM NOT\_NULL\_FROM0 num\_lists
|- !n. ~NULL(FROM0 n)
\ENDTHEOREM
\THEOREM RANGE num\_lists
|- (!m. RANGE m 0 = []) /\
   (!m n. RANGE m(SUC n) = CONS m(RANGE(SUC m)n))
\ENDTHEOREM
\THEOREM RANGE\_SHIFT num\_lists
|- !n m. RANGE(SUC m)n = MAP SUC(RANGE m n)
\ENDTHEOREM
\THEOREM RANGE\_TOP num\_lists
|- !n m. RANGE m(SUC n) = APPEND(RANGE m n)[m + n]
\ENDTHEOREM
\THEOREM SUC\_UPTO\_SUC num\_lists
|- !m n. (SUC m) UPTO (SUC n) = MAP SUC(m UPTO n)
\ENDTHEOREM
\THEOREM UPTO num\_lists
|- !n1 n2. n1 UPTO n2 = MAP($+ n1)(n1 <= n2 => FROM0(n2 - n1) | [])
\ENDTHEOREM
\THEOREM UPTO\_EQ\_CONS\_SUC\_UPTO num\_lists
|- !m n. m <= n ==> (m UPTO n = CONS m((SUC m) UPTO n))
\ENDTHEOREM
\THEOREM UPTO\_SUC\_EQ\_APPEND\_UPTO num\_lists
|- !m n. m <= (SUC n) ==> (m UPTO (SUC n) = APPEND(m UPTO n)[SUC n])
\ENDTHEOREM
