hol88 (2.02.19940316-13.1) Manual/Reference/theorems.tex

Summary

 Manual/Reference/theorems.tex |  515 ++++++++++++++++++++----------------------
 1 file changed, 250 insertions(+), 265 deletions(-)

    
download this patch

Patch contents

--- hol88-2.02.19940316.orig/Manual/Reference/theorems.tex
+++ hol88-2.02.19940316/Manual/Reference/theorems.tex
@@ -1,7 +1,4 @@
-\chapter{Pre-proved Theorems}
-\input{theorems-intro}
-\section{Definitions of Basic Logical Constants}
-\THEOREM AND\_DEF bool
+\chapter{Pre-proved Theorems}\input{theorems-intro}\section{Definitions of Basic Logical Constants}\THEOREM AND\_DEF bool
 |- $/\ = (\t1 t2. !t. (t1 ==> t2 ==> t) ==> t)
 \ENDTHEOREM
 \THEOREM EXISTS\_DEF bool
@@ -10,12 +7,12 @@
 \THEOREM EXISTS\_UNIQUE\_DEF bool
 |- $?! = (\P. $? P /\ (!x y. P x /\ P y ==> (x = y)))
 \ENDTHEOREM
-\THEOREM FORALL\_DEF bool
-|- $! = (\P. P = (\x. T))
-\ENDTHEOREM
 \THEOREM F\_DEF bool
 |- F = (!t. t)
 \ENDTHEOREM
+\THEOREM FORALL\_DEF bool
+|- $! = (\P. P = (\x. T))
+\ENDTHEOREM
 \THEOREM NOT\_DEF bool
 |- $~ = (\t. t ==> F)
 \ENDTHEOREM
@@ -25,8 +22,7 @@
 \THEOREM T\_DEF bool
 |- T = ((\x. x) = (\x. x))
 \ENDTHEOREM
-\section{Constants for syntactic abbreviations}
-\THEOREM ARB bool
+\section{Constants for syntactic abbreviations}\THEOREM ARB bool
 |- ARB = (@x. T)
 \ENDTHEOREM
 \THEOREM COND\_DEF bool
@@ -49,8 +45,7 @@
 \THEOREM RES\_SELECT bool
 |- !P B. RES_SELECT P B = (@x. P x /\ B x)
 \ENDTHEOREM
-\section{Axioms}
-\THEOREM ARB\_THM bool
+\section{Axioms}\THEOREM ARB\_THM bool
 |- $= = $=
 \ENDTHEOREM
 \THEOREM BOOL\_CASES\_AX bool
@@ -68,8 +63,7 @@
 \THEOREM SELECT\_AX bool
 |- !P x. P x ==> P($@ P)
 \ENDTHEOREM
-\section{Logical tautologies}
-\THEOREM AND1\_THM {\none}
+\section{Logical tautologies}\THEOREM AND1\_THM {\none}
 |- !t1 t2. t1 /\ t2 ==> t1 
 \ENDTHEOREM
 \THEOREM AND2\_THM {\none}
@@ -171,13 +165,13 @@
 \THEOREM FALSITY {\none}
 |- !t. F ==> t
 \ENDTHEOREM
+\THEOREM F\_IMP {\none}
+|- !t. ~t ==>(t ==> F)
+\ENDTHEOREM
 \THEOREM FORALL\_SIMP {\none}
 |- !t. (!x. t) = t
 \ENDTHEOREM
 
-\THEOREM F\_IMP {\none}
-|- !t. ~t ==>(t ==> F)
-\ENDTHEOREM
 \THEOREM IMP\_CLAUSES {\none}
 |- !t. (T ==> t) = t /\
        (t ==> T) = T /\
@@ -258,8 +252,7 @@
 \THEOREM TRUTH {\none}
 |- T
 \ENDTHEOREM
-\section{Theorems about functions}
-\THEOREM ABS\_SIMP {\none}
+\section{Theorems about functions}\THEOREM ABS\_SIMP {\none}
 |- !t1 t2. (\x. t1)t2 = t1
 \ENDTHEOREM
 
@@ -309,24 +302,22 @@
 \THEOREM RIGHT\_ID\_DEF fun
 |- !f e. RIGHT_ID f e = (!x. f x e = x)
 \ENDTHEOREM
-\section{Theorems about the type {\tt one}}
-\THEOREM one one
-|- !v. v = one
+\section{Theorems about the type {\tt one}}\THEOREM one\_axiom one
+|- !f g. f = g
 \ENDTHEOREM
 \THEOREM one\_Axiom one
 |- !e. ?! fn. fn one = e
 \ENDTHEOREM
-\THEOREM one\_axiom one
-|- !f g. f = g
-\ENDTHEOREM
 \THEOREM one\_DEF one
 |- one = (@x. T)
 \ENDTHEOREM
+\THEOREM one one
+|- !v. v = one
+\ENDTHEOREM
 \THEOREM one\_TY\_DEF one
 |- ?rep. TYPE_DEFINITION(\b. b)rep
 \ENDTHEOREM
-\section{Theorems about combinators}
-\THEOREM I\_DEF combin
+\section{Theorems about combinators}\THEOREM I\_DEF combin
 |- I = S K K
 \ENDTHEOREM
 \THEOREM I\_o\_ID combin
@@ -356,19 +347,18 @@
 \THEOREM S\_THM combin
 |- !f g x. S f g x = f x(g x)
 \ENDTHEOREM
-\section{Theorems about pairs}
-\THEOREM COMMA\_DEF bool
+\section{Theorems about pairs}\THEOREM COMMA\_DEF bool
 |- !x y. x,y = (@p. REP_prod p = MK_PAIR x y)
 \ENDTHEOREM
 \THEOREM CURRY\_DEF bool
 |- !f x y. CURRY f x y = f(x,y)
 \ENDTHEOREM
-\THEOREM FST bool
-|- !x y. FST(x,y) = x
-\ENDTHEOREM
 \THEOREM FST\_DEF bool
 |- !p. FST p = (@x. ?y. MK_PAIR x y = REP_prod p)
 \ENDTHEOREM
+\THEOREM FST bool
+|- !x y. FST(x,y) = x
+\ENDTHEOREM
 \THEOREM IS\_PAIR\_DEF bool
 |- !p. IS_PAIR p = (?x y. p = MK_PAIR x y)
 \ENDTHEOREM
@@ -390,28 +380,27 @@
      (!p' p''. (rep p' = rep p'') ==> (p' = p'')) /\
      (!p. IS_PAIR p = (?p'. p = rep p')))
 \ENDTHEOREM
-\THEOREM SND bool
-|- !x y. SND(x,y) = y
-\ENDTHEOREM
 \THEOREM SND\_DEF bool
 |- !p. SND p = (@y. ?x. MK_PAIR x y = REP_prod p)
 \ENDTHEOREM
+\THEOREM SND bool
+|- !x y. SND(x,y) = y
+\ENDTHEOREM
 \THEOREM UNCURRY\_DEF bool
 |- !f x y. UNCURRY f(x,y) = f x y
 \ENDTHEOREM
-\section{Theorems about disjoint sums}
+\section{Theorems about disjoint sums}\THEOREM INL\_DEF sum
+|- !e. INL e = ABS_sum(\b x y. (x = e) /\ b)
+\ENDTHEOREM
 \THEOREM INL sum
 |- !x. ISL x ==> (INL(OUTL x) = x)
 \ENDTHEOREM
-\THEOREM INL\_DEF sum
-|- !e. INL e = ABS_sum(\b x y. (x = e) /\ b)
+\THEOREM INR\_DEF sum
+|- !e. INR e = ABS_sum(\b x y. (y = e) /\ ~b)
 \ENDTHEOREM
 \THEOREM INR sum
 |- !x. ISR x ==> (INR(OUTR x) = x)
 \ENDTHEOREM
-\THEOREM INR\_DEF sum
-|- !e. INR e = ABS_sum(\b x y. (y = e) /\ ~b)
-\ENDTHEOREM
 \THEOREM ISL sum
 |- (!x. ISL(INL x)) /\ (!y. ~ISL(INR y))
 \ENDTHEOREM
@@ -433,12 +422,12 @@
 \THEOREM OUTR sum
 |- !x. OUTR(INR x) = x
 \ENDTHEOREM
-\THEOREM sum\_Axiom sum
-|- !f g. ?! h. (!x. h(INL x) = f x) /\ (!x. h(INR x) = g x)
-\ENDTHEOREM
 \THEOREM sum\_axiom sum
 |- !f g. ?! h. (h o INL = f) /\ (h o INR = g)
 \ENDTHEOREM
+\THEOREM sum\_Axiom sum
+|- !f g. ?! h. (!x. h(INL x) = f x) /\ (!x. h(INR x) = g x)
+\ENDTHEOREM
 \THEOREM sum\_ISO\_DEF sum
 |- (!a. ABS_sum(REP_sum a) = a) /\
    (!r. IS_SUM_REP r = (REP_sum(ABS_sum r) = r))
@@ -446,16 +435,12 @@
 \THEOREM sum\_TY\_DEF sum
 |- ?rep. TYPE_DEFINITION IS_SUM_REP rep
 \ENDTHEOREM
-\section{Theorems about arithmetic}
-\THEOREM ADD arithmetic
-|- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
+\section{Theorems about arithmetic}\THEOREM ADD\_0 arithmetic
+|- !m. m + 0 = m
 \ENDTHEOREM
 \THEOREM ADD1 arithmetic
 |- !m. SUC m = m + 1
 \ENDTHEOREM
-\THEOREM ADD\_0 arithmetic
-|- !m. m + 0 = m
-\ENDTHEOREM
 \THEOREM ADD\_ASSOC arithmetic
 |- !m n p. m + (n + p) = (m + n) + p
 \ENDTHEOREM
@@ -465,6 +450,9 @@
    ((SUC m) + n = SUC(m + n)) /\
    (m + (SUC n) = SUC(m + n))
 \ENDTHEOREM
+\THEOREM ADD arithmetic
+|- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
+\ENDTHEOREM
 \THEOREM ADD\_EQ\_0 arithmetic
 |- !m n. (m + n = 0) = (m = 0) /\ (n = 0)
 \ENDTHEOREM
@@ -523,15 +511,15 @@
 \THEOREM EQ\_MONO\_ADD\_EQ arithmetic
 |- !m n p. (m + p = n + p) = (m = n)
 \ENDTHEOREM
-\THEOREM EVEN arithmetic
-|- (EVEN 0 = T) /\ (!n. EVEN(SUC n) = ~EVEN n)
-\ENDTHEOREM
 \THEOREM EVEN\_ADD arithmetic
 |- !m n. EVEN(m + n) = (EVEN m = EVEN n)
 \ENDTHEOREM
 \THEOREM EVEN\_AND\_ODD arithmetic
 |- !n. ~(EVEN n /\ ODD n)
 \ENDTHEOREM
+\THEOREM EVEN arithmetic
+|- (EVEN 0 = T) /\ (!n. EVEN(SUC n) = ~EVEN n)
+\ENDTHEOREM
 \THEOREM EVEN\_DOUBLE arithmetic
 |- !n. EVEN(2 * n)
 \ENDTHEOREM
@@ -550,12 +538,12 @@
 \THEOREM EVEN\_OR\_ODD arithmetic
 |- !n. EVEN n \/ ODD n
 \ENDTHEOREM
-\THEOREM EXP arithmetic
-|- (!m. m EXP 0 = 1) /\ (!m n. m EXP (SUC n) = m * (m EXP n))
-\ENDTHEOREM
 \THEOREM EXP\_ADD arithmetic
 |- !p q n. n EXP (p + q) = (n EXP p) * (n EXP q)
 \ENDTHEOREM
+\THEOREM EXP arithmetic
+|- (!m. m EXP 0 = 1) /\ (!m n. m EXP (SUC n) = m * (m EXP n))
+\ENDTHEOREM
 \THEOREM FACT arithmetic
 |- (FACT 0 = 1) /\ (!n. FACT(SUC n) = (SUC n) * (FACT n))
 \ENDTHEOREM
@@ -609,24 +597,21 @@
 \THEOREM LEFT\_SUB\_DISTRIB arithmetic
 |- !m n p. p * (m - n) = (p * m) - (p * n)
 \ENDTHEOREM
-\THEOREM LESS prim\_rec
-|- !m n. m < n = (?P. (!n'. P(SUC n') ==> P n') /\ P m /\ ~P n)
-\ENDTHEOREM
-\THEOREM LESS\_0 prim\_rec
-|- !n. 0 < (SUC n)
-\ENDTHEOREM
 \THEOREM LESS\_0\_0 prim\_rec
 |- 0 < (SUC 0)
 \ENDTHEOREM
 \THEOREM LESS\_0\_CASES arithmetic
 |- !m. (0 = m) \/ 0 < m
 \ENDTHEOREM
-\THEOREM LESS\_ADD arithmetic
-|- !m n. n < m ==> (?p. p + n = m)
+\THEOREM LESS\_0 prim\_rec
+|- !n. 0 < (SUC n)
 \ENDTHEOREM
 \THEOREM LESS\_ADD\_1 arithmetic
 |- !m n. n < m ==> (?p. m = n + (p + 1))
 \ENDTHEOREM
+\THEOREM LESS\_ADD arithmetic
+|- !m n. n < m ==> (?p. p + n = m)
+\ENDTHEOREM
 \THEOREM LESS\_ADD\_NONZERO arithmetic
 |- !m n. ~(n = 0) ==> m < (m + n)
 \ENDTHEOREM
@@ -642,14 +627,8 @@
 \THEOREM LESS\_CASES\_IMP arithmetic
 |- !m n. ~m < n /\ ~(m = n) ==> n < m
 \ENDTHEOREM
-\THEOREM LESS\_EQ arithmetic
-|- !m n. m < n = (SUC m) <= n
-\ENDTHEOREM
-\THEOREM LESS\_EQUAL\_ADD arithmetic
-|- !m n. m <= n ==> (?p. n = m + p)
-\ENDTHEOREM
-\THEOREM LESS\_EQUAL\_ANTISYM arithmetic
-|- !n m. n <= m /\ m <= n ==> (n = m)
+\THEOREM LESS prim\_rec
+|- !m n. m < n = (?P. (!n'. P(SUC n') ==> P n') /\ P m /\ ~P n)
 \ENDTHEOREM
 \THEOREM LESS\_EQ\_0 arithmetic
 |- !n. n <= 0 = (n = 0)
@@ -666,6 +645,9 @@
 \THEOREM LESS\_EQ\_CASES arithmetic
 |- !m n. m <= n \/ n <= m
 \ENDTHEOREM
+\THEOREM LESS\_EQ arithmetic
+|- !m n. m < n = (SUC m) <= n
+\ENDTHEOREM
 \THEOREM LESS\_EQ\_EXISTS arithmetic
 |- !m n. m <= n = (?p. n = m + p)
 \ENDTHEOREM
@@ -678,12 +660,12 @@
 \THEOREM LESS\_EQ\_LESS\_TRANS arithmetic
 |- !m n p. m <= n /\ n < p ==> m < p
 \ENDTHEOREM
-\THEOREM LESS\_EQ\_MONO arithmetic
-|- !n m. (SUC n) <= (SUC m) = n <= m
-\ENDTHEOREM
 \THEOREM LESS\_EQ\_MONO\_ADD\_EQ arithmetic
 |- !m n p. (m + p) <= (n + p) = m <= n
 \ENDTHEOREM
+\THEOREM LESS\_EQ\_MONO arithmetic
+|- !n m. (SUC n) <= (SUC m) = n <= m
+\ENDTHEOREM
 \THEOREM LESS\_EQ\_REFL arithmetic
 |- !m. m <= m
 \ENDTHEOREM
@@ -696,6 +678,12 @@
 \THEOREM LESS\_EQ\_TRANS arithmetic
 |- !m n p. m <= n /\ n <= p ==> m <= p
 \ENDTHEOREM
+\THEOREM LESS\_EQUAL\_ADD arithmetic
+|- !m n. m <= n ==> (?p. n = m + p)
+\ENDTHEOREM
+\THEOREM LESS\_EQUAL\_ANTISYM arithmetic
+|- !n m. n <= m /\ m <= n ==> (n = m)
+\ENDTHEOREM
 \THEOREM LESS\_EXP\_SUC\_MONO arithmetic
 |- !n m. ((SUC(SUC m)) EXP n) < ((SUC(SUC m)) EXP (SUC n))
 \ENDTHEOREM
@@ -723,9 +711,6 @@
 \THEOREM LESS\_MOD arithmetic
 |- !n k. k < n ==> (k MOD n = k)
 \ENDTHEOREM
-\THEOREM LESS\_MONO prim\_rec
-|- !m n. m < n ==> (SUC m) < (SUC n)
-\ENDTHEOREM
 \THEOREM LESS\_MONO\_ADD arithmetic
 |- !m n p. m < n ==> (m + p) < (n + p)
 \ENDTHEOREM
@@ -735,6 +720,9 @@
 \THEOREM LESS\_MONO\_ADD\_INV arithmetic
 |- !m n p. (m + p) < (n + p) ==> m < n
 \ENDTHEOREM
+\THEOREM LESS\_MONO prim\_rec
+|- !m n. m < n ==> (SUC m) < (SUC n)
+\ENDTHEOREM
 \THEOREM LESS\_MONO\_EQ arithmetic
 |- !m n. (SUC m) < (SUC n) = m < n
 \ENDTHEOREM
@@ -759,12 +747,12 @@
 \THEOREM LESS\_OR arithmetic
 |- !m n. m < n ==> (SUC m) <= n
 \ENDTHEOREM
-\THEOREM LESS\_OR\_EQ arithmetic
-|- !m n. m <= n = m < n \/ (m = n)
-\ENDTHEOREM
 \THEOREM LESS\_OR\_EQ\_ADD arithmetic
 |- !n m. n < m \/ (?p. n = p + m)
 \ENDTHEOREM
+\THEOREM LESS\_OR\_EQ arithmetic
+|- !m n. m <= n = m < n \/ (m = n)
+\ENDTHEOREM
 \THEOREM LESS\_REFL prim\_rec
 |- !n. ~n < n
 \ENDTHEOREM
@@ -822,9 +810,6 @@
 \THEOREM MONOID\_MULT\_1 arithmetic
 |- MONOID $* 1
 \ENDTHEOREM
-\THEOREM MULT arithmetic
-|- (!n. 0 * n = 0) /\ (!m n. (SUC m) * n = (m * n) + n)
-\ENDTHEOREM
 \THEOREM MULT\_0 arithmetic
 |- !m. m * 0 = 0
 \ENDTHEOREM
@@ -840,6 +825,9 @@
     ((SUC m) * n = (m * n) + n) /\
     (m * (SUC n) = m + (m * n))
 \ENDTHEOREM
+\THEOREM MULT arithmetic
+|- (!n. 0 * n = 0) /\ (!m n. (SUC m) * n = (m * n) + n)
+\ENDTHEOREM
 \THEOREM MULT\_EQ\_0 arithmetic
 |- !m n. (m * n = 0) = (m = 0) \/ (n = 0)
 \ENDTHEOREM
@@ -879,12 +867,12 @@
 \THEOREM NOT\_LEQ arithmetic
 |- !m n. ~m <= n = (SUC n) <= m
 \ENDTHEOREM
-\THEOREM NOT\_LESS arithmetic
-|- !m n. ~m < n = n <= m
-\ENDTHEOREM
 \THEOREM NOT\_LESS\_0 prim\_rec
 |- !n. ~n < 0
 \ENDTHEOREM
+\THEOREM NOT\_LESS arithmetic
+|- !m n. ~m < n = n <= m
+\ENDTHEOREM
 \THEOREM NOT\_LESS\_EQ prim\_rec
 |- !m n. (m = n) ==> ~m < n
 \ENDTHEOREM
@@ -897,18 +885,18 @@
 \THEOREM NOT\_ODD\_EQ\_EVEN arithmetic
 |- !n m. ~(SUC(n + n) = m + m)
 \ENDTHEOREM
-\THEOREM NOT\_SUC num
-|- !n. ~(SUC n = 0)
-\ENDTHEOREM
 \THEOREM NOT\_SUC\_ADD\_LESS\_EQ arithmetic
 |- !m n. ~(SUC(m + n)) <= m
 \ENDTHEOREM
-\THEOREM NOT\_SUC\_LESS\_EQ arithmetic
-|- !n m. ~(SUC n) <= m = m <= n
+\THEOREM NOT\_SUC num
+|- !n. ~(SUC n = 0)
 \ENDTHEOREM
 \THEOREM NOT\_SUC\_LESS\_EQ\_0 arithmetic
 |- !n. ~(SUC n) <= 0
 \ENDTHEOREM
+\THEOREM NOT\_SUC\_LESS\_EQ arithmetic
+|- !n m. ~(SUC n) <= m = m <= n
+\ENDTHEOREM
 \THEOREM num\_Axiom prim\_rec
 |- !e f. ?! fn. (fn 0 = e) /\ (!n. fn(SUC n) = f(fn n)n)
 \ENDTHEOREM
@@ -922,12 +910,12 @@
 \THEOREM num\_TY\_DEF num
 |- ?rep. TYPE_DEFINITION IS_NUM_REP rep
 \ENDTHEOREM
-\THEOREM ODD arithmetic
-|- (ODD 0 = F) /\ (!n. ODD(SUC n) = ~ODD n)
-\ENDTHEOREM
 \THEOREM ODD\_ADD arithmetic
 |- !m n. ODD(m + n) = ~(ODD m = ODD n)
 \ENDTHEOREM
+\THEOREM ODD arithmetic
+|- (ODD 0 = F) /\ (!n. ODD(SUC n) = ~ODD n)
+\ENDTHEOREM
 \THEOREM ODD\_DOUBLE arithmetic
 |- !n. ODD(SUC(2 * n))
 \ENDTHEOREM
@@ -946,18 +934,18 @@
 \THEOREM OR\_LESS arithmetic
 |- !m n. (SUC m) <= n ==> m < n
 \ENDTHEOREM
-\THEOREM PRE prim\_rec
-|- (PRE 0 = 0) /\ (!m. PRE(SUC m) = m)
-\ENDTHEOREM
 \THEOREM PRE\_DEF prim\_rec
 |- !m. PRE m = ((m = 0) => 0 | (@n. m = SUC n))
 \ENDTHEOREM
-\THEOREM PRE\_SUB arithmetic
-|- !m n. PRE(m - n) = (PRE m) - n
+\THEOREM PRE prim\_rec
+|- (PRE 0 = 0) /\ (!m. PRE(SUC m) = m)
 \ENDTHEOREM
 \THEOREM PRE\_SUB1 arithmetic
 |- !m. PRE m = m - 1
 \ENDTHEOREM
+\THEOREM PRE\_SUB arithmetic
+|- !m n. PRE(m - n) = (PRE m) - n
+\ENDTHEOREM
 \THEOREM PRE\_SUC\_EQ arithmetic
 |- !m n. 0 < n ==> ((m = PRE n) = (SUC m = n))
 \ENDTHEOREM
@@ -1013,9 +1001,6 @@
     (SIMP_REC x f 0 = x) /\
     (!m. SIMP_REC x f(SUC m) = f(SIMP_REC x f m))
 \ENDTHEOREM
-\THEOREM SUB arithmetic
-|- (!m. 0 - m = 0) /\ (!m n. (SUC m) - n = (m < n => 0 | SUC(m - n)))
-\ENDTHEOREM
 \THEOREM SUB\_0 arithmetic
 |- !m. (0 - m = 0) /\ (m - 0 = m)
 \ENDTHEOREM
@@ -1025,8 +1010,8 @@
 \THEOREM SUB\_CANCEL arithmetic
 |- !p n m. n <= p /\ m <= p ==> ((p - n = p - m) = (n = m))
 \ENDTHEOREM
-\THEOREM SUB\_EQUAL\_0 arithmetic
-|- !c. c - c = 0
+\THEOREM SUB arithmetic
+|- (!m. 0 - m = 0) /\ (!m n. (SUC m) - n = (m < n => 0 | SUC(m - n)))
 \ENDTHEOREM
 \THEOREM SUB\_EQ\_0 arithmetic
 |- !m n. (m - n = 0) = m <= n
@@ -1034,6 +1019,9 @@
 \THEOREM SUB\_EQ\_EQ\_0 arithmetic
 |- !m n. (m - n = m) = (m = 0) \/ (n = 0)
 \ENDTHEOREM
+\THEOREM SUB\_EQUAL\_0 arithmetic
+|- !c. c - c = 0
+\ENDTHEOREM
 \THEOREM SUB\_LEFT\_ADD arithmetic
 |- !m n p. m + (n - p) = (n <= p => m | (m + n) - p)
 \ENDTHEOREM
@@ -1061,12 +1049,12 @@
 \THEOREM SUB\_LESS\_0 arithmetic
 |- !n m. m < n = 0 < (n - m)
 \ENDTHEOREM
-\THEOREM SUB\_LESS\_EQ arithmetic
-|- !n m. (n - m) <= n
-\ENDTHEOREM
 \THEOREM SUB\_LESS\_EQ\_ADD arithmetic
 |- !m p. m <= p ==> (!n. (p - m) <= n = p <= (m + n))
 \ENDTHEOREM
+\THEOREM SUB\_LESS\_EQ arithmetic
+|- !n m. (n - m) <= n
+\ENDTHEOREM
 \THEOREM SUB\_LESS\_OR arithmetic
 |- !m n. n < m ==> n <= (m - 1)
 \ENDTHEOREM
@@ -1148,12 +1136,7 @@
 \THEOREM ZERO\_REP\_DEF num
 |- ZERO_REP = (@x. !y. ~(x = SUC_REP y))
 \ENDTHEOREM
-\section{Theorems about lists}
-\THEOREM ALL\_EL list
-|- (!P. ALL_EL P[] = T) /\
-   (!P x l. ALL_EL P(CONS x l) = P x /\ ALL_EL P l)
-\ENDTHEOREM
-\THEOREM ALL\_EL\_APPEND list
+\section{Theorems about lists}\THEOREM ALL\_EL\_APPEND list
 |- !P l1 l2. ALL_EL P(APPEND l1 l2) = ALL_EL P l1 /\ ALL_EL P l2
 \ENDTHEOREM
 \THEOREM ALL\_EL\_BUTFIRSTN list
@@ -1166,6 +1149,10 @@
 \THEOREM ALL\_EL\_CONJ list
 |- !P Q l. ALL_EL(\x. P x /\ Q x)l = ALL_EL P l /\ ALL_EL Q l
 \ENDTHEOREM
+\THEOREM ALL\_EL list
+|- (!P. ALL_EL P[] = T) /\
+   (!P x l. ALL_EL P(CONS x l) = P x /\ ALL_EL P l)
+\ENDTHEOREM
 \THEOREM ALL\_EL\_FIRSTN list
 |- !P l. ALL_EL P l ==> (!m. m <= (LENGTH l) ==> ALL_EL P(FIRSTN m l))
 \ENDTHEOREM
@@ -1214,13 +1201,12 @@
    (!h t l. AP(CONS h t)l = CONS(h(HD l))(AP t(TL l)))
 \ENDTHEOREM
 
-\THEOREM APPEND list
-|- (!l. APPEND[]l = l) /\
-   (!l1 l2 h. APPEND(CONS h l1)l2 = CONS h(APPEND l1 l2))
-\ENDTHEOREM
 \THEOREM APPEND\_ASSOC list
 |- !l1 l2 l3. APPEND l1(APPEND l2 l3) = APPEND(APPEND l1 l2)l3
 \ENDTHEOREM
+\THEOREM APPEND\_BUTLAST\_LAST list
+|- !l. ~(l = []) ==> (APPEND(BUTLAST l)[LAST l] = l)
+\ENDTHEOREM
 \THEOREM APPEND\_BUTLASTN\_BUTFIRSTN list
 |- !m n l.
     (m + n = LENGTH l) ==> (APPEND(BUTLASTN m l)(BUTFIRSTN n l) = l)
@@ -1228,8 +1214,9 @@
 \THEOREM APPEND\_BUTLASTN\_LASTN list
 |- !n l. n <= (LENGTH l) ==> (APPEND(BUTLASTN n l)(LASTN n l) = l)
 \ENDTHEOREM
-\THEOREM APPEND\_BUTLAST\_LAST list
-|- !l. ~(l = []) ==> (APPEND(BUTLAST l)[LAST l] = l)
+\THEOREM APPEND list
+|- (!l. APPEND[]l = l) /\
+   (!l1 l2 h. APPEND(CONS h l1)l2 = CONS h(APPEND l1 l2))
 \ENDTHEOREM
 \THEOREM APPEND\_FIRSTN\_BUTFIRSTN list
 |- !n l. n <= (LENGTH l) ==> (APPEND(FIRSTN n l)(BUTFIRSTN n l) = l)
@@ -1273,10 +1260,6 @@
       LEFT_ID f e ==>
       (!l. FOLDR f e(FLAT l) = FOLDR f e(MAP(FOLDR f e)l)))
 \ENDTHEOREM
-\THEOREM BUTFIRSTN list
-|- (!l. BUTFIRSTN 0 l = l) /\
-   (!n x l. BUTFIRSTN(SUC n)(CONS x l) = BUTFIRSTN n l)
-\ENDTHEOREM
 \THEOREM BUTFIRSTN\_APPEND1 list
 |- !n l1.
     n <= (LENGTH l1) ==>
@@ -1292,6 +1275,10 @@
     (n + m) <= (LENGTH l) ==>
     (BUTFIRSTN n(BUTFIRSTN m l) = BUTFIRSTN(n + m)l)
 \ENDTHEOREM
+\THEOREM BUTFIRSTN list
+|- (!l. BUTFIRSTN 0 l = l) /\
+   (!n x l. BUTFIRSTN(SUC n)(CONS x l) = BUTFIRSTN n l)
+\ENDTHEOREM
 \THEOREM BUTFIRSTN\_LASTN list
 |- !n l. n <= (LENGTH l) ==> (BUTFIRSTN n l = LASTN((LENGTH l) - n)l)
 \ENDTHEOREM
@@ -1313,13 +1300,12 @@
     n <= (LENGTH l) ==>
     (!x. BUTFIRSTN n(SNOC x l) = SNOC x(BUTFIRSTN n l))
 \ENDTHEOREM
+\THEOREM BUTLAST\_DEF list
+|- !l. BUTLAST l = SEG(PRE(LENGTH l))0 l
+\ENDTHEOREM
 \THEOREM BUTLAST list
 |- !x l. BUTLAST(SNOC x l) = l
 \ENDTHEOREM
-\THEOREM BUTLASTN list
-|- (!l. BUTLASTN 0 l = l) /\
-   (!n x l. BUTLASTN(SUC n)(SNOC x l) = BUTLASTN n l)
-\ENDTHEOREM
 \THEOREM BUTLASTN\_1 list
 |- !l. ~(l = []) ==> (BUTLASTN 1 l = BUTLAST l)
 \ENDTHEOREM
@@ -1347,6 +1333,10 @@
     n <= (LENGTH l) ==>
     (!x. BUTLASTN n(CONS x l) = CONS x(BUTLASTN n l))
 \ENDTHEOREM
+\THEOREM BUTLASTN list
+|- (!l. BUTLASTN 0 l = l) /\
+   (!n x l. BUTLASTN(SUC n)(SNOC x l) = BUTLASTN n l)
+\ENDTHEOREM
 \THEOREM BUTLASTN\_FIRSTN list
 |- !n l. n <= (LENGTH l) ==> (BUTLASTN n l = FIRSTN((LENGTH l) - n)l)
 \ENDTHEOREM
@@ -1381,9 +1371,6 @@
 \THEOREM BUTLASTN\_SUC\_BUTLAST list
 |- !n l. n < (LENGTH l) ==> (BUTLASTN(SUC n)l = BUTLASTN n(BUTLAST l))
 \ENDTHEOREM
-\THEOREM BUTLAST\_DEF list
-|- !l. BUTLAST l = SEG(PRE(LENGTH l))0 l
-\ENDTHEOREM
 \THEOREM COMM\_ASSOC\_FOLDL\_REVERSE list
 |- !f. COMM f ==> ASSOC f ==> (!e l. FOLDL f e(REVERSE l) = FOLDL f e l)
 \ENDTHEOREM
@@ -1400,9 +1387,6 @@
     COMM f ==>
     (!e'. MONOID f e' ==> (!e l. FOLDR f e l = f e(FOLDR f e' l)))
 \ENDTHEOREM
-\THEOREM CONS list
-|- !l. ~NULL l ==> (CONS(HD l)(TL l) = l)
-\ENDTHEOREM
 \THEOREM CONS\_11 list
 |- !h t h' t'. (CONS h t = CONS h' t') = (h = h') /\ (t = t')
 \ENDTHEOREM
@@ -1415,11 +1399,28 @@
     ABS_list
     ((\m. ((m = 0) => h | FST(REP_list t)(PRE m))),SUC(SND(REP_list t)))
 \ENDTHEOREM
+\THEOREM CONS list
+|- !l. ~NULL l ==> (CONS(HD l)(TL l) = l)
+\ENDTHEOREM
+\THEOREM EL\_APPEND1 list
+|- !n l1 l2. n < (LENGTH l1) ==> (EL n(APPEND l1 l2) = EL n l1)
+\ENDTHEOREM
+\THEOREM EL\_APPEND2 list
+|- !l1 n.
+    (LENGTH l1) <= n ==>
+    (!l2. EL n(APPEND l1 l2) = EL(n - (LENGTH l1))l2)
+\ENDTHEOREM
+\THEOREM EL\_CONS list
+|- !n. 0 < n ==> (!x l. EL n(CONS x l) = EL(PRE n)l)
+\ENDTHEOREM
 \THEOREM EL list
 |- (!l. EL 0 l = HD l) /\ (!l n. EL(SUC n)l = EL n(TL l))
 \ENDTHEOREM
-\THEOREM ELL list
-|- (!l. ELL 0 l = LAST l) /\ (!n l. ELL(SUC n)l = ELL n(BUTLAST l))
+\THEOREM EL\_ELL list
+|- !n l. n < (LENGTH l) ==> (EL n l = ELL(PRE((LENGTH l) - n))l)
+\ENDTHEOREM
+\THEOREM EL\_IS\_EL list
+|- !n l. n < (LENGTH l) ==> IS_EL(EL n l)l
 \ENDTHEOREM
 \THEOREM ELL\_0\_SNOC list
 |- !l x. ELL 0(SNOC x l) = x
@@ -1435,9 +1436,18 @@
 \THEOREM ELL\_CONS list
 |- !n l. n < (LENGTH l) ==> (!x. ELL n(CONS x l) = ELL n l)
 \ENDTHEOREM
+\THEOREM ELL list
+|- (!l. ELL 0 l = LAST l) /\ (!n l. ELL(SUC n)l = ELL n(BUTLAST l))
+\ENDTHEOREM
 \THEOREM ELL\_EL list
 |- !n l. n < (LENGTH l) ==> (ELL n l = EL(PRE((LENGTH l) - n))l)
 \ENDTHEOREM
+\THEOREM EL\_LENGTH\_APPEND list
+|- !l2 l1. ~NULL l2 ==> (EL(LENGTH l1)(APPEND l1 l2) = HD l2)
+\ENDTHEOREM
+\THEOREM EL\_LENGTH\_SNOC list
+|- !l x. EL(LENGTH l)(SNOC x l) = x
+\ENDTHEOREM
 \THEOREM ELL\_IS\_EL list
 |- !n l. n < (LENGTH l) ==> IS_EL(EL n l)l
 \ENDTHEOREM
@@ -1475,29 +1485,6 @@
 \THEOREM ELL\_SUC\_SNOC list
 |- !n x l. ELL(SUC n)(SNOC x l) = ELL n l
 \ENDTHEOREM
-\THEOREM EL\_APPEND1 list
-|- !n l1 l2. n < (LENGTH l1) ==> (EL n(APPEND l1 l2) = EL n l1)
-\ENDTHEOREM
-\THEOREM EL\_APPEND2 list
-|- !l1 n.
-    (LENGTH l1) <= n ==>
-    (!l2. EL n(APPEND l1 l2) = EL(n - (LENGTH l1))l2)
-\ENDTHEOREM
-\THEOREM EL\_CONS list
-|- !n. 0 < n ==> (!x l. EL n(CONS x l) = EL(PRE n)l)
-\ENDTHEOREM
-\THEOREM EL\_ELL list
-|- !n l. n < (LENGTH l) ==> (EL n l = ELL(PRE((LENGTH l) - n))l)
-\ENDTHEOREM
-\THEOREM EL\_IS\_EL list
-|- !n l. n < (LENGTH l) ==> IS_EL(EL n l)l
-\ENDTHEOREM
-\THEOREM EL\_LENGTH\_APPEND list
-|- !l2 l1. ~NULL l2 ==> (EL(LENGTH l1)(APPEND l1 l2) = HD l2)
-\ENDTHEOREM
-\THEOREM EL\_LENGTH\_SNOC list
-|- !l x. EL(LENGTH l)(SNOC x l) = x
-\ENDTHEOREM
 \THEOREM EL\_MAP list
 |- !n l. n < (LENGTH l) ==> (!f. EL n(MAP f l) = f(EL n l))
 \ENDTHEOREM
@@ -1548,17 +1535,17 @@
       LEFT_ID g e ==>
       (!l. FOLDR f e(FLAT l) = FOLDR g e(MAP(FOLDR f e)l)))
 \ENDTHEOREM
-\THEOREM FILTER list
-|- (!P. FILTER P[] = []) /\
-   (!P x l.
-     FILTER P(CONS x l) = (P x => CONS x(FILTER P l) | FILTER P l))
-\ENDTHEOREM
 \THEOREM FILTER\_APPEND list
 |- !f l1 l2. FILTER f(APPEND l1 l2) = APPEND(FILTER f l1)(FILTER f l2)
 \ENDTHEOREM
 \THEOREM FILTER\_COMM list
 |- !f1 f2 l. FILTER f1(FILTER f2 l) = FILTER f2(FILTER f1 l)
 \ENDTHEOREM
+\THEOREM FILTER list
+|- (!P. FILTER P[] = []) /\
+   (!P x l.
+     FILTER P(CONS x l) = (P x => CONS x(FILTER P l) | FILTER P l))
+\ENDTHEOREM
 \THEOREM FILTER\_FILTER list
 |- !P Q l. FILTER P(FILTER Q l) = FILTER(\x. P x /\ Q x)l
 \ENDTHEOREM
@@ -1583,10 +1570,6 @@
 \THEOREM FILTER\_SNOC list
 |- !P x l. FILTER P(SNOC x l) = (P x => SNOC x(FILTER P l) | FILTER P l)
 \ENDTHEOREM
-\THEOREM FIRSTN list
-|- (!l. FIRSTN 0 l = []) /\
-   (!n x l. FIRSTN(SUC n)(CONS x l) = CONS x(FIRSTN n l))
-\ENDTHEOREM
 \THEOREM FIRSTN\_APPEND1 list
 |- !n l1.
     n <= (LENGTH l1) ==> (!l2. FIRSTN n(APPEND l1 l2) = FIRSTN n l1)
@@ -1599,6 +1582,10 @@
 \THEOREM FIRSTN\_BUTLASTN list
 |- !n l. n <= (LENGTH l) ==> (FIRSTN n l = BUTLASTN((LENGTH l) - n)l)
 \ENDTHEOREM
+\THEOREM FIRSTN list
+|- (!l. FIRSTN 0 l = []) /\
+   (!n x l. FIRSTN(SUC n)(CONS x l) = CONS x(FIRSTN n l))
+\ENDTHEOREM
 \THEOREM FIRSTN\_FIRSTN list
 |- !m l.
     m <= (LENGTH l) ==>
@@ -1619,12 +1606,12 @@
 \THEOREM FIRSTN\_SNOC list
 |- !n l. n <= (LENGTH l) ==> (!x. FIRSTN n(SNOC x l) = FIRSTN n l)
 \ENDTHEOREM
-\THEOREM FLAT list
-|- (FLAT[] = []) /\ (!h t. FLAT(CONS h t) = APPEND h(FLAT t))
-\ENDTHEOREM
 \THEOREM FLAT\_APPEND list
 |- !l1 l2. FLAT(APPEND l1 l2) = APPEND(FLAT l1)(FLAT l2)
 \ENDTHEOREM
+\THEOREM FLAT list
+|- (FLAT[] = []) /\ (!h t. FLAT(CONS h t) = APPEND h(FLAT t))
+\ENDTHEOREM
 \THEOREM FLAT\_FLAT list
 |- !l. FLAT(FLAT l) = FLAT(MAP FLAT l)
 \ENDTHEOREM
@@ -1640,13 +1627,13 @@
 \THEOREM FLAT\_SNOC list
 |- !x l. FLAT(SNOC x l) = APPEND(FLAT l)x
 \ENDTHEOREM
+\THEOREM FOLDL\_APPEND list
+|- !f e l1 l2. FOLDL f e(APPEND l1 l2) = FOLDL f(FOLDL f e l1)l2
+\ENDTHEOREM
 \THEOREM FOLDL list
 |- (!f e. FOLDL f e[] = e) /\
    (!f e x l. FOLDL f e(CONS x l) = FOLDL f(f e x)l)
 \ENDTHEOREM
-\THEOREM FOLDL\_APPEND list
-|- !f e l1 l2. FOLDL f e(APPEND l1 l2) = FOLDL f(FOLDL f e l1)l2
-\ENDTHEOREM
 \THEOREM FOLDL\_FILTER list
 |- !f e P l. FOLDL f e(FILTER P l) = FOLDL(\x y. (P y => f x y | x))e l
 \ENDTHEOREM
@@ -1668,16 +1655,16 @@
 \THEOREM FOLDL\_SNOC\_NIL list
 |- !l. FOLDL(\xs x. SNOC x xs)[]l = l
 \ENDTHEOREM
-\THEOREM FOLDR list
-|- (!f e. FOLDR f e[] = e) /\
-   (!f e x l. FOLDR f e(CONS x l) = f x(FOLDR f e l))
-\ENDTHEOREM
 \THEOREM FOLDR\_APPEND list
 |- !f e l1 l2. FOLDR f e(APPEND l1 l2) = FOLDR f(FOLDR f e l2)l1
 \ENDTHEOREM
 \THEOREM FOLDR\_CONS\_NIL list
 |- !l. FOLDR CONS[]l = l
 \ENDTHEOREM
+\THEOREM FOLDR list
+|- (!f e. FOLDR f e[] = e) /\
+   (!f e x l. FOLDR f e(CONS x l) = f x(FOLDR f e l))
+\ENDTHEOREM
 \THEOREM FOLDR\_FILTER list
 |- !f e P l. FOLDR f e(FILTER P l) = FOLDR(\x y. (P x => f x y | y))e l
 \ENDTHEOREM
@@ -1716,10 +1703,6 @@
 \THEOREM HD list
 |- !h t. HD(CONS h t) = h
 \ENDTHEOREM
-\THEOREM IS\_EL list
-|- (!x. IS_EL x[] = F) /\
-   (!y x l. IS_EL y(CONS x l) = (y = x) \/ IS_EL y l)
-\ENDTHEOREM
 \THEOREM IS\_EL\_APPEND list
 |- !l1 l2 x. IS_EL x(APPEND l1 l2) = IS_EL x l1 \/ IS_EL x l2
 \ENDTHEOREM
@@ -1732,6 +1715,10 @@
 \THEOREM IS\_EL\_DEF list
 |- !x l. IS_EL x l = SOME_EL($= x)l
 \ENDTHEOREM
+\THEOREM IS\_EL list
+|- (!x. IS_EL x[] = F) /\
+   (!y x l. IS_EL y(CONS x l) = (y = x) \/ IS_EL y l)
+\ENDTHEOREM
 \THEOREM IS\_EL\_FILTER list
 |- !P x. P x ==> (!l. IS_EL x(FILTER P l) = IS_EL x l)
 \ENDTHEOREM
@@ -1772,15 +1759,15 @@
 \THEOREM IS\_list\_REP list
 |- !r. IS_list_REP r = (?f n. r = (\m. (m < n => f m | (@x. T))),n)
 \ENDTHEOREM
+\THEOREM IS\_PREFIX\_APPEND list
+|- !l1 l2. IS_PREFIX l1 l2 = (?l. l1 = APPEND l2 l)
+\ENDTHEOREM
 \THEOREM IS\_PREFIX list
 |- (!l. IS_PREFIX l[] = T) /\
    (!x l. IS_PREFIX[](CONS x l) = F) /\
    (!x1 l1 x2 l2.
      IS_PREFIX(CONS x1 l1)(CONS x2 l2) = (x1 = x2) /\ IS_PREFIX l1 l2)
 \ENDTHEOREM
-\THEOREM IS\_PREFIX\_APPEND list
-|- !l1 l2. IS_PREFIX l1 l2 = (?l. l1 = APPEND l2 l)
-\ENDTHEOREM
 \THEOREM IS\_PREFIX\_IS\_SUBLIST list
 |- !l1 l2. IS_PREFIX l1 l2 ==> IS_SUBLIST l1 l2
 \ENDTHEOREM
@@ -1790,6 +1777,9 @@
 \THEOREM IS\_PREFIX\_REVERSE list
 |- !l1 l2. IS_PREFIX(REVERSE l1)(REVERSE l2) = IS_SUFFIX l1 l2
 \ENDTHEOREM
+\THEOREM IS\_SUBLIST\_APPEND list
+|- !l1 l2. IS_SUBLIST l1 l2 = (?l l'. l1 = APPEND l(APPEND l2 l'))
+\ENDTHEOREM
 \THEOREM IS\_SUBLIST list
 |- (!l. IS_SUBLIST l[] = T) /\
    (!x l. IS_SUBLIST[](CONS x l) = F) /\
@@ -1797,33 +1787,32 @@
      IS_SUBLIST(CONS x1 l1)(CONS x2 l2) =
      (x1 = x2) /\ IS_PREFIX l1 l2 \/ IS_SUBLIST l1(CONS x2 l2))
 \ENDTHEOREM
-\THEOREM IS\_SUBLIST\_APPEND list
-|- !l1 l2. IS_SUBLIST l1 l2 = (?l l'. l1 = APPEND l(APPEND l2 l'))
-\ENDTHEOREM
 \THEOREM IS\_SUBLIST\_REVERSE list
 |- !l1 l2. IS_SUBLIST(REVERSE l1)(REVERSE l2) = IS_SUBLIST l1 l2
 \ENDTHEOREM
+\THEOREM IS\_SUFFIX\_APPEND list
+|- !l1 l2. IS_SUFFIX l1 l2 = (?l. l1 = APPEND l l2)
+\ENDTHEOREM
 \THEOREM IS\_SUFFIX list
 |- (!l. IS_SUFFIX l[] = T) /\
    (!x l. IS_SUFFIX[](SNOC x l) = F) /\
    (!x1 l1 x2 l2.
      IS_SUFFIX(SNOC x1 l1)(SNOC x2 l2) = (x1 = x2) /\ IS_SUFFIX l1 l2)
 \ENDTHEOREM
-\THEOREM IS\_SUFFIX\_APPEND list
-|- !l1 l2. IS_SUFFIX l1 l2 = (?l. l1 = APPEND l l2)
-\ENDTHEOREM
 \THEOREM IS\_SUFFIX\_IS\_SUBLIST list
 |- !l1 l2. IS_SUFFIX l1 l2 ==> IS_SUBLIST l1 l2
 \ENDTHEOREM
 \THEOREM IS\_SUFFIX\_REVERSE list
 |- !l1 l2. IS_SUFFIX(REVERSE l1)(REVERSE l2) = IS_PREFIX l1 l2
 \ENDTHEOREM
+\THEOREM LAST\_DEF list
+|- !l. LAST l = HD(SEG 1(PRE(LENGTH l))l)
+\ENDTHEOREM
 \THEOREM LAST list
 |- !x l. LAST(SNOC x l) = x
 \ENDTHEOREM
-\THEOREM LASTN list
-|- (!l. LASTN 0 l = []) /\
-   (!n x l. LASTN(SUC n)(SNOC x l) = SNOC x(LASTN n l))
+\THEOREM LAST\_LASTN\_LAST list
+|- !n l. n <= (LENGTH l) ==> 0 < n ==> (LAST(LASTN n l) = LAST l)
 \ENDTHEOREM
 \THEOREM LASTN\_1 list
 |- !l. ~(l = []) ==> (LASTN 1 l = [LAST l])
@@ -1847,6 +1836,10 @@
 \THEOREM LASTN\_CONS list
 |- !n l. n <= (LENGTH l) ==> (!x. LASTN n(CONS x l) = LASTN n l)
 \ENDTHEOREM
+\THEOREM LASTN list
+|- (!l. LASTN 0 l = []) /\
+   (!n x l. LASTN(SUC n)(SNOC x l) = SNOC x(LASTN n l))
+\ENDTHEOREM
 \THEOREM LASTN\_LASTN list
 |- !l n m.
     m <= (LENGTH l) ==> n <= m ==> (LASTN n(LASTN m l) = LASTN n l)
@@ -1866,15 +1859,6 @@
 \THEOREM LASTN\_SEG list
 |- !n l. n <= (LENGTH l) ==> (LASTN n l = SEG n((LENGTH l) - n)l)
 \ENDTHEOREM
-\THEOREM LAST\_DEF list
-|- !l. LAST l = HD(SEG 1(PRE(LENGTH l))l)
-\ENDTHEOREM
-\THEOREM LAST\_LASTN\_LAST list
-|- !n l. n <= (LENGTH l) ==> 0 < n ==> (LAST(LASTN n l) = LAST l)
-\ENDTHEOREM
-\THEOREM LENGTH list
-|- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t))
-\ENDTHEOREM
 \THEOREM LENGTH\_APPEND list
 |- !l1 l2. LENGTH(APPEND l1 l2) = (LENGTH l1) + (LENGTH l2)
 \ENDTHEOREM
@@ -1891,14 +1875,17 @@
 |- !l n.
     (LENGTH l = SUC n) = (?h l'. (LENGTH l' = n) /\ (l = CONS h l'))
 \ENDTHEOREM
-\THEOREM LENGTH\_EQ list
-|- !x y. (x = y) ==> (LENGTH x = LENGTH y)
+\THEOREM LENGTH list
+|- (LENGTH[] = 0) /\ (!h t. LENGTH(CONS h t) = SUC(LENGTH t))
 \ENDTHEOREM
 \THEOREM LENGTH\_EQ\_CONS list
 |- !P n.
     (!l. (LENGTH l = SUC n) ==> P l) =
     (!l. (LENGTH l = n) ==> (\l. !x. P(CONS x l))l)
 \ENDTHEOREM
+\THEOREM LENGTH\_EQ list
+|- !x y. (x = y) ==> (LENGTH x = LENGTH y)
+\ENDTHEOREM
 \THEOREM LENGTH\_EQ\_NIL list
 |- !P. (!l. (LENGTH l = 0) ==> P l) = P[]
 \ENDTHEOREM
@@ -1920,9 +1907,6 @@
 \THEOREM LENGTH\_LASTN list
 |- !n l. n <= (LENGTH l) ==> (LENGTH(LASTN n l) = n)
 \ENDTHEOREM
-\THEOREM LENGTH\_MAP list
-|- !l f. LENGTH(MAP f l) = LENGTH l
-\ENDTHEOREM
 \THEOREM LENGTH\_MAP2 list
 |- !l1 l2.
     (LENGTH l1 = LENGTH l2) ==>
@@ -1930,6 +1914,9 @@
       (LENGTH(MAP2 f l1 l2) = LENGTH l1) /\
       (LENGTH(MAP2 f l1 l2) = LENGTH l2))
 \ENDTHEOREM
+\THEOREM LENGTH\_MAP list
+|- !l f. LENGTH(MAP f l) = LENGTH l
+\ENDTHEOREM
 \THEOREM LENGTH\_NIL list
 |- !l. (LENGTH l = 0) = (l = [])
 \ENDTHEOREM
@@ -1984,9 +1971,6 @@
 \THEOREM list\_TY\_DEF list
 |- ?rep. TYPE_DEFINITION IS_list_REP rep
 \ENDTHEOREM
-\THEOREM MAP list
-|- (!f. MAP f[] = []) /\ (!f h t. MAP f(CONS h t) = CONS(f h)(MAP f t))
-\ENDTHEOREM
 \THEOREM MAP2 list
 |- (!f. MAP2 f[][] = []) /\
    (!f h1 t1 h2 t2.
@@ -2000,6 +1984,9 @@
 \THEOREM MAP\_APPEND list
 |- !f l1 l2. MAP f(APPEND l1 l2) = APPEND(MAP f l1)(MAP f l2)
 \ENDTHEOREM
+\THEOREM MAP list
+|- (!f. MAP f[] = []) /\ (!f h t. MAP f(CONS h t) = CONS(f h)(MAP f t))
+\ENDTHEOREM
 \THEOREM MAP\_FILTER list
 |- !f P l.
     (!x. P(f x) = P x) ==> (MAP f(FILTER P l) = FILTER P(MAP f l))
@@ -2052,12 +2039,12 @@
 \THEOREM NOT\_SOME\_EL\_ALL\_EL list
 |- !P l. ~SOME_EL P l = ALL_EL($~ o P)l
 \ENDTHEOREM
-\THEOREM NULL list
-|- NULL[] /\ (!h t. ~NULL(CONS h t))
-\ENDTHEOREM
 \THEOREM NULL\_DEF list
 |- (NULL[] = T) /\ (!h t. NULL(CONS h t) = F)
 \ENDTHEOREM
+\THEOREM NULL list
+|- NULL[] /\ (!h t. ~NULL(CONS h t))
+\ENDTHEOREM
 \THEOREM NULL\_EQ\_NIL list
 |- !l. NULL l = (l = [])
 \ENDTHEOREM
@@ -2081,13 +2068,13 @@
    (!n t l.
      PART(CONS n t)l = CONS(FST(SPLIT n l))(PART t(SND(SPLIT n l))))
 \ENDTHEOREM
+\THEOREM PREFIX\_DEF list
+|- !P l. PREFIX P l = FST(SPLITP($~ o P)l)
+\ENDTHEOREM
 \THEOREM PREFIX list
 |- (!P. PREFIX P[] = []) /\
    (!P x l. PREFIX P(CONS x l) = (P x => CONS x(PREFIX P l) | []))
 \ENDTHEOREM
-\THEOREM PREFIX\_DEF list
-|- !P l. PREFIX P l = FST(SPLITP($~ o P)l)
-\ENDTHEOREM
 \THEOREM PREFIX\_FOLDR list
 |- !P l. PREFIX P l = FOLDR(\x l'. (P x => CONS x l' | []))[]l
 \ENDTHEOREM
@@ -2095,12 +2082,12 @@
 |- (!x. REPLICATE 0 x = []) /\
    (!n x. REPLICATE(SUC n)x = CONS x(REPLICATE n x))
 \ENDTHEOREM
-\THEOREM REVERSE list
-|- (REVERSE[] = []) /\ (!x l. REVERSE(CONS x l) = SNOC x(REVERSE l))
-\ENDTHEOREM
 \THEOREM REVERSE\_APPEND list
 |- !l1 l2. REVERSE(APPEND l1 l2) = APPEND(REVERSE l2)(REVERSE l1)
 \ENDTHEOREM
+\THEOREM REVERSE list
+|- (REVERSE[] = []) /\ (!x l. REVERSE(CONS x l) = SNOC x(REVERSE l))
+\ENDTHEOREM
 \THEOREM REVERSE\_EQ\_NIL list
 |- !l. (REVERSE l = []) = (l = [])
 \ENDTHEOREM
@@ -2128,22 +2115,9 @@
    (!f e x l.
      SCANR f e(CONS x l) = CONS(f x(HD(SCANR f e l)))(SCANR f e l))
 \ENDTHEOREM
-\THEOREM SEG list
-|- (!k l. SEG 0 k l = []) /\
-   (!m x l. SEG(SUC m)0(CONS x l) = CONS x(SEG m 0 l)) /\
-   (!m k x l. SEG(SUC m)(SUC k)(CONS x l) = SEG(SUC m)k l)
-\ENDTHEOREM
 \THEOREM SEG\_0\_SNOC list
 |- !m l x. m <= (LENGTH l) ==> (SEG m 0(SNOC x l) = SEG m 0 l)
 \ENDTHEOREM
-\THEOREM SEG\_APPEND list
-|- !m l1 n l2.
-    m < (LENGTH l1) /\
-    (LENGTH l1) <= (n + m) /\
-    (n + m) <= ((LENGTH l1) + (LENGTH l2)) ==>
-    (SEG n m(APPEND l1 l2) =
-     APPEND(SEG((LENGTH l1) - m)m l1)(SEG((n + m) - (LENGTH l1))0 l2))
-\ENDTHEOREM
 \THEOREM SEG\_APPEND1 list
 |- !n m l1.
     (n + m) <= (LENGTH l1) ==> (!l2. SEG n m(APPEND l1 l2) = SEG n m l1)
@@ -2153,6 +2127,19 @@
     (LENGTH l1) <= m /\ n <= (LENGTH l2) ==>
     (SEG n m(APPEND l1 l2) = SEG n(m - (LENGTH l1))l2)
 \ENDTHEOREM
+\THEOREM SEG\_APPEND list
+|- !m l1 n l2.
+    m < (LENGTH l1) /\
+    (LENGTH l1) <= (n + m) /\
+    (n + m) <= ((LENGTH l1) + (LENGTH l2)) ==>
+    (SEG n m(APPEND l1 l2) =
+     APPEND(SEG((LENGTH l1) - m)m l1)(SEG((n + m) - (LENGTH l1))0 l2))
+\ENDTHEOREM
+\THEOREM SEG list
+|- (!k l. SEG 0 k l = []) /\
+   (!m x l. SEG(SUC m)0(CONS x l) = CONS x(SEG m 0 l)) /\
+   (!m k x l. SEG(SUC m)(SUC k)(CONS x l) = SEG(SUC m)k l)
+\ENDTHEOREM
 \THEOREM SEG\_FIRSTN\_BUTFISTN list
 |- !n m l.
     (n + m) <= (LENGTH l) ==> (SEG n m l = FIRSTN n(BUTFIRSTN m l))
@@ -2184,10 +2171,6 @@
 \THEOREM SEG\_SUC\_CONS list
 |- !m n l x. SEG m(SUC n)(CONS x l) = SEG m n l
 \ENDTHEOREM
-\THEOREM SNOC list
-|- (!x. SNOC x[] = [x]) /\
-   (!x x' l. SNOC x(CONS x' l) = CONS x'(SNOC x l))
-\ENDTHEOREM
 \THEOREM SNOC\_11 list
 |- !x l x' l'. (SNOC x l = SNOC x' l') = (x = x') /\ (l = l')
 \ENDTHEOREM
@@ -2200,6 +2183,10 @@
 \THEOREM SNOC\_CASES list
 |- !l. (l = []) \/ (?l' x. l = SNOC x l')
 \ENDTHEOREM
+\THEOREM SNOC list
+|- (!x. SNOC x[] = [x]) /\
+   (!x x' l. SNOC x(CONS x' l) = CONS x'(SNOC x l))
+\ENDTHEOREM
 \THEOREM SNOC\_EQ\_LENGTH\_EQ list
 |- !x1 l1 x2 l2. (SNOC x1 l1 = SNOC x2 l2) ==> (LENGTH l1 = LENGTH l2)
 \ENDTHEOREM
@@ -2212,10 +2199,6 @@
 \THEOREM SNOC\_REVERSE\_CONS list
 |- !x l. SNOC x l = REVERSE(CONS x(REVERSE l))
 \ENDTHEOREM
-\THEOREM SOME\_EL list
-|- (!P. SOME_EL P[] = F) /\
-   (!P x l. SOME_EL P(CONS x l) = P x \/ SOME_EL P l)
-\ENDTHEOREM
 \THEOREM SOME\_EL\_APPEND list
 |- !P l1 l2. SOME_EL P(APPEND l1 l2) = SOME_EL P l1 \/ SOME_EL P l2
 \ENDTHEOREM
@@ -2230,6 +2213,10 @@
 \THEOREM SOME\_EL\_DISJ list
 |- !P Q l. SOME_EL(\x. P x \/ Q x)l = SOME_EL P l \/ SOME_EL Q l
 \ENDTHEOREM
+\THEOREM SOME\_EL list
+|- (!P. SOME_EL P[] = F) /\
+   (!P x l. SOME_EL P(CONS x l) = P x \/ SOME_EL P l)
+\ENDTHEOREM
 \THEOREM SOME\_EL\_FIRSTN list
 |- !m l. m <= (LENGTH l) ==> (!P. SOME_EL P(FIRSTN m l) ==> SOME_EL P l)
 \ENDTHEOREM
@@ -2277,12 +2264,12 @@
 \THEOREM SUFFIX\_DEF list
 |- !P l. SUFFIX P l = FOLDL(\l' x. (P x => SNOC x l' | []))[]l
 \ENDTHEOREM
-\THEOREM SUM list
-|- (SUM[] = 0) /\ (!h t. SUM(CONS h t) = h + (SUM t))
-\ENDTHEOREM
 \THEOREM SUM\_APPEND list
 |- !l1 l2. SUM(APPEND l1 l2) = (SUM l1) + (SUM l2)
 \ENDTHEOREM
+\THEOREM SUM list
+|- (SUM[] = 0) /\ (!h t. SUM(CONS h t) = h + (SUM t))
+\ENDTHEOREM
 \THEOREM SUM\_FLAT list
 |- !l. SUM(FLAT l) = SUM(MAP SUM l)
 \ENDTHEOREM
@@ -2336,8 +2323,7 @@
 \THEOREM ZIP\_UNZIP list
 |- !l. ZIP(UNZIP l) = l
 \ENDTHEOREM
-\section{Theorems about trees}
-\THEOREM AP ltree
+\section{Theorems about trees}\THEOREM AP ltree
 |- (!l. AP[]l = []) /\
    (!h t l. AP(CONS h t)l = CONS(h(HD l))(AP t(TL l)))
 \ENDTHEOREM
@@ -2372,21 +2358,21 @@
 \THEOREM ltree\_TY\_DEF ltree
 |- ?rep. TYPE_DEFINITION Is_ltree rep
 \ENDTHEOREM
-\THEOREM Node ltree
-|- !v tl.
-    Node v tl =
-    ABS_ltree
-    (node(MAP(FST o REP_ltree)tl),CONS v(FLAT(MAP(SND o REP_ltree)tl)))
-\ENDTHEOREM
-\THEOREM node tree
-|- !tl. node tl = ABS_tree(node_REP(MAP REP_tree tl))
+\THEOREM node\_11 tree
+|- !tl1 tl2. (node tl1 = node tl2) = (tl1 = tl2)
 \ENDTHEOREM
 \THEOREM Node\_11 ltree
 |- !v1 v2 trl1 trl2.
     (Node v1 trl1 = Node v2 trl2) = (v1 = v2) /\ (trl1 = trl2)
 \ENDTHEOREM
-\THEOREM node\_11 tree
-|- !tl1 tl2. (node tl1 = node tl2) = (tl1 = tl2)
+\THEOREM node tree
+|- !tl. node tl = ABS_tree(node_REP(MAP REP_tree tl))
+\ENDTHEOREM
+\THEOREM Node ltree
+|- !v tl.
+    Node v tl =
+    ABS_ltree
+    (node(MAP(FST o REP_ltree)tl),CONS v(FLAT(MAP(SND o REP_ltree)tl)))
 \ENDTHEOREM
 \THEOREM Node\_onto ltree
 |- !l. ?v trl. l = Node v trl
@@ -2426,8 +2412,7 @@
     trf n f =
     (@fn. !trl. (HT(node trl)) <= n ==> (fn(node trl) = f(MAP fn trl)))
 \ENDTHEOREM
-\section{Theorems used to define types}
-\THEOREM ABS\_REP\_THM BASIC-HOL
+\section{Theorems used to define types}\THEOREM ABS\_REP\_THM BASIC-HOL
 |- !P.
     (?rep. TYPE_DEFINITION P rep) ==>
     (?rep abs. (!a. abs(rep a) = a) /\ (!r. P r = (rep(abs r) = r)))
@@ -2435,17 +2420,11 @@
 \THEOREM exists\_TRP tydefs
 |- !P. (?v. P v[]) ==> (?t. TRP P t)
 \ENDTHEOREM
-\THEOREM TRP tydefs
-|- !P v tl. TRP P(Node v tl) = P v tl /\ ALL_EL(TRP P)tl
-\ENDTHEOREM
 \THEOREM TRP\_DEF tydefs
 |- !P. TRP P = (@trp. !v tl. trp(Node v tl) = P v tl /\ ALL_EL trp tl)
 \ENDTHEOREM
-\THEOREM TYPE\_DEFINITION bool
-|- !P rep.
-    TYPE_DEFINITION P rep =
-    (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
-    (!x. P x = (?x'. x = rep x'))
+\THEOREM TRP tydefs
+|- !P v tl. TRP P(Node v tl) = P v tl /\ ALL_EL(TRP P)tl
 \ENDTHEOREM
 \THEOREM TY\_DEF\_THM tydefs
 |- !REP ABS P.
@@ -2456,3 +2435,9 @@
         P v(MAP REP tl) ==>
         (fn(ABS(Node v(MAP REP tl))) = f(MAP fn tl)v tl))
 \ENDTHEOREM
+\THEOREM TYPE\_DEFINITION bool
+|- !P rep.
+    TYPE_DEFINITION P rep =
+    (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
+    (!x. P x = (?x'. x = rep x'))
+\ENDTHEOREM