Structure listTheory


Source File Identifier index Theory binding index

signature listTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ALL_DISTINCT : thm
    val APPEND : thm
    val DROP_def : thm
    val EL : thm
    val EVERY_DEF : thm
    val EVERYi_def : thm
    val EXISTS_DEF : thm
    val FILTER : thm
    val FIND_def : thm
    val FLAT : thm
    val FOLDL : thm
    val FOLDR : thm
    val FRONT_DEF : thm
    val GENLIST : thm
    val GENLIST_AUX : thm
    val HD : thm
    val INDEX_FIND_def : thm
    val INDEX_OF_def : thm
    val LAST_DEF : thm
    val LENGTH : thm
    val LEN_DEF : thm
    val LIST_APPLY_def : thm
    val LIST_BIND_def : thm
    val LIST_GUARD_def : thm
    val LIST_IGNORE_BIND_def : thm
    val LIST_LIFT2_def : thm
    val LIST_TO_SET_DEF : thm
    val LLEX_def : thm
    val LRC_def : thm
    val LUPDATE_def : thm
    val MAP : thm
    val NULL_DEF : thm
    val OPT_MMAP_def : thm
    val PAD_LEFT : thm
    val PAD_RIGHT : thm
    val REVERSE_DEF : thm
    val REV_DEF : thm
    val SET_TO_LIST_primitive_def : thm
    val SHORTLEX_def : thm
    val SNOC : thm
    val SUM : thm
    val SUM_ACC_DEF : thm
    val TAKE_def : thm
    val TL_DEF : thm
    val UNIQUE_DEF : thm
    val UNZIP : thm
    val ZIP_def : thm
    val dropWhile_def : thm
    val isPREFIX : thm
    val list_TY_DEF : thm
    val list_case_def : thm
    val list_size_def : thm
    val nub_def : thm
    val oEL_def : thm
    val oHD_def : thm
    val splitAtPki_def : thm
  
  (*  Theorems  *)
    val ALL_DISTINCT_APPEND : thm
    val ALL_DISTINCT_CARD_LIST_TO_SET : thm
    val ALL_DISTINCT_DROP : thm
    val ALL_DISTINCT_EL_IMP : thm
    val ALL_DISTINCT_FILTER : thm
    val ALL_DISTINCT_FILTER_EL_IMP : thm
    val ALL_DISTINCT_FLAT_REVERSE : thm
    val ALL_DISTINCT_GENLIST : thm
    val ALL_DISTINCT_MAP : thm
    val ALL_DISTINCT_MAP_INJ : thm
    val ALL_DISTINCT_REVERSE : thm
    val ALL_DISTINCT_SET_TO_LIST : thm
    val ALL_DISTINCT_SING : thm
    val ALL_DISTINCT_SNOC : thm
    val ALL_DISTINCT_ZIP : thm
    val ALL_DISTINCT_ZIP_SWAP : thm
    val APPEND_11 : thm
    val APPEND_11_LENGTH : thm
    val APPEND_ASSOC : thm
    val APPEND_EQ_APPEND : thm
    val APPEND_EQ_APPEND_MID : thm
    val APPEND_EQ_CONS : thm
    val APPEND_EQ_SELF : thm
    val APPEND_EQ_SING : thm
    val APPEND_FRONT_LAST : thm
    val APPEND_LENGTH_EQ : thm
    val APPEND_NIL : thm
    val APPEND_SNOC : thm
    val APPEND_eq_NIL : thm
    val BIGUNION_IMAGE_set_SUBSET : thm
    val CARD_LIST_TO_SET : thm
    val CARD_LIST_TO_SET_ALL_DISTINCT : thm
    val CONS : thm
    val CONS_11 : thm
    val CONS_ACYCLIC : thm
    val DISJOINT_GENLIST_PLUS : thm
    val DROP_0 : thm
    val DROP_GENLIST : thm
    val DROP_LENGTH_TOO_LONG : thm
    val DROP_NIL : thm
    val DROP_compute : thm
    val DROP_cons : thm
    val DROP_nil : thm
    val DROP_splitAtPki : thm
    val EL_ALL_DISTINCT_EL_EQ : thm
    val EL_APPEND_EQN : thm
    val EL_DROP : thm
    val EL_GENLIST : thm
    val EL_LENGTH_SNOC : thm
    val EL_LENGTH_dropWhile_REVERSE : thm
    val EL_LUPDATE : thm
    val EL_MAP : thm
    val EL_MAP2 : thm
    val EL_REVERSE : thm
    val EL_SNOC : thm
    val EL_TAKE : thm
    val EL_ZIP : thm
    val EL_compute : thm
    val EL_restricted : thm
    val EL_simp : thm
    val EL_simp_restricted : thm
    val EQ_LIST : thm
    val EVERY2_EVERY : thm
    val EVERY2_LENGTH : thm
    val EVERY2_LUPDATE_same : thm
    val EVERY2_MAP : thm
    val EVERY2_MEM_MONO : thm
    val EVERY2_REVERSE : thm
    val EVERY2_THM : thm
    val EVERY2_cong : thm
    val EVERY2_mono : thm
    val EVERY2_refl : thm
    val EVERY2_sym : thm
    val EVERY2_trans : thm
    val EVERY_APPEND : thm
    val EVERY_CONG : thm
    val EVERY_CONJ : thm
    val EVERY_EL : thm
    val EVERY_FILTER : thm
    val EVERY_FILTER_IMP : thm
    val EVERY_FLAT : thm
    val EVERY_GENLIST : thm
    val EVERY_MAP : thm
    val EVERY_MEM : thm
    val EVERY_MEM_MONO : thm
    val EVERY_MONOTONIC : thm
    val EVERY_NOT_EXISTS : thm
    val EVERY_SIMP : thm
    val EVERY_SNOC : thm
    val EXISTS_APPEND : thm
    val EXISTS_CONG : thm
    val EXISTS_GENLIST : thm
    val EXISTS_LIST : thm
    val EXISTS_LIST_EQ_MAP : thm
    val EXISTS_MAP : thm
    val EXISTS_MEM : thm
    val EXISTS_NOT_EVERY : thm
    val EXISTS_SIMP : thm
    val EXISTS_SNOC : thm
    val FILTER_ALL_DISTINCT : thm
    val FILTER_APPEND_DISTRIB : thm
    val FILTER_COND_REWRITE : thm
    val FILTER_EQ_APPEND : thm
    val FILTER_EQ_CONS : thm
    val FILTER_EQ_ID : thm
    val FILTER_EQ_NIL : thm
    val FILTER_F : thm
    val FILTER_NEQ_ID : thm
    val FILTER_NEQ_NIL : thm
    val FILTER_REVERSE : thm
    val FILTER_T : thm
    val FINITE_LIST_TO_SET : thm
    val FLAT_APPEND : thm
    val FLAT_EQ_NIL : thm
    val FLAT_compute : thm
    val FOLDL2_FOLDL : thm
    val FOLDL2_cong : thm
    val FOLDL2_def : thm
    val FOLDL2_ind : thm
    val FOLDL_CONG : thm
    val FOLDL_EQ_FOLDR : thm
    val FOLDL_SNOC : thm
    val FOLDL_UNION_BIGUNION : thm
    val FOLDL_UNION_BIGUNION_paired : thm
    val FOLDL_ZIP_SAME : thm
    val FOLDR_CONG : thm
    val FOLDR_CONS : thm
    val FORALL_LIST : thm
    val FRONT_CONS : thm
    val FRONT_CONS_EQ_NIL : thm
    val FRONT_SNOC : thm
    val GENLIST_APPEND : thm
    val GENLIST_AUX_compute : thm
    val GENLIST_CONS : thm
    val GENLIST_EL : thm
    val GENLIST_EL_MAP : thm
    val GENLIST_FUN_EQ : thm
    val GENLIST_GENLIST_AUX : thm
    val GENLIST_ID : thm
    val GENLIST_NUMERALS : thm
    val GENLIST_PLUS_APPEND : thm
    val HD_DROP : thm
    val HD_GENLIST : thm
    val HD_GENLIST_COR : thm
    val HD_REVERSE : thm
    val HD_dropWhile : thm
    val IMAGE_EL_count_LENGTH : thm
    val IMP_EVERY_LUPDATE : thm
    val INFINITE_LIST_UNIV : thm
    val INJ_MAP_EQ : thm
    val INJ_MAP_EQ_IFF : thm
    val ITSET_eq_FOLDL_SET_TO_LIST : thm
    val LAST_APPEND_CONS : thm
    val LAST_CONS : thm
    val LAST_CONS_cond : thm
    val LAST_EL : thm
    val LAST_MAP : thm
    val LAST_REVERSE : thm
    val LAST_SNOC : thm
    val LAST_compute : thm
    val LENGTH_APPEND : thm
    val LENGTH_CONS : thm
    val LENGTH_DROP : thm
    val LENGTH_EQ_CONS : thm
    val LENGTH_EQ_NIL : thm
    val LENGTH_EQ_NUM : thm
    val LENGTH_EQ_NUM_compute : thm
    val LENGTH_EQ_SUM : thm
    val LENGTH_FILTER_LEQ_MONO : thm
    val LENGTH_FRONT_CONS : thm
    val LENGTH_GENLIST : thm
    val LENGTH_LEN : thm
    val LENGTH_LT_SHORTLEX : thm
    val LENGTH_LUPDATE : thm
    val LENGTH_MAP : thm
    val LENGTH_MAP2 : thm
    val LENGTH_NIL : thm
    val LENGTH_NIL_SYM : thm
    val LENGTH_REVERSE : thm
    val LENGTH_SNOC : thm
    val LENGTH_TAKE : thm
    val LENGTH_TAKE_EQ : thm
    val LENGTH_TL : thm
    val LENGTH_UNZIP : thm
    val LENGTH_ZIP : thm
    val LENGTH_ZIP_MIN : thm
    val LENGTH_dropWhile_LESS_EQ : thm
    val LENGTH_o_REVERSE : thm
    val LEN_LENGTH_LEM : thm
    val LIST_APPLY_o : thm
    val LIST_BIND_APPEND : thm
    val LIST_BIND_ID : thm
    val LIST_BIND_LIST_BIND : thm
    val LIST_BIND_MAP : thm
    val LIST_BIND_THM : thm
    val LIST_EQ : thm
    val LIST_EQ_MAP_PAIR : thm
    val LIST_EQ_REWRITE : thm
    val LIST_NOT_EQ : thm
    val LIST_REL_APPEND : thm
    val LIST_REL_APPEND_EQ : thm
    val LIST_REL_APPEND_IMP : thm
    val LIST_REL_APPEND_suff : thm
    val LIST_REL_CONJ : thm
    val LIST_REL_CONS1 : thm
    val LIST_REL_CONS2 : thm
    val LIST_REL_EL_EQN : thm
    val LIST_REL_EVERY_ZIP : thm
    val LIST_REL_LENGTH : thm
    val LIST_REL_MAP1 : thm
    val LIST_REL_MAP2 : thm
    val LIST_REL_MAP_inv_image : thm
    val LIST_REL_MEM_IMP : thm
    val LIST_REL_NIL : thm
    val LIST_REL_O : thm
    val LIST_REL_SNOC : thm
    val LIST_REL_SPLIT1 : thm
    val LIST_REL_SPLIT2 : thm
    val LIST_REL_cases : thm
    val LIST_REL_def : thm
    val LIST_REL_eq : thm
    val LIST_REL_ind : thm
    val LIST_REL_mono : thm
    val LIST_REL_rules : thm
    val LIST_REL_strongind : thm
    val LIST_REL_trans : thm
    val LIST_TO_SET : thm
    val LIST_TO_SET_APPEND : thm
    val LIST_TO_SET_EQ_EMPTY : thm
    val LIST_TO_SET_FILTER : thm
    val LIST_TO_SET_FLAT : thm
    val LIST_TO_SET_GENLIST : thm
    val LIST_TO_SET_MAP : thm
    val LIST_TO_SET_REVERSE : thm
    val LIST_TO_SET_SNOC : thm
    val LIST_TO_SET_THM : thm
    val LLEX_CONG : thm
    val LLEX_EL_THM : thm
    val LLEX_MONO : thm
    val LLEX_NIL2 : thm
    val LLEX_THM : thm
    val LLEX_not_WF : thm
    val LLEX_total : thm
    val LLEX_transitive : thm
    val LRC_MEM : thm
    val LRC_MEM_right : thm
    val LUPDATE_LENGTH : thm
    val LUPDATE_MAP : thm
    val LUPDATE_NIL : thm
    val LUPDATE_SAME : thm
    val LUPDATE_SEM : thm
    val LUPDATE_SNOC : thm
    val LUPDATE_SOME_MAP : thm
    val LUPDATE_compute : thm
    val MAP2 : thm
    val MAP2_APPEND : thm
    val MAP2_CONG : thm
    val MAP2_DEF : thm
    val MAP2_MAP : thm
    val MAP2_NIL : thm
    val MAP2_ZIP : thm
    val MAP2_ind : thm
    val MAP_APPEND : thm
    val MAP_APPEND_MAP_EQ : thm
    val MAP_CONG : thm
    val MAP_DROP : thm
    val MAP_EQ_APPEND : thm
    val MAP_EQ_CONS : thm
    val MAP_EQ_EVERY2 : thm
    val MAP_EQ_NIL : thm
    val MAP_EQ_SING : thm
    val MAP_EQ_f : thm
    val MAP_FLAT : thm
    val MAP_FRONT : thm
    val MAP_GENLIST : thm
    val MAP_ID : thm
    val MAP_LIST_BIND : thm
    val MAP_MAP_o : thm
    val MAP_SNOC : thm
    val MAP_TAKE : thm
    val MAP_TL : thm
    val MAP_ZIP : thm
    val MAP_ZIP_SAME : thm
    val MAP_o : thm
    val MEM : thm
    val MEM_APPEND : thm
    val MEM_APPEND_lemma : thm
    val MEM_DROP : thm
    val MEM_EL : thm
    val MEM_FILTER : thm
    val MEM_FLAT : thm
    val MEM_GENLIST : thm
    val MEM_LUPDATE : thm
    val MEM_LUPDATE_E : thm
    val MEM_MAP : thm
    val MEM_REVERSE : thm
    val MEM_SET_TO_LIST : thm
    val MEM_SNOC : thm
    val MEM_SPLIT : thm
    val MEM_SPLIT_APPEND_first : thm
    val MEM_SPLIT_APPEND_last : thm
    val MEM_ZIP : thm
    val MEM_ZIP_MEM_MAP : thm
    val MEM_dropWhile_IMP : thm
    val MONO_EVERY : thm
    val MONO_EXISTS : thm
    val NOT_CONS_NIL : thm
    val NOT_EQ_LIST : thm
    val NOT_EVERY : thm
    val NOT_EXISTS : thm
    val NOT_NIL_CONS : thm
    val NOT_NIL_EQ_LENGTH_NOT_0 : thm
    val NOT_NULL_MEM : thm
    val NRC_LRC : thm
    val NULL : thm
    val NULL_APPEND : thm
    val NULL_EQ : thm
    val NULL_FILTER : thm
    val NULL_GENLIST : thm
    val NULL_LENGTH : thm
    val OPT_MMAP_cong : thm
    val REVERSE_11 : thm
    val REVERSE_APPEND : thm
    val REVERSE_EQ_NIL : thm
    val REVERSE_EQ_SING : thm
    val REVERSE_GENLIST : thm
    val REVERSE_REV : thm
    val REVERSE_REVERSE : thm
    val REVERSE_SNOC : thm
    val REVERSE_SNOC_DEF : thm
    val REVERSE_o_REVERSE : thm
    val REV_REVERSE_LEM : thm
    val SET_TO_LIST_CARD : thm
    val SET_TO_LIST_EMPTY : thm
    val SET_TO_LIST_IND : thm
    val SET_TO_LIST_INV : thm
    val SET_TO_LIST_IN_MEM : thm
    val SET_TO_LIST_SING : thm
    val SET_TO_LIST_THM : thm
    val SHORTLEX_LENGTH_LE : thm
    val SHORTLEX_MONO : thm
    val SHORTLEX_NIL2 : thm
    val SHORTLEX_THM : thm
    val SHORTLEX_total : thm
    val SHORTLEX_transitive : thm
    val SINGL_APPLY_MAP : thm
    val SINGL_APPLY_PERMUTE : thm
    val SINGL_LIST_APPLY_L : thm
    val SINGL_LIST_APPLY_R : thm
    val SINGL_SINGL_APPLY : thm
    val SING_HD : thm
    val SNOC_11 : thm
    val SNOC_APPEND : thm
    val SNOC_Axiom : thm
    val SNOC_CASES : thm
    val SNOC_INDUCT : thm
    val SUM_ACC_SUM_LEM : thm
    val SUM_APPEND : thm
    val SUM_IMAGE_LIST_TO_SET_upper_bound : thm
    val SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST : thm
    val SUM_MAP_FOLDL : thm
    val SUM_MAP_MEM_bound : thm
    val SUM_MAP_PLUS : thm
    val SUM_MAP_PLUS_ZIP : thm
    val SUM_SNOC : thm
    val SUM_SUM_ACC : thm
    val SUM_eq_0 : thm
    val SWAP_REVERSE : thm
    val SWAP_REVERSE_SYM : thm
    val TAKE1 : thm
    val TAKE1_DROP : thm
    val TAKE_0 : thm
    val TAKE_APPEND1 : thm
    val TAKE_APPEND2 : thm
    val TAKE_DROP : thm
    val TAKE_EQ_NIL : thm
    val TAKE_GENLIST : thm
    val TAKE_LENGTH_ID : thm
    val TAKE_LENGTH_ID_rwt : thm
    val TAKE_LENGTH_TOO_LONG : thm
    val TAKE_SUM : thm
    val TAKE_TAKE_MIN : thm
    val TAKE_compute : thm
    val TAKE_cons : thm
    val TAKE_nil : thm
    val TAKE_splitAtPki : thm
    val TL : thm
    val TL_GENLIST : thm
    val UNION_APPEND : thm
    val UNIQUE_FILTER : thm
    val UNIQUE_LENGTH_FILTER : thm
    val UNZIP_MAP : thm
    val UNZIP_THM : thm
    val UNZIP_ZIP : thm
    val WF_LIST_PRED : thm
    val WF_SHORTLEX : thm
    val WF_SHORTLEX_same_lengths : thm
    val ZIP : thm
    val ZIP_DROP : thm
    val ZIP_EQ_NIL : thm
    val ZIP_GENLIST : thm
    val ZIP_MAP : thm
    val ZIP_UNZIP : thm
    val all_distinct_nub : thm
    val datatype_list : thm
    val dropWhile_APPEND_EVERY : thm
    val dropWhile_APPEND_EXISTS : thm
    val dropWhile_eq_nil : thm
    val dropWhile_splitAtPki : thm
    val el_append3 : thm
    val every_zip_fst : thm
    val every_zip_snd : thm
    val exists_list_GENLIST : thm
    val isPREFIX_CONSR : thm
    val isPREFIX_NILR : thm
    val isPREFIX_THM : thm
    val last_drop : thm
    val lazy_list_case_compute : thm
    val length_nub_append : thm
    val list_11 : thm
    val list_Axiom : thm
    val list_Axiom_old : thm
    val list_CASES : thm
    val list_INDUCT : thm
    val list_INDUCT0 : thm
    val list_case_compute : thm
    val list_case_cong : thm
    val list_case_eq : thm
    val list_distinct : thm
    val list_induction : thm
    val list_nchotomy : thm
    val list_size_cong : thm
    val list_to_set_diff : thm
    val lupdate_append : thm
    val lupdate_append2 : thm
    val mem_exists_set : thm
    val nub_append : thm
    val nub_set : thm
    val oEL_DROP : thm
    val oEL_EQ_EL : thm
    val oEL_LUPDATE : thm
    val oEL_TAKE_E : thm
    val oEL_THM : thm
    val oHD_thm : thm
    val splitAtPki_APPEND : thm
    val splitAtPki_EQN : thm
    val splitAtPki_MAP : thm
    val splitAtPki_RAND : thm
    val splitAtPki_change_predicate : thm
  
  val list_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [ind_type] Parent theory of "list"
   
   [pred_set] Parent theory of "list"
   
   [ALL_DISTINCT]  Definition
      
      ⊢ (ALL_DISTINCT [] ⇔ T) ∧
        ∀h t. ALL_DISTINCT (h::t) ⇔ ¬MEM h t ∧ ALL_DISTINCT t
   
   [APPEND]  Definition
      
      ⊢ (∀l. [] ⧺ l = l) ∧ ∀l1 l2 h. h::l1 ⧺ l2 = h::(l1 ⧺ l2)
   
   [DROP_def]  Definition
      
      ⊢ (∀n. DROP n [] = []) ∧
        ∀n x xs. DROP n (x::xs) = if n = 0 then x::xs else DROP (n − 1) xs
   
   [EL]  Definition
      
      ⊢ (∀l. EL 0 l = HD l) ∧ ∀l n. EL (SUC n) l = EL n (TL l)
   
   [EVERY_DEF]  Definition
      
      ⊢ (∀P. EVERY P [] ⇔ T) ∧ ∀P h t. EVERY P (h::t) ⇔ P h ∧ EVERY P t
   
   [EVERYi_def]  Definition
      
      ⊢ (∀P. EVERYi P [] ⇔ T) ∧
        ∀P h t. EVERYi P (h::t) ⇔ P 0 h ∧ EVERYi (P ∘ SUC) t
   
   [EXISTS_DEF]  Definition
      
      ⊢ (∀P. EXISTS P [] ⇔ F) ∧ ∀P h t. EXISTS P (h::t) ⇔ P h ∨ EXISTS P t
   
   [FILTER]  Definition
      
      ⊢ (∀P. FILTER P [] = []) ∧
        ∀P h t. FILTER P (h::t) = if P h then h::FILTER P t else FILTER P t
   
   [FIND_def]  Definition
      
      ⊢ ∀P. FIND P = OPTION_MAP SND ∘ INDEX_FIND 0 P
   
   [FLAT]  Definition
      
      ⊢ FLAT [] = [] ∧ ∀h t. FLAT (h::t) = h ⧺ FLAT t
   
   [FOLDL]  Definition
      
      ⊢ (∀f e. FOLDL f e [] = e) ∧
        ∀f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l
   
   [FOLDR]  Definition
      
      ⊢ (∀f e. FOLDR f e [] = e) ∧
        ∀f e x l. FOLDR f e (x::l) = f x (FOLDR f e l)
   
   [FRONT_DEF]  Definition
      
      ⊢ ∀h t. FRONT (h::t) = if t = [] then [] else h::FRONT t
   
   [GENLIST]  Definition
      
      ⊢ (∀f. GENLIST f 0 = []) ∧
        ∀f n. GENLIST f (SUC n) = SNOC (f n) (GENLIST f n)
   
   [GENLIST_AUX]  Definition
      
      ⊢ (∀f l. GENLIST_AUX f 0 l = l) ∧
        ∀f n l. GENLIST_AUX f (SUC n) l = GENLIST_AUX f n (f n::l)
   
   [HD]  Definition
      
      ⊢ ∀h t. HD (h::t) = h
   
   [INDEX_FIND_def]  Definition
      
      ⊢ (∀i P. INDEX_FIND i P [] = NONE) ∧
        ∀i P h t.
            INDEX_FIND i P (h::t) =
            if P h then SOME (i,h) else INDEX_FIND (SUC i) P t
   
   [INDEX_OF_def]  Definition
      
      ⊢ ∀x. INDEX_OF x = OPTION_MAP FST ∘ INDEX_FIND 0 ($= x)
   
   [LAST_DEF]  Definition
      
      ⊢ ∀h t. LAST (h::t) = if t = [] then h else LAST t
   
   [LENGTH]  Definition
      
      ⊢ LENGTH [] = 0 ∧ ∀h t. LENGTH (h::t) = SUC (LENGTH t)
   
   [LEN_DEF]  Definition
      
      ⊢ (∀n. LEN [] n = n) ∧ ∀h t n. LEN (h::t) n = LEN t (n + 1)
   
   [LIST_APPLY_def]  Definition
      
      ⊢ ∀fs xs. fs <*> xs = LIST_BIND fs (combin$C MAP xs)
   
   [LIST_BIND_def]  Definition
      
      ⊢ ∀l f. LIST_BIND l f = FLAT (MAP f l)
   
   [LIST_GUARD_def]  Definition
      
      ⊢ ∀b. LIST_GUARD b = if b then [()] else []
   
   [LIST_IGNORE_BIND_def]  Definition
      
      ⊢ ∀m1 m2. LIST_IGNORE_BIND m1 m2 = LIST_BIND m1 (K m2)
   
   [LIST_LIFT2_def]  Definition
      
      ⊢ ∀f xs ys. LIST_LIFT2 f xs ys = MAP f xs <*> ys
   
   [LIST_TO_SET_DEF]  Definition
      
      ⊢ (∀x. set [] x ⇔ F) ∧ ∀h t x. set (h::t) x ⇔ x = h ∨ set t x
   
   [LLEX_def]  Definition
      
      ⊢ (∀R l2. LLEX R [] l2 ⇔ l2 ≠ []) ∧
        ∀R h1 t1 l2.
            LLEX R (h1::t1) l2 ⇔
            case l2 of
              [] => F
            | h2::t2 =>
              if R h1 h2 then T else if h1 = h2 then LLEX R t1 t2 else F
   
   [LRC_def]  Definition
      
      ⊢ (∀R x y. LRC R [] x y ⇔ x = y) ∧
        ∀R h t x y. LRC R (h::t) x y ⇔ x = h ∧ ∃z. R x z ∧ LRC R t z y
   
   [LUPDATE_def]  Definition
      
      ⊢ (∀e n. LUPDATE e n [] = []) ∧ (∀e x l. LUPDATE e 0 (x::l) = e::l) ∧
        ∀e n x l. LUPDATE e (SUC n) (x::l) = x::LUPDATE e n l
   
   [MAP]  Definition
      
      ⊢ (∀f. MAP f [] = []) ∧ ∀f h t. MAP f (h::t) = f h::MAP f t
   
   [NULL_DEF]  Definition
      
      ⊢ (NULL [] ⇔ T) ∧ ∀h t. NULL (h::t) ⇔ F
   
   [OPT_MMAP_def]  Definition
      
      ⊢ (∀f. OPT_MMAP f [] = SOME []) ∧
        ∀f h0 t0.
            OPT_MMAP f (h0::t0) =
            OPTION_BIND (f h0)
              (λh. OPTION_BIND (OPT_MMAP f t0) (λt. SOME (h::t)))
   
   [PAD_LEFT]  Definition
      
      ⊢ ∀c n s. PAD_LEFT c n s = GENLIST (K c) (n − LENGTH s) ⧺ s
   
   [PAD_RIGHT]  Definition
      
      ⊢ ∀c n s. PAD_RIGHT c n s = s ⧺ GENLIST (K c) (n − LENGTH s)
   
   [REVERSE_DEF]  Definition
      
      ⊢ REVERSE [] = [] ∧ ∀h t. REVERSE (h::t) = REVERSE t ⧺ [h]
   
   [REV_DEF]  Definition
      
      ⊢ (∀acc. REV [] acc = acc) ∧
        ∀h t acc. REV (h::t) acc = REV t (h::acc)
   
   [SET_TO_LIST_primitive_def]  Definition
      
      ⊢ SET_TO_LIST =
        WFREC (@R. WF R ∧ ∀s. FINITE s ∧ s ≠ ∅ ⇒ R (REST s) s)
          (λSET_TO_LIST a.
               I
                 (if FINITE a then
                    if a = ∅ then [] else CHOICE a::SET_TO_LIST (REST a)
                  else ARB))
   
   [SHORTLEX_def]  Definition
      
      ⊢ (∀R l2. SHORTLEX R [] l2 ⇔ l2 ≠ []) ∧
        ∀R h1 t1 l2.
            SHORTLEX R (h1::t1) l2 ⇔
            case l2 of
              [] => F
            | h2::t2 =>
              if LENGTH t1 < LENGTH t2 then T
              else if LENGTH t1 = LENGTH t2 then
                if R h1 h2 then T
                else if h1 = h2 then SHORTLEX R t1 t2
                else F
              else F
   
   [SNOC]  Definition
      
      ⊢ (∀x. SNOC x [] = [x]) ∧ ∀x x' l. SNOC x (x'::l) = x'::SNOC x l
   
   [SUM]  Definition
      
      ⊢ SUM [] = 0 ∧ ∀h t. SUM (h::t) = h + SUM t
   
   [SUM_ACC_DEF]  Definition
      
      ⊢ (∀acc. SUM_ACC [] acc = acc) ∧
        ∀h t acc. SUM_ACC (h::t) acc = SUM_ACC t (h + acc)
   
   [TAKE_def]  Definition
      
      ⊢ (∀n. TAKE n [] = []) ∧
        ∀n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n − 1) xs
   
   [TL_DEF]  Definition
      
      ⊢ TL [] = [] ∧ ∀h t. TL (h::t) = t
   
   [UNIQUE_DEF]  Definition
      
      ⊢ ∀e L.
            UNIQUE e L ⇔ ∃L1 L2. L1 ⧺ [e] ⧺ L2 = L ∧ ¬MEM e L1 ∧ ¬MEM e L2
   
   [UNZIP]  Definition
      
      ⊢ UNZIP [] = ([],[]) ∧
        ∀x l. UNZIP (x::l) = (FST x::FST (UNZIP l),SND x::SND (UNZIP l))
   
   [ZIP_def]  Definition
      
      ⊢ (∀l2. ZIP ([],l2) = []) ∧ (∀l1. ZIP (l1,[]) = []) ∧
        ∀x1 l1 x2 l2. ZIP (x1::l1,x2::l2) = (x1,x2)::ZIP (l1,l2)
   
   [dropWhile_def]  Definition
      
      ⊢ (∀P. dropWhile P [] = []) ∧
        ∀P h t. dropWhile P (h::t) = if P h then dropWhile P t else h::t
   
   [isPREFIX]  Definition
      
      ⊢ (∀l. [] ≼ l ⇔ T) ∧
        ∀h t l. h::t ≼ l ⇔ case l of [] => F | h'::t' => h = h' ∧ t ≼ t'
   
   [list_TY_DEF]  Definition
      
      ⊢ ∃rep.
            TYPE_DEFINITION
              (λa0'.
                   ∀ $var$('list').
                       (∀a0'.
                            a0' =
                            ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM) ∨
                            (∃a0 a1.
                                 a0' =
                                 (λa0 a1.
                                      ind_type$CONSTR (SUC 0) a0
                                        (ind_type$FCONS a1
                                           (λn. ind_type$BOTTOM))) a0 a1 ∧
                                 $var$('list') a1) ⇒
                            $var$('list') a0') ⇒
                       $var$('list') a0') rep
   
   [list_case_def]  Definition
      
      ⊢ (∀v f. list_CASE [] v f = v) ∧
        ∀a0 a1 v f. list_CASE (a0::a1) v f = f a0 a1
   
   [list_size_def]  Definition
      
      ⊢ (∀f. list_size f [] = 0) ∧
        ∀f a0 a1. list_size f (a0::a1) = 1 + (f a0 + list_size f a1)
   
   [nub_def]  Definition
      
      ⊢ nub [] = [] ∧
        ∀x l. nub (x::l) = if MEM x l then nub l else x::nub l
   
   [oEL_def]  Definition
      
      ⊢ (∀n. oEL n [] = NONE) ∧
        ∀n x xs. oEL n (x::xs) = if n = 0 then SOME x else oEL (n − 1) xs
   
   [oHD_def]  Definition
      
      ⊢ ∀l. oHD l = case l of [] => NONE | h::v1 => SOME h
   
   [splitAtPki_def]  Definition
      
      ⊢ (∀P k. splitAtPki P k [] = k [] []) ∧
        ∀P k h t.
            splitAtPki P k (h::t) =
            if P 0 h then k [] (h::t)
            else splitAtPki (P ∘ SUC) (λp s. k (h::p) s) t
   
   [ALL_DISTINCT_APPEND]  Theorem
      
      ⊢ ∀l1 l2.
            ALL_DISTINCT (l1 ⧺ l2) ⇔
            ALL_DISTINCT l1 ∧ ALL_DISTINCT l2 ∧ ∀e. MEM e l1 ⇒ ¬MEM e l2
   
   [ALL_DISTINCT_CARD_LIST_TO_SET]  Theorem
      
      ⊢ ∀ls. ALL_DISTINCT ls ⇒ CARD (set ls) = LENGTH ls
   
   [ALL_DISTINCT_DROP]  Theorem
      
      ⊢ ∀ls n. ALL_DISTINCT ls ⇒ ALL_DISTINCT (DROP n ls)
   
   [ALL_DISTINCT_EL_IMP]  Theorem
      
      ⊢ ∀l n1 n2.
            ALL_DISTINCT l ∧ n1 < LENGTH l ∧ n2 < LENGTH l ⇒
            (EL n1 l = EL n2 l ⇔ n1 = n2)
   
   [ALL_DISTINCT_FILTER]  Theorem
      
      ⊢ ∀l. ALL_DISTINCT l ⇔ ∀x. MEM x l ⇒ FILTER ($= x) l = [x]
   
   [ALL_DISTINCT_FILTER_EL_IMP]  Theorem
      
      ⊢ ∀P l n1 n2.
            ALL_DISTINCT (FILTER P l) ∧ n1 < LENGTH l ∧ n2 < LENGTH l ∧
            P (EL n1 l) ∧ EL n1 l = EL n2 l ⇒
            n1 = n2
   
   [ALL_DISTINCT_FLAT_REVERSE]  Theorem
      
      ⊢ ∀xs. ALL_DISTINCT (FLAT (REVERSE xs)) ⇔ ALL_DISTINCT (FLAT xs)
   
   [ALL_DISTINCT_GENLIST]  Theorem
      
      ⊢ ALL_DISTINCT (GENLIST f n) ⇔
        ∀m1 m2. m1 < n ∧ m2 < n ∧ f m1 = f m2 ⇒ m1 = m2
   
   [ALL_DISTINCT_MAP]  Theorem
      
      ⊢ ∀f ls. ALL_DISTINCT (MAP f ls) ⇒ ALL_DISTINCT ls
   
   [ALL_DISTINCT_MAP_INJ]  Theorem
      
      ⊢ ∀ls f.
            (∀x y. MEM x ls ∧ MEM y ls ∧ f x = f y ⇒ x = y) ∧
            ALL_DISTINCT ls ⇒
            ALL_DISTINCT (MAP f ls)
   
   [ALL_DISTINCT_REVERSE]  Theorem
      
      ⊢ ∀l. ALL_DISTINCT (REVERSE l) ⇔ ALL_DISTINCT l
   
   [ALL_DISTINCT_SET_TO_LIST]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ALL_DISTINCT (SET_TO_LIST s)
   
   [ALL_DISTINCT_SING]  Theorem
      
      ⊢ ∀x. ALL_DISTINCT [x]
   
   [ALL_DISTINCT_SNOC]  Theorem
      
      ⊢ ∀x l. ALL_DISTINCT (SNOC x l) ⇔ ¬MEM x l ∧ ALL_DISTINCT l
   
   [ALL_DISTINCT_ZIP]  Theorem
      
      ⊢ ∀l1 l2.
            ALL_DISTINCT l1 ∧ LENGTH l1 = LENGTH l2 ⇒
            ALL_DISTINCT (ZIP (l1,l2))
   
   [ALL_DISTINCT_ZIP_SWAP]  Theorem
      
      ⊢ ∀l1 l2.
            ALL_DISTINCT (ZIP (l1,l2)) ∧ LENGTH l1 = LENGTH l2 ⇒
            ALL_DISTINCT (ZIP (l2,l1))
   
   [APPEND_11]  Theorem
      
      ⊢ (∀l1 l2 l3. l1 ⧺ l2 = l1 ⧺ l3 ⇔ l2 = l3) ∧
        ∀l1 l2 l3. l2 ⧺ l1 = l3 ⧺ l1 ⇔ l2 = l3
   
   [APPEND_11_LENGTH]  Theorem
      
      ⊢ (∀l1 l2 l1' l2'.
             LENGTH l1 = LENGTH l1' ⇒
             (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')) ∧
        ∀l1 l2 l1' l2'.
            LENGTH l2 = LENGTH l2' ⇒
            (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')
   
   [APPEND_ASSOC]  Theorem
      
      ⊢ ∀l1 l2 l3. l1 ⧺ (l2 ⧺ l3) = l1 ⧺ l2 ⧺ l3
   
   [APPEND_EQ_APPEND]  Theorem
      
      ⊢ l1 ⧺ l2 = m1 ⧺ m2 ⇔
        (∃l. l1 = m1 ⧺ l ∧ m2 = l ⧺ l2) ∨ ∃l. m1 = l1 ⧺ l ∧ l2 = l ⧺ m2
   
   [APPEND_EQ_APPEND_MID]  Theorem
      
      ⊢ l1 ⧺ [e] ⧺ l2 = m1 ⧺ m2 ⇔
        (∃l. m1 = l1 ⧺ [e] ⧺ l ∧ l2 = l ⧺ m2) ∨
        ∃l. l1 = m1 ⧺ l ∧ m2 = l ⧺ [e] ⧺ l2
   
   [APPEND_EQ_CONS]  Theorem
      
      ⊢ l1 ⧺ l2 = h::t ⇔
        l1 = [] ∧ l2 = h::t ∨ ∃lt. l1 = h::lt ∧ t = lt ⧺ l2
   
   [APPEND_EQ_SELF]  Theorem
      
      ⊢ (∀l1 l2. l1 ⧺ l2 = l1 ⇔ l2 = []) ∧
        (∀l1 l2. l1 ⧺ l2 = l2 ⇔ l1 = []) ∧
        (∀l1 l2. l1 = l1 ⧺ l2 ⇔ l2 = []) ∧ ∀l1 l2. l2 = l1 ⧺ l2 ⇔ l1 = []
   
   [APPEND_EQ_SING]  Theorem
      
      ⊢ l1 ⧺ l2 = [e] ⇔ l1 = [e] ∧ l2 = [] ∨ l1 = [] ∧ l2 = [e]
   
   [APPEND_FRONT_LAST]  Theorem
      
      ⊢ ∀l. l ≠ [] ⇒ FRONT l ⧺ [LAST l] = l
   
   [APPEND_LENGTH_EQ]  Theorem
      
      ⊢ ∀l1 l1'.
            LENGTH l1 = LENGTH l1' ⇒
            ∀l2 l2'.
                LENGTH l2 = LENGTH l2' ⇒
                (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')
   
   [APPEND_NIL]  Theorem
      
      ⊢ ∀l. l ⧺ [] = l
   
   [APPEND_SNOC]  Theorem
      
      ⊢ ∀l1 x l2. l1 ⧺ SNOC x l2 = SNOC x (l1 ⧺ l2)
   
   [APPEND_eq_NIL]  Theorem
      
      ⊢ (∀l1 l2. [] = l1 ⧺ l2 ⇔ l1 = [] ∧ l2 = []) ∧
        ∀l1 l2. l1 ⧺ l2 = [] ⇔ l1 = [] ∧ l2 = []
   
   [BIGUNION_IMAGE_set_SUBSET]  Theorem
      
      ⊢ BIGUNION (IMAGE f (set ls)) ⊆ s ⇔ ∀x. MEM x ls ⇒ f x ⊆ s
   
   [CARD_LIST_TO_SET]  Theorem
      
      ⊢ CARD (set ls) ≤ LENGTH ls
   
   [CARD_LIST_TO_SET_ALL_DISTINCT]  Theorem
      
      ⊢ ∀ls. CARD (set ls) = LENGTH ls ⇒ ALL_DISTINCT ls
   
   [CONS]  Theorem
      
      ⊢ ∀l. ¬NULL l ⇒ HD l::TL l = l
   
   [CONS_11]  Theorem
      
      ⊢ ∀a0 a1 a0' a1'. a0::a1 = a0'::a1' ⇔ a0 = a0' ∧ a1 = a1'
   
   [CONS_ACYCLIC]  Theorem
      
      ⊢ ∀l x. l ≠ x::l ∧ x::l ≠ l
   
   [DISJOINT_GENLIST_PLUS]  Theorem
      
      ⊢ DISJOINT x (set (GENLIST ($+ n) (a + b))) ⇒
        DISJOINT x (set (GENLIST ($+ n) a)) ∧
        DISJOINT x (set (GENLIST ($+ (n + a)) b))
   
   [DROP_0]  Theorem
      
      ⊢ DROP 0 l = l
   
   [DROP_GENLIST]  Theorem
      
      ⊢ DROP n (GENLIST f m) = GENLIST (f ∘ $+ n) (m − n)
   
   [DROP_LENGTH_TOO_LONG]  Theorem
      
      ⊢ ∀l n. LENGTH l ≤ n ⇒ DROP n l = []
   
   [DROP_NIL]  Theorem
      
      ⊢ ∀ls n. DROP n ls = [] ⇔ n ≥ LENGTH ls
   
   [DROP_compute]  Theorem
      
      ⊢ (∀l. DROP 0 l = l) ∧ (∀n. DROP (NUMERAL (BIT1 n)) [] = []) ∧
        (∀n. DROP (NUMERAL (BIT2 n)) [] = []) ∧
        (∀n h t.
             DROP (NUMERAL (BIT1 n)) (h::t) = DROP (NUMERAL (BIT1 n) − 1) t) ∧
        ∀n h t. DROP (NUMERAL (BIT2 n)) (h::t) = DROP (NUMERAL (BIT1 n)) t
   
   [DROP_cons]  Theorem
      
      ⊢ 0 < n ⇒ DROP n (x::xs) = DROP (n − 1) xs
   
   [DROP_nil]  Theorem
      
      ⊢ ∀n. DROP n [] = []
   
   [DROP_splitAtPki]  Theorem
      
      ⊢ DROP n l = splitAtPki (K ∘ $= n) (K I) l
   
   [EL_ALL_DISTINCT_EL_EQ]  Theorem
      
      ⊢ ∀l.
            ALL_DISTINCT l ⇔
            ∀n1 n2.
                n1 < LENGTH l ∧ n2 < LENGTH l ⇒
                (EL n1 l = EL n2 l ⇔ n1 = n2)
   
   [EL_APPEND_EQN]  Theorem
      
      ⊢ ∀l1 l2 n.
            EL n (l1 ⧺ l2) =
            if n < LENGTH l1 then EL n l1 else EL (n − LENGTH l1) l2
   
   [EL_DROP]  Theorem
      
      ⊢ ∀m n l. m + n < LENGTH l ⇒ EL m (DROP n l) = EL (m + n) l
   
   [EL_GENLIST]  Theorem
      
      ⊢ ∀f n x. x < n ⇒ EL x (GENLIST f n) = f x
   
   [EL_LENGTH_SNOC]  Theorem
      
      ⊢ ∀l x. EL (LENGTH l) (SNOC x l) = x
   
   [EL_LENGTH_dropWhile_REVERSE]  Theorem
      
      ⊢ ∀P ls k.
            LENGTH (dropWhile P (REVERSE ls)) ≤ k ∧ k < LENGTH ls ⇒
            P (EL k ls)
   
   [EL_LUPDATE]  Theorem
      
      ⊢ ∀ys x i k.
            EL i (LUPDATE x k ys) =
            if i = k ∧ k < LENGTH ys then x else EL i ys
   
   [EL_MAP]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ ∀f. EL n (MAP f l) = f (EL n l)
   
   [EL_MAP2]  Theorem
      
      ⊢ ∀ts tt n.
            n < MIN (LENGTH ts) (LENGTH tt) ⇒
            EL n (MAP2 f ts tt) = f (EL n ts) (EL n tt)
   
   [EL_REVERSE]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ EL n (REVERSE l) = EL (PRE (LENGTH l − n)) l
   
   [EL_SNOC]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ ∀x. EL n (SNOC x l) = EL n l
   
   [EL_TAKE]  Theorem
      
      ⊢ ∀n x l. x < n ⇒ EL x (TAKE n l) = EL x l
   
   [EL_ZIP]  Theorem
      
      ⊢ ∀l1 l2 n.
            LENGTH l1 = LENGTH l2 ∧ n < LENGTH l1 ⇒
            EL n (ZIP (l1,l2)) = (EL n l1,EL n l2)
   
   [EL_compute]  Theorem
      
      ⊢ ∀n. EL n l = if n = 0 then HD l else EL (PRE n) (TL l)
   
   [EL_restricted]  Theorem
      
      ⊢ EL 0 = HD ∧ EL (SUC n) (l::ls) = EL n ls
   
   [EL_simp]  Theorem
      
      ⊢ EL (NUMERAL (BIT1 n)) l = EL (PRE (NUMERAL (BIT1 n))) (TL l) ∧
        EL (NUMERAL (BIT2 n)) l = EL (NUMERAL (BIT1 n)) (TL l)
   
   [EL_simp_restricted]  Theorem
      
      ⊢ EL (NUMERAL (BIT1 n)) (l::ls) = EL (PRE (NUMERAL (BIT1 n))) ls ∧
        EL (NUMERAL (BIT2 n)) (l::ls) = EL (NUMERAL (BIT1 n)) ls
   
   [EQ_LIST]  Theorem
      
      ⊢ ∀h1 h2. h1 = h2 ⇒ ∀l1 l2. l1 = l2 ⇒ h1::l1 = h2::l2
   
   [EVERY2_EVERY]  Theorem
      
      ⊢ ∀l1 l2 f.
            LIST_REL f l1 l2 ⇔
            LENGTH l1 = LENGTH l2 ∧ EVERY (UNCURRY f) (ZIP (l1,l2))
   
   [EVERY2_LENGTH]  Theorem
      
      ⊢ ∀P l1 l2. LIST_REL P l1 l2 ⇒ LENGTH l1 = LENGTH l2
   
   [EVERY2_LUPDATE_same]  Theorem
      
      ⊢ ∀P l1 l2 v1 v2 n.
            P v1 v2 ∧ LIST_REL P l1 l2 ⇒
            LIST_REL P (LUPDATE v1 n l1) (LUPDATE v2 n l2)
   
   [EVERY2_MAP]  Theorem
      
      ⊢ (LIST_REL P (MAP f l1) l2 ⇔ LIST_REL (λx y. P (f x) y) l1 l2) ∧
        (LIST_REL Q l1 (MAP g l2) ⇔ LIST_REL (λx y. Q x (g y)) l1 l2)
   
   [EVERY2_MEM_MONO]  Theorem
      
      ⊢ ∀P Q l1 l2.
            (∀x. MEM x (ZIP (l1,l2)) ∧ UNCURRY P x ⇒ UNCURRY Q x) ∧
            LIST_REL P l1 l2 ⇒
            LIST_REL Q l1 l2
   
   [EVERY2_REVERSE]  Theorem
      
      ⊢ ∀R l1 l2. LIST_REL R l1 l2 ⇒ LIST_REL R (REVERSE l1) (REVERSE l2)
   
   [EVERY2_THM]  Theorem
      
      ⊢ (∀P ys. LIST_REL P [] ys ⇔ ys = []) ∧
        (∀P yys x xs.
             LIST_REL P (x::xs) yys ⇔
             ∃y ys. yys = y::ys ∧ P x y ∧ LIST_REL P xs ys) ∧
        (∀P xs. LIST_REL P xs [] ⇔ xs = []) ∧
        ∀P xxs y ys.
            LIST_REL P xxs (y::ys) ⇔
            ∃x xs. xxs = x::xs ∧ P x y ∧ LIST_REL P xs ys
   
   [EVERY2_cong]  Theorem
      
      ⊢ ∀l1 l1' l2 l2' P P'.
            l1 = l1' ∧ l2 = l2' ∧
            (∀x y. MEM x l1' ∧ MEM y l2' ⇒ (P x y ⇔ P' x y)) ⇒
            (LIST_REL P l1 l2 ⇔ LIST_REL P' l1' l2')
   
   [EVERY2_mono]  Theorem
      
      ⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ LIST_REL R1 l1 l2 ⇒ LIST_REL R2 l1 l2
   
   [EVERY2_refl]  Theorem
      
      ⊢ (∀x. MEM x ls ⇒ R x x) ⇒ LIST_REL R ls ls
   
   [EVERY2_sym]  Theorem
      
      ⊢ (∀x y. R1 x y ⇒ R2 y x) ⇒ ∀x y. LIST_REL R1 x y ⇒ LIST_REL R2 y x
   
   [EVERY2_trans]  Theorem
      
      ⊢ (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
        ∀x y z. LIST_REL R x y ∧ LIST_REL R y z ⇒ LIST_REL R x z
   
   [EVERY_APPEND]  Theorem
      
      ⊢ ∀P l1 l2. EVERY P (l1 ⧺ l2) ⇔ EVERY P l1 ∧ EVERY P l2
   
   [EVERY_CONG]  Theorem
      
      ⊢ ∀l1 l2 P P'.
            l1 = l2 ∧ (∀x. MEM x l2 ⇒ (P x ⇔ P' x)) ⇒
            (EVERY P l1 ⇔ EVERY P' l2)
   
   [EVERY_CONJ]  Theorem
      
      ⊢ ∀P Q l. EVERY (λx. P x ∧ Q x) l ⇔ EVERY P l ∧ EVERY Q l
   
   [EVERY_EL]  Theorem
      
      ⊢ ∀l P. EVERY P l ⇔ ∀n. n < LENGTH l ⇒ P (EL n l)
   
   [EVERY_FILTER]  Theorem
      
      ⊢ ∀P1 P2 l. EVERY P1 (FILTER P2 l) ⇔ EVERY (λx. P2 x ⇒ P1 x) l
   
   [EVERY_FILTER_IMP]  Theorem
      
      ⊢ ∀P1 P2 l. EVERY P1 l ⇒ EVERY P1 (FILTER P2 l)
   
   [EVERY_FLAT]  Theorem
      
      ⊢ EVERY P (FLAT ls) ⇔ EVERY (EVERY P) ls
   
   [EVERY_GENLIST]  Theorem
      
      ⊢ ∀n. EVERY P (GENLIST f n) ⇔ ∀i. i < n ⇒ P (f i)
   
   [EVERY_MAP]  Theorem
      
      ⊢ ∀P f l. EVERY P (MAP f l) ⇔ EVERY (λx. P (f x)) l
   
   [EVERY_MEM]  Theorem
      
      ⊢ ∀P l. EVERY P l ⇔ ∀e. MEM e l ⇒ P e
   
   [EVERY_MEM_MONO]  Theorem
      
      ⊢ ∀P Q l. (∀x. MEM x l ∧ P x ⇒ Q x) ∧ EVERY P l ⇒ EVERY Q l
   
   [EVERY_MONOTONIC]  Theorem
      
      ⊢ ∀P Q. (∀x. P x ⇒ Q x) ⇒ ∀l. EVERY P l ⇒ EVERY Q l
   
   [EVERY_NOT_EXISTS]  Theorem
      
      ⊢ ∀P l. EVERY P l ⇔ ¬EXISTS (λx. ¬P x) l
   
   [EVERY_SIMP]  Theorem
      
      ⊢ ∀c l. EVERY (λx. c) l ⇔ l = [] ∨ c
   
   [EVERY_SNOC]  Theorem
      
      ⊢ ∀P x l. EVERY P (SNOC x l) ⇔ EVERY P l ∧ P x
   
   [EXISTS_APPEND]  Theorem
      
      ⊢ ∀P l1 l2. EXISTS P (l1 ⧺ l2) ⇔ EXISTS P l1 ∨ EXISTS P l2
   
   [EXISTS_CONG]  Theorem
      
      ⊢ ∀l1 l2 P P'.
            l1 = l2 ∧ (∀x. MEM x l2 ⇒ (P x ⇔ P' x)) ⇒
            (EXISTS P l1 ⇔ EXISTS P' l2)
   
   [EXISTS_GENLIST]  Theorem
      
      ⊢ ∀n. EXISTS P (GENLIST f n) ⇔ ∃i. i < n ∧ P (f i)
   
   [EXISTS_LIST]  Theorem
      
      ⊢ (∃l. P l) ⇔ P [] ∨ ∃h t. P (h::t)
   
   [EXISTS_LIST_EQ_MAP]  Theorem
      
      ⊢ ∀ls f. EVERY (λx. ∃y. x = f y) ls ⇒ ∃l. ls = MAP f l
   
   [EXISTS_MAP]  Theorem
      
      ⊢ ∀P f l. EXISTS P (MAP f l) ⇔ EXISTS (λx. P (f x)) l
   
   [EXISTS_MEM]  Theorem
      
      ⊢ ∀P l. EXISTS P l ⇔ ∃e. MEM e l ∧ P e
   
   [EXISTS_NOT_EVERY]  Theorem
      
      ⊢ ∀P l. EXISTS P l ⇔ ¬EVERY (λx. ¬P x) l
   
   [EXISTS_SIMP]  Theorem
      
      ⊢ ∀c l. EXISTS (λx. c) l ⇔ l ≠ [] ∧ c
   
   [EXISTS_SNOC]  Theorem
      
      ⊢ ∀P x l. EXISTS P (SNOC x l) ⇔ P x ∨ EXISTS P l
   
   [FILTER_ALL_DISTINCT]  Theorem
      
      ⊢ ∀P l. ALL_DISTINCT l ⇒ ALL_DISTINCT (FILTER P l)
   
   [FILTER_APPEND_DISTRIB]  Theorem
      
      ⊢ ∀P L M. FILTER P (L ⧺ M) = FILTER P L ⧺ FILTER P M
   
   [FILTER_COND_REWRITE]  Theorem
      
      ⊢ FILTER P [] = [] ∧ (∀h. P h ⇒ FILTER P (h::l) = h::FILTER P l) ∧
        ∀h. ¬P h ⇒ FILTER P (h::l) = FILTER P l
   
   [FILTER_EQ_APPEND]  Theorem
      
      ⊢ ∀P l l1 l2.
            FILTER P l = l1 ⧺ l2 ⇔
            ∃l3 l4. l = l3 ⧺ l4 ∧ FILTER P l3 = l1 ∧ FILTER P l4 = l2
   
   [FILTER_EQ_CONS]  Theorem
      
      ⊢ ∀P l h lr.
            FILTER P l = h::lr ⇔
            ∃l1 l2.
                l = l1 ⧺ [h] ⧺ l2 ∧ FILTER P l1 = [] ∧ FILTER P l2 = lr ∧
                P h
   
   [FILTER_EQ_ID]  Theorem
      
      ⊢ ∀P l. FILTER P l = l ⇔ EVERY P l
   
   [FILTER_EQ_NIL]  Theorem
      
      ⊢ ∀P l. FILTER P l = [] ⇔ EVERY (λx. ¬P x) l
   
   [FILTER_F]  Theorem
      
      ⊢ ∀xs. FILTER (λx. F) xs = []
   
   [FILTER_NEQ_ID]  Theorem
      
      ⊢ ∀P l. FILTER P l ≠ l ⇔ ∃x. MEM x l ∧ ¬P x
   
   [FILTER_NEQ_NIL]  Theorem
      
      ⊢ ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x
   
   [FILTER_REVERSE]  Theorem
      
      ⊢ ∀l P. FILTER P (REVERSE l) = REVERSE (FILTER P l)
   
   [FILTER_T]  Theorem
      
      ⊢ ∀xs. FILTER (λx. T) xs = xs
   
   [FINITE_LIST_TO_SET]  Theorem
      
      ⊢ ∀l. FINITE (set l)
   
   [FLAT_APPEND]  Theorem
      
      ⊢ ∀l1 l2. FLAT (l1 ⧺ l2) = FLAT l1 ⧺ FLAT l2
   
   [FLAT_EQ_NIL]  Theorem
      
      ⊢ ∀ls. FLAT ls = [] ⇔ EVERY ($= []) ls
   
   [FLAT_compute]  Theorem
      
      ⊢ FLAT [] = [] ∧ FLAT ([]::t) = FLAT t ∧
        FLAT ((h::t1)::t2) = h::FLAT (t1::t2)
   
   [FOLDL2_FOLDL]  Theorem
      
      ⊢ ∀l1 l2.
            LENGTH l1 = LENGTH l2 ⇒
            ∀f a.
                FOLDL2 f a l1 l2 =
                FOLDL (λa. UNCURRY (f a)) a (ZIP (l1,l2))
   
   [FOLDL2_cong]  Theorem
      
      ⊢ ∀l1 l1' l2 l2' a a' f f'.
            l1 = l1' ∧ l2 = l2' ∧ a = a' ∧
            (∀z b c. MEM b l1' ∧ MEM c l2' ⇒ f z b c = f' z b c) ⇒
            FOLDL2 f a l1 l2 = FOLDL2 f' a' l1' l2'
   
   [FOLDL2_def]  Theorem
      
      ⊢ (∀f cs c bs b a.
             FOLDL2 f a (b::bs) (c::cs) = FOLDL2 f (f a b c) bs cs) ∧
        (∀f cs a. FOLDL2 f a [] cs = a) ∧
        ∀v7 v6 f a. FOLDL2 f a (v6::v7) [] = a
   
   [FOLDL2_ind]  Theorem
      
      ⊢ ∀P.
            (∀f a b bs c cs. P f (f a b c) bs cs ⇒ P f a (b::bs) (c::cs)) ∧
            (∀f a cs. P f a [] cs) ∧ (∀f a v6 v7. P f a (v6::v7) []) ⇒
            ∀v v1 v2 v3. P v v1 v2 v3
   
   [FOLDL_CONG]  Theorem
      
      ⊢ ∀l l' b b' f f'.
            l = l' ∧ b = b' ∧ (∀x a. MEM x l' ⇒ f a x = f' a x) ⇒
            FOLDL f b l = FOLDL f' b' l'
   
   [FOLDL_EQ_FOLDR]  Theorem
      
      ⊢ ∀f l e. ASSOC f ∧ COMM f ⇒ FOLDL f e l = FOLDR f e l
   
   [FOLDL_SNOC]  Theorem
      
      ⊢ ∀f e x l. FOLDL f e (SNOC x l) = f (FOLDL f e l) x
   
   [FOLDL_UNION_BIGUNION]  Theorem
      
      ⊢ ∀f ls s.
            FOLDL (λs x. s ∪ f x) s ls = s ∪ BIGUNION (IMAGE f (set ls))
   
   [FOLDL_UNION_BIGUNION_paired]  Theorem
      
      ⊢ ∀f ls s.
            FOLDL (λs (x,y). s ∪ f x y) s ls =
            s ∪ BIGUNION (IMAGE (UNCURRY f) (set ls))
   
   [FOLDL_ZIP_SAME]  Theorem
      
      ⊢ ∀ls f e. FOLDL f e (ZIP (ls,ls)) = FOLDL (λx y. f x (y,y)) e ls
   
   [FOLDR_CONG]  Theorem
      
      ⊢ ∀l l' b b' f f'.
            l = l' ∧ b = b' ∧ (∀x a. MEM x l' ⇒ f x a = f' x a) ⇒
            FOLDR f b l = FOLDR f' b' l'
   
   [FOLDR_CONS]  Theorem
      
      ⊢ ∀f ls a. FOLDR (λx y. f x::y) a ls = MAP f ls ⧺ a
   
   [FORALL_LIST]  Theorem
      
      ⊢ (∀l. P l) ⇔ P [] ∧ ∀h t. P (h::t)
   
   [FRONT_CONS]  Theorem
      
      ⊢ (∀x. FRONT [x] = []) ∧ ∀x y z. FRONT (x::y::z) = x::FRONT (y::z)
   
   [FRONT_CONS_EQ_NIL]  Theorem
      
      ⊢ (∀x xs. FRONT (x::xs) = [] ⇔ xs = []) ∧
        (∀x xs. [] = FRONT (x::xs) ⇔ xs = []) ∧
        ∀x xs. NULL (FRONT (x::xs)) ⇔ NULL xs
   
   [FRONT_SNOC]  Theorem
      
      ⊢ ∀x l. FRONT (SNOC x l) = l
   
   [GENLIST_APPEND]  Theorem
      
      ⊢ ∀f a b. GENLIST f (a + b) = GENLIST f b ⧺ GENLIST (λt. f (t + b)) a
   
   [GENLIST_AUX_compute]  Theorem
      
      ⊢ (∀f l. GENLIST_AUX f 0 l = l) ∧
        (∀f n l.
             GENLIST_AUX f (NUMERAL (BIT1 n)) l =
             GENLIST_AUX f (NUMERAL (BIT1 n) − 1)
               (f (NUMERAL (BIT1 n) − 1)::l)) ∧
        ∀f n l.
            GENLIST_AUX f (NUMERAL (BIT2 n)) l =
            GENLIST_AUX f (NUMERAL (BIT1 n)) (f (NUMERAL (BIT1 n))::l)
   
   [GENLIST_CONS]  Theorem
      
      ⊢ GENLIST f (SUC n) = f 0::GENLIST (f ∘ SUC) n
   
   [GENLIST_EL]  Theorem
      
      ⊢ ∀ls f n.
            n = LENGTH ls ∧ (∀i. i < n ⇒ f i = EL i ls) ⇒ GENLIST f n = ls
   
   [GENLIST_EL_MAP]  Theorem
      
      ⊢ ∀f ls. GENLIST (λn. f (EL n ls)) (LENGTH ls) = MAP f ls
   
   [GENLIST_FUN_EQ]  Theorem
      
      ⊢ ∀n f g. GENLIST f n = GENLIST g n ⇔ ∀x. x < n ⇒ f x = g x
   
   [GENLIST_GENLIST_AUX]  Theorem
      
      ⊢ ∀n. GENLIST f n = GENLIST_AUX f n []
   
   [GENLIST_ID]  Theorem
      
      ⊢ ∀x. GENLIST (λi. EL i x) (LENGTH x) = x
   
   [GENLIST_NUMERALS]  Theorem
      
      ⊢ GENLIST f 0 = [] ∧
        GENLIST f (NUMERAL n) = GENLIST_AUX f (NUMERAL n) []
   
   [GENLIST_PLUS_APPEND]  Theorem
      
      ⊢ GENLIST ($+ a) n1 ⧺ GENLIST ($+ (n1 + a)) n2 =
        GENLIST ($+ a) (n1 + n2)
   
   [HD_DROP]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ HD (DROP n l) = EL n l
   
   [HD_GENLIST]  Theorem
      
      ⊢ HD (GENLIST f (SUC n)) = f 0
   
   [HD_GENLIST_COR]  Theorem
      
      ⊢ ∀n f. 0 < n ⇒ HD (GENLIST f n) = f 0
   
   [HD_REVERSE]  Theorem
      
      ⊢ ∀x. x ≠ [] ⇒ HD (REVERSE x) = LAST x
   
   [HD_dropWhile]  Theorem
      
      ⊢ ∀P ls. EXISTS ($~ ∘ P) ls ⇒ ¬P (HD (dropWhile P ls))
   
   [IMAGE_EL_count_LENGTH]  Theorem
      
      ⊢ ∀f ls.
            IMAGE (λn. f (EL n ls)) (count (LENGTH ls)) = IMAGE f (set ls)
   
   [IMP_EVERY_LUPDATE]  Theorem
      
      ⊢ ∀xs h i. P h ∧ EVERY P xs ⇒ EVERY P (LUPDATE h i xs)
   
   [INFINITE_LIST_UNIV]  Theorem
      
      ⊢ INFINITE 𝕌(:α list)
   
   [INJ_MAP_EQ]  Theorem
      
      ⊢ ∀f l1 l2.
            INJ f (set l1 ∪ set l2) 𝕌(:β) ∧ MAP f l1 = MAP f l2 ⇒ l1 = l2
   
   [INJ_MAP_EQ_IFF]  Theorem
      
      ⊢ ∀f l1 l2.
            INJ f (set l1 ∪ set l2) 𝕌(:β) ⇒ (MAP f l1 = MAP f l2 ⇔ l1 = l2)
   
   [ITSET_eq_FOLDL_SET_TO_LIST]  Theorem
      
      ⊢ ∀s.
            FINITE s ⇒
            ∀f a. ITSET f s a = FOLDL (combin$C f) a (SET_TO_LIST s)
   
   [LAST_APPEND_CONS]  Theorem
      
      ⊢ ∀h l1 l2. LAST (l1 ⧺ h::l2) = LAST (h::l2)
   
   [LAST_CONS]  Theorem
      
      ⊢ (∀x. LAST [x] = x) ∧ ∀x y z. LAST (x::y::z) = LAST (y::z)
   
   [LAST_CONS_cond]  Theorem
      
      ⊢ LAST (h::t) = if t = [] then h else LAST t
   
   [LAST_EL]  Theorem
      
      ⊢ ∀ls. ls ≠ [] ⇒ LAST ls = EL (PRE (LENGTH ls)) ls
   
   [LAST_MAP]  Theorem
      
      ⊢ ∀l f. l ≠ [] ⇒ LAST (MAP f l) = f (LAST l)
   
   [LAST_REVERSE]  Theorem
      
      ⊢ ∀ls. ls ≠ [] ⇒ LAST (REVERSE ls) = HD ls
   
   [LAST_SNOC]  Theorem
      
      ⊢ ∀x l. LAST (SNOC x l) = x
   
   [LAST_compute]  Theorem
      
      ⊢ (∀x. LAST [x] = x) ∧ ∀h1 h2 t. LAST (h1::h2::t) = LAST (h2::t)
   
   [LENGTH_APPEND]  Theorem
      
      ⊢ ∀l1 l2. LENGTH (l1 ⧺ l2) = LENGTH l1 + LENGTH l2
   
   [LENGTH_CONS]  Theorem
      
      ⊢ ∀l n. LENGTH l = SUC n ⇔ ∃h l'. LENGTH l' = n ∧ l = h::l'
   
   [LENGTH_DROP]  Theorem
      
      ⊢ ∀n l. LENGTH (DROP n l) = LENGTH l − n
   
   [LENGTH_EQ_CONS]  Theorem
      
      ⊢ ∀P n.
            (∀l. LENGTH l = SUC n ⇒ P l) ⇔
            ∀l. LENGTH l = n ⇒ (λl. ∀x. P (x::l)) l
   
   [LENGTH_EQ_NIL]  Theorem
      
      ⊢ ∀P. (∀l. LENGTH l = 0 ⇒ P l) ⇔ P []
   
   [LENGTH_EQ_NUM]  Theorem
      
      ⊢ (∀l. LENGTH l = 0 ⇔ l = []) ∧
        (∀l n. LENGTH l = SUC n ⇔ ∃h l'. LENGTH l' = n ∧ l = h::l') ∧
        ∀l n1 n2.
            LENGTH l = n1 + n2 ⇔
            ∃l1 l2. LENGTH l1 = n1 ∧ LENGTH l2 = n2 ∧ l = l1 ⧺ l2
   
   [LENGTH_EQ_NUM_compute]  Theorem
      
      ⊢ (∀l. LENGTH l = 0 ⇔ l = []) ∧
        (∀l n.
             LENGTH l = NUMERAL (BIT1 n) ⇔
             ∃h l'. LENGTH l' = NUMERAL (BIT1 n) − 1 ∧ l = h::l') ∧
        (∀l n.
             LENGTH l = NUMERAL (BIT2 n) ⇔
             ∃h l'. LENGTH l' = NUMERAL (BIT1 n) ∧ l = h::l') ∧
        ∀l n1 n2.
            LENGTH l = n1 + n2 ⇔
            ∃l1 l2. LENGTH l1 = n1 ∧ LENGTH l2 = n2 ∧ l = l1 ⧺ l2
   
   [LENGTH_EQ_SUM]  Theorem
      
      ⊢ ∀l n1 n2.
            LENGTH l = n1 + n2 ⇔
            ∃l1 l2. LENGTH l1 = n1 ∧ LENGTH l2 = n2 ∧ l = l1 ⧺ l2
   
   [LENGTH_FILTER_LEQ_MONO]  Theorem
      
      ⊢ ∀P Q.
            (∀x. P x ⇒ Q x) ⇒
            ∀ls. LENGTH (FILTER P ls) ≤ LENGTH (FILTER Q ls)
   
   [LENGTH_FRONT_CONS]  Theorem
      
      ⊢ ∀x xs. LENGTH (FRONT (x::xs)) = LENGTH xs
   
   [LENGTH_GENLIST]  Theorem
      
      ⊢ ∀f n. LENGTH (GENLIST f n) = n
   
   [LENGTH_LEN]  Theorem
      
      ⊢ ∀L. LENGTH L = LEN L 0
   
   [LENGTH_LT_SHORTLEX]  Theorem
      
      ⊢ ∀l1 l2. LENGTH l1 < LENGTH l2 ⇒ SHORTLEX R l1 l2
   
   [LENGTH_LUPDATE]  Theorem
      
      ⊢ ∀x n ys. LENGTH (LUPDATE x n ys) = LENGTH ys
   
   [LENGTH_MAP]  Theorem
      
      ⊢ ∀l f. LENGTH (MAP f l) = LENGTH l
   
   [LENGTH_MAP2]  Theorem
      
      ⊢ ∀xs ys. LENGTH (MAP2 f xs ys) = MIN (LENGTH xs) (LENGTH ys)
   
   [LENGTH_NIL]  Theorem
      
      ⊢ ∀l. LENGTH l = 0 ⇔ l = []
   
   [LENGTH_NIL_SYM]  Theorem
      
      ⊢ 0 = LENGTH l ⇔ l = []
   
   [LENGTH_REVERSE]  Theorem
      
      ⊢ ∀l. LENGTH (REVERSE l) = LENGTH l
   
   [LENGTH_SNOC]  Theorem
      
      ⊢ ∀x l. LENGTH (SNOC x l) = SUC (LENGTH l)
   
   [LENGTH_TAKE]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (TAKE n l) = n
   
   [LENGTH_TAKE_EQ]  Theorem
      
      ⊢ LENGTH (TAKE n xs) = if n ≤ LENGTH xs then n else LENGTH xs
   
   [LENGTH_TL]  Theorem
      
      ⊢ ∀l. 0 < LENGTH l ⇒ LENGTH (TL l) = LENGTH l − 1
   
   [LENGTH_UNZIP]  Theorem
      
      ⊢ ∀pl.
            LENGTH (FST (UNZIP pl)) = LENGTH pl ∧
            LENGTH (SND (UNZIP pl)) = LENGTH pl
   
   [LENGTH_ZIP]  Theorem
      
      ⊢ ∀l1 l2.
            LENGTH l1 = LENGTH l2 ⇒
            LENGTH (ZIP (l1,l2)) = LENGTH l1 ∧
            LENGTH (ZIP (l1,l2)) = LENGTH l2
   
   [LENGTH_ZIP_MIN]  Theorem
      
      ⊢ ∀xs ys. LENGTH (ZIP (xs,ys)) = MIN (LENGTH xs) (LENGTH ys)
   
   [LENGTH_dropWhile_LESS_EQ]  Theorem
      
      ⊢ ∀P ls. LENGTH (dropWhile P ls) ≤ LENGTH ls
   
   [LENGTH_o_REVERSE]  Theorem
      
      ⊢ LENGTH ∘ REVERSE = LENGTH ∧ LENGTH ∘ REVERSE ∘ f = LENGTH ∘ f
   
   [LEN_LENGTH_LEM]  Theorem
      
      ⊢ ∀L n. LEN L n = LENGTH L + n
   
   [LIST_APPLY_o]  Theorem
      
      ⊢ [$o] <*> fs <*> gs <*> xs = fs <*> (gs <*> xs)
   
   [LIST_BIND_APPEND]  Theorem
      
      ⊢ LIST_BIND (l1 ⧺ l2) f = LIST_BIND l1 f ⧺ LIST_BIND l2 f
   
   [LIST_BIND_ID]  Theorem
      
      ⊢ LIST_BIND l (λx. x) = FLAT l ∧ LIST_BIND l I = FLAT l
   
   [LIST_BIND_LIST_BIND]  Theorem
      
      ⊢ LIST_BIND (LIST_BIND l g) f =
        LIST_BIND l (combin$C LIST_BIND f ∘ g)
   
   [LIST_BIND_MAP]  Theorem
      
      ⊢ LIST_BIND (MAP f l) g = LIST_BIND l (g ∘ f)
   
   [LIST_BIND_THM]  Theorem
      
      ⊢ LIST_BIND [] f = [] ∧ LIST_BIND (h::t) f = f h ⧺ LIST_BIND t f
   
   [LIST_EQ]  Theorem
      
      ⊢ ∀l1 l2.
            LENGTH l1 = LENGTH l2 ∧ (∀x. x < LENGTH l1 ⇒ EL x l1 = EL x l2) ⇒
            l1 = l2
   
   [LIST_EQ_MAP_PAIR]  Theorem
      
      ⊢ ∀l1 l2. MAP FST l1 = MAP FST l2 ∧ MAP SND l1 = MAP SND l2 ⇒ l1 = l2
   
   [LIST_EQ_REWRITE]  Theorem
      
      ⊢ ∀l1 l2.
            l1 = l2 ⇔
            LENGTH l1 = LENGTH l2 ∧ ∀x. x < LENGTH l1 ⇒ EL x l1 = EL x l2
   
   [LIST_NOT_EQ]  Theorem
      
      ⊢ ∀l1 l2. l1 ≠ l2 ⇒ ∀h1 h2. h1::l1 ≠ h2::l2
   
   [LIST_REL_APPEND]  Theorem
      
      ⊢ LIST_REL R l1 l2 ∧ LIST_REL R l3 l4 ⇔
        LIST_REL R (l1 ⧺ l3) (l2 ⧺ l4) ∧ LENGTH l1 = LENGTH l2 ∧
        LENGTH l3 = LENGTH l4
   
   [LIST_REL_APPEND_EQ]  Theorem
      
      ⊢ LENGTH x1 = LENGTH x2 ⇒
        (LIST_REL R (x1 ⧺ y1) (x2 ⧺ y2) ⇔
         LIST_REL R x1 x2 ∧ LIST_REL R y1 y2)
   
   [LIST_REL_APPEND_IMP]  Theorem
      
      ⊢ ∀xs ys xs1 ys1.
            LIST_REL P (xs ⧺ xs1) (ys ⧺ ys1) ∧ LENGTH xs = LENGTH ys ⇒
            LIST_REL P xs ys ∧ LIST_REL P xs1 ys1
   
   [LIST_REL_APPEND_suff]  Theorem
      
      ⊢ LIST_REL R l1 l2 ∧ LIST_REL R l3 l4 ⇒
        LIST_REL R (l1 ⧺ l3) (l2 ⧺ l4)
   
   [LIST_REL_CONJ]  Theorem
      
      ⊢ LIST_REL (λa b. P a b ∧ Q a b) l1 l2 ⇔
        LIST_REL (λa b. P a b) l1 l2 ∧ LIST_REL (λa b. Q a b) l1 l2
   
   [LIST_REL_CONS1]  Theorem
      
      ⊢ LIST_REL R (h::t) xs ⇔
        ∃h' t'. xs = h'::t' ∧ R h h' ∧ LIST_REL R t t'
   
   [LIST_REL_CONS2]  Theorem
      
      ⊢ LIST_REL R xs (h::t) ⇔
        ∃h' t'. xs = h'::t' ∧ R h' h ∧ LIST_REL R t' t
   
   [LIST_REL_EL_EQN]  Theorem
      
      ⊢ ∀R l1 l2.
            LIST_REL R l1 l2 ⇔
            LENGTH l1 = LENGTH l2 ∧
            ∀n. n < LENGTH l1 ⇒ R (EL n l1) (EL n l2)
   
   [LIST_REL_EVERY_ZIP]  Theorem
      
      ⊢ ∀R l1 l2.
            LIST_REL R l1 l2 ⇔
            LENGTH l1 = LENGTH l2 ∧ EVERY (UNCURRY R) (ZIP (l1,l2))
   
   [LIST_REL_LENGTH]  Theorem
      
      ⊢ ∀x y. LIST_REL R x y ⇒ LENGTH x = LENGTH y
   
   [LIST_REL_MAP1]  Theorem
      
      ⊢ LIST_REL R (MAP f l1) l2 ⇔ LIST_REL (R ∘ f) l1 l2
   
   [LIST_REL_MAP2]  Theorem
      
      ⊢ LIST_REL (λa b. R a b) l1 (MAP f l2) ⇔
        LIST_REL (λa b. R a (f b)) l1 l2
   
   [LIST_REL_MAP_inv_image]  Theorem
      
      ⊢ LIST_REL R (MAP f l1) (MAP f l2) ⇔ LIST_REL (inv_image R f) l1 l2
   
   [LIST_REL_MEM_IMP]  Theorem
      
      ⊢ ∀xs ys P x. LIST_REL P xs ys ∧ MEM x xs ⇒ ∃y. MEM y ys ∧ P x y
   
   [LIST_REL_NIL]  Theorem
      
      ⊢ (LIST_REL R [] y ⇔ y = []) ∧ (LIST_REL R x [] ⇔ x = [])
   
   [LIST_REL_O]  Theorem
      
      ⊢ ∀R1 R2. LIST_REL (R1 ∘ᵣ R2) = LIST_REL R1 ∘ᵣ LIST_REL R2
   
   [LIST_REL_SNOC]  Theorem
      
      ⊢ (LIST_REL R (SNOC x xs) yys ⇔
         ∃y ys. yys = SNOC y ys ∧ LIST_REL R xs ys ∧ R x y) ∧
        (LIST_REL R xxs (SNOC y ys) ⇔
         ∃x xs. xxs = SNOC x xs ∧ LIST_REL R xs ys ∧ R x y)
   
   [LIST_REL_SPLIT1]  Theorem
      
      ⊢ ∀xs1 zs.
            LIST_REL P (xs1 ⧺ xs2) zs ⇔
            ∃ys1 ys2.
                zs = ys1 ⧺ ys2 ∧ LIST_REL P xs1 ys1 ∧ LIST_REL P xs2 ys2
   
   [LIST_REL_SPLIT2]  Theorem
      
      ⊢ ∀xs1 zs.
            LIST_REL P zs (xs1 ⧺ xs2) ⇔
            ∃ys1 ys2.
                zs = ys1 ⧺ ys2 ∧ LIST_REL P ys1 xs1 ∧ LIST_REL P ys2 xs2
   
   [LIST_REL_cases]  Theorem
      
      ⊢ ∀R a0 a1.
            LIST_REL R a0 a1 ⇔
            a0 = [] ∧ a1 = [] ∨
            ∃h1 h2 t1 t2.
                a0 = h1::t1 ∧ a1 = h2::t2 ∧ R h1 h2 ∧ LIST_REL R t1 t2
   
   [LIST_REL_def]  Theorem
      
      ⊢ (LIST_REL R [] [] ⇔ T) ∧ (LIST_REL R (a::as) [] ⇔ F) ∧
        (LIST_REL R [] (b::bs) ⇔ F) ∧
        (LIST_REL R (a::as) (b::bs) ⇔ R a b ∧ LIST_REL R as bs)
   
   [LIST_REL_eq]  Theorem
      
      ⊢ LIST_REL $= = $=
   
   [LIST_REL_ind]  Theorem
      
      ⊢ ∀R LIST_REL'.
            LIST_REL' [] [] ∧
            (∀h1 h2 t1 t2.
                 R h1 h2 ∧ LIST_REL' t1 t2 ⇒ LIST_REL' (h1::t1) (h2::t2)) ⇒
            ∀a0 a1. LIST_REL R a0 a1 ⇒ LIST_REL' a0 a1
   
   [LIST_REL_mono]  Theorem
      
      ⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ LIST_REL R1 l1 l2 ⇒ LIST_REL R2 l1 l2
   
   [LIST_REL_rules]  Theorem
      
      ⊢ ∀R.
            LIST_REL R [] [] ∧
            ∀h1 h2 t1 t2.
                R h1 h2 ∧ LIST_REL R t1 t2 ⇒ LIST_REL R (h1::t1) (h2::t2)
   
   [LIST_REL_strongind]  Theorem
      
      ⊢ ∀R LIST_REL'.
            LIST_REL' [] [] ∧
            (∀h1 h2 t1 t2.
                 R h1 h2 ∧ LIST_REL R t1 t2 ∧ LIST_REL' t1 t2 ⇒
                 LIST_REL' (h1::t1) (h2::t2)) ⇒
            ∀a0 a1. LIST_REL R a0 a1 ⇒ LIST_REL' a0 a1
   
   [LIST_REL_trans]  Theorem
      
      ⊢ ∀l1 l2 l3.
            (∀n.
                 n < LENGTH l1 ∧ R (EL n l1) (EL n l2) ∧
                 R (EL n l2) (EL n l3) ⇒
                 R (EL n l1) (EL n l3)) ∧ LIST_REL R l1 l2 ∧
            LIST_REL R l2 l3 ⇒
            LIST_REL R l1 l3
   
   [LIST_TO_SET]  Theorem
      
      ⊢ set [] = ∅ ∧ set (h::t) = h INSERT set t
   
   [LIST_TO_SET_APPEND]  Theorem
      
      ⊢ ∀l1 l2. set (l1 ⧺ l2) = set l1 ∪ set l2
   
   [LIST_TO_SET_EQ_EMPTY]  Theorem
      
      ⊢ (set l = ∅ ⇔ l = []) ∧ (∅ = set l ⇔ l = [])
   
   [LIST_TO_SET_FILTER]  Theorem
      
      ⊢ set (FILTER P l) = {x | P x} ∩ set l
   
   [LIST_TO_SET_FLAT]  Theorem
      
      ⊢ ∀ls. set (FLAT ls) = BIGUNION (set (MAP set ls))
   
   [LIST_TO_SET_GENLIST]  Theorem
      
      ⊢ ∀f n. set (GENLIST f n) = IMAGE f (count n)
   
   [LIST_TO_SET_MAP]  Theorem
      
      ⊢ ∀f l. set (MAP f l) = IMAGE f (set l)
   
   [LIST_TO_SET_REVERSE]  Theorem
      
      ⊢ ∀ls. set (REVERSE ls) = set ls
   
   [LIST_TO_SET_SNOC]  Theorem
      
      ⊢ set (SNOC x ls) = x INSERT set ls
   
   [LIST_TO_SET_THM]  Theorem
      
      ⊢ set [] = ∅ ∧ set (h::t) = h INSERT set t
   
   [LLEX_CONG]  Theorem
      
      ⊢ ∀R l1 l2 R' l1' l2'.
            l1 = l1' ∧ l2 = l2' ∧
            (∀a b. MEM a l1' ∧ MEM b l2' ⇒ (R a b ⇔ R' a b)) ⇒
            (LLEX R l1 l2 ⇔ LLEX R' l1' l2')
   
   [LLEX_EL_THM]  Theorem
      
      ⊢ ∀R l1 l2.
            LLEX R l1 l2 ⇔
            ∃n.
                n ≤ LENGTH l1 ∧ n < LENGTH l2 ∧ TAKE n l1 = TAKE n l2 ∧
                (n < LENGTH l1 ⇒ R (EL n l1) (EL n l2))
   
   [LLEX_MONO]  Theorem
      
      ⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ LLEX R1 x y ⇒ LLEX R2 x y
   
   [LLEX_NIL2]  Theorem
      
      ⊢ ¬LLEX R l []
   
   [LLEX_THM]  Theorem
      
      ⊢ (¬LLEX R [] [] ∧ ¬LLEX R (h1::t1) []) ∧ LLEX R [] (h2::t2) ∧
        (LLEX R (h1::t1) (h2::t2) ⇔ R h1 h2 ∨ h1 = h2 ∧ LLEX R t1 t2)
   
   [LLEX_not_WF]  Theorem
      
      ⊢ (∃a b. R a b) ⇒ ¬WF (LLEX R)
   
   [LLEX_total]  Theorem
      
      ⊢ total (RC R) ⇒ total (RC (LLEX R))
   
   [LLEX_transitive]  Theorem
      
      ⊢ transitive R ⇒ transitive (LLEX R)
   
   [LRC_MEM]  Theorem
      
      ⊢ LRC R ls x y ∧ MEM e ls ⇒ ∃z t. R e z ∧ LRC R t z y
   
   [LRC_MEM_right]  Theorem
      
      ⊢ LRC R (h::t) x y ∧ MEM e t ⇒ ∃z p. R z e ∧ LRC R p x z
   
   [LUPDATE_LENGTH]  Theorem
      
      ⊢ ∀xs x y ys. LUPDATE x (LENGTH xs) (xs ⧺ y::ys) = xs ⧺ x::ys
   
   [LUPDATE_MAP]  Theorem
      
      ⊢ ∀x n l f. MAP f (LUPDATE x n l) = LUPDATE (f x) n (MAP f l)
   
   [LUPDATE_NIL]  Theorem
      
      ⊢ ∀xs n x. LUPDATE x n xs = [] ⇔ xs = []
   
   [LUPDATE_SAME]  Theorem
      
      ⊢ ∀n ls. n < LENGTH ls ⇒ LUPDATE (EL n ls) n ls = ls
   
   [LUPDATE_SEM]  Theorem
      
      ⊢ (∀e n l. LENGTH (LUPDATE e n l) = LENGTH l) ∧
        ∀e n l p.
            p < LENGTH l ⇒
            EL p (LUPDATE e n l) = if p = n then e else EL p l
   
   [LUPDATE_SNOC]  Theorem
      
      ⊢ ∀ys k x y.
            LUPDATE x k (SNOC y ys) =
            if k = LENGTH ys then SNOC x ys else SNOC y (LUPDATE x k ys)
   
   [LUPDATE_SOME_MAP]  Theorem
      
      ⊢ ∀xs n f h.
            LUPDATE (SOME (f h)) n (MAP (OPTION_MAP f) xs) =
            MAP (OPTION_MAP f) (LUPDATE (SOME h) n xs)
   
   [LUPDATE_compute]  Theorem
      
      ⊢ (∀e n. LUPDATE e n [] = []) ∧ (∀e x l. LUPDATE e 0 (x::l) = e::l) ∧
        (∀e n x l.
             LUPDATE e (NUMERAL (BIT1 n)) (x::l) =
             x::LUPDATE e (NUMERAL (BIT1 n) − 1) l) ∧
        ∀e n x l.
            LUPDATE e (NUMERAL (BIT2 n)) (x::l) =
            x::LUPDATE e (NUMERAL (BIT1 n)) l
   
   [MAP2]  Theorem
      
      ⊢ (∀f. MAP2 f [] [] = []) ∧
        ∀f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2
   
   [MAP2_APPEND]  Theorem
      
      ⊢ ∀xs ys xs1 ys1 f.
            LENGTH xs = LENGTH xs1 ⇒
            MAP2 f (xs ⧺ ys) (xs1 ⧺ ys1) = MAP2 f xs xs1 ⧺ MAP2 f ys ys1
   
   [MAP2_CONG]  Theorem
      
      ⊢ ∀l1 l1' l2 l2' f f'.
            l1 = l1' ∧ l2 = l2' ∧
            (∀x y. MEM x l1' ∧ MEM y l2' ⇒ f x y = f' x y) ⇒
            MAP2 f l1 l2 = MAP2 f' l1' l2'
   
   [MAP2_DEF]  Theorem
      
      ⊢ (∀t2 t1 h2 h1 f. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2) ∧
        (∀y f. MAP2 f [] y = []) ∧ ∀v5 v4 f. MAP2 f (v4::v5) [] = []
   
   [MAP2_MAP]  Theorem
      
      ⊢ ∀l1 l2.
            LENGTH l1 = LENGTH l2 ⇒
            ∀f. MAP2 f l1 l2 = MAP (UNCURRY f) (ZIP (l1,l2))
   
   [MAP2_NIL]  Theorem
      
      ⊢ MAP2 f x [] = []
   
   [MAP2_ZIP]  Theorem
      
      ⊢ ∀l1 l2.
            LENGTH l1 = LENGTH l2 ⇒
            ∀f. MAP2 f l1 l2 = MAP (UNCURRY f) (ZIP (l1,l2))
   
   [MAP2_ind]  Theorem
      
      ⊢ ∀P.
            (∀f h1 t1 h2 t2. P f t1 t2 ⇒ P f (h1::t1) (h2::t2)) ∧
            (∀f y. P f [] y) ∧ (∀f v4 v5. P f (v4::v5) []) ⇒
            ∀v v1 v2. P v v1 v2
   
   [MAP_APPEND]  Theorem
      
      ⊢ ∀f l1 l2. MAP f (l1 ⧺ l2) = MAP f l1 ⧺ MAP f l2
   
   [MAP_APPEND_MAP_EQ]  Theorem
      
      ⊢ ∀xs ys.
            MAP f1 xs ⧺ MAP g1 ys = MAP f2 xs ⧺ MAP g2 ys ⇔
            MAP f1 xs = MAP f2 xs ∧ MAP g1 ys = MAP g2 ys
   
   [MAP_CONG]  Theorem
      
      ⊢ ∀l1 l2 f f'.
            l1 = l2 ∧ (∀x. MEM x l2 ⇒ f x = f' x) ⇒ MAP f l1 = MAP f' l2
   
   [MAP_DROP]  Theorem
      
      ⊢ ∀l i. MAP f (DROP i l) = DROP i (MAP f l)
   
   [MAP_EQ_APPEND]  Theorem
      
      ⊢ MAP f l = l1 ⧺ l2 ⇔
        ∃l10 l20. l = l10 ⧺ l20 ∧ l1 = MAP f l10 ∧ l2 = MAP f l20
   
   [MAP_EQ_CONS]  Theorem
      
      ⊢ MAP f l = h::t ⇔ ∃x0 t0. l = x0::t0 ∧ h = f x0 ∧ t = MAP f t0
   
   [MAP_EQ_EVERY2]  Theorem
      
      ⊢ ∀f1 f2 l1 l2.
            MAP f1 l1 = MAP f2 l2 ⇔
            LENGTH l1 = LENGTH l2 ∧ LIST_REL (λx y. f1 x = f2 y) l1 l2
   
   [MAP_EQ_NIL]  Theorem
      
      ⊢ ∀l f. (MAP f l = [] ⇔ l = []) ∧ ([] = MAP f l ⇔ l = [])
   
   [MAP_EQ_SING]  Theorem
      
      ⊢ MAP f l = [x] ⇔ ∃x0. l = [x0] ∧ x = f x0
   
   [MAP_EQ_f]  Theorem
      
      ⊢ ∀f1 f2 l. MAP f1 l = MAP f2 l ⇔ ∀e. MEM e l ⇒ f1 e = f2 e
   
   [MAP_FLAT]  Theorem
      
      ⊢ MAP f (FLAT l) = FLAT (MAP (MAP f) l)
   
   [MAP_FRONT]  Theorem
      
      ⊢ ∀ls. ls ≠ [] ⇒ MAP f (FRONT ls) = FRONT (MAP f ls)
   
   [MAP_GENLIST]  Theorem
      
      ⊢ ∀f g n. MAP f (GENLIST g n) = GENLIST (f ∘ g) n
   
   [MAP_ID]  Theorem
      
      ⊢ MAP (λx. x) l = l ∧ MAP I l = l
   
   [MAP_LIST_BIND]  Theorem
      
      ⊢ MAP f (LIST_BIND l g) = LIST_BIND l (MAP f ∘ g)
   
   [MAP_MAP_o]  Theorem
      
      ⊢ ∀f g l. MAP f (MAP g l) = MAP (f ∘ g) l
   
   [MAP_SNOC]  Theorem
      
      ⊢ ∀f x l. MAP f (SNOC x l) = SNOC (f x) (MAP f l)
   
   [MAP_TAKE]  Theorem
      
      ⊢ ∀f n l. MAP f (TAKE n l) = TAKE n (MAP f l)
   
   [MAP_TL]  Theorem
      
      ⊢ ∀l f. ¬NULL l ⇒ MAP f (TL l) = TL (MAP f l)
   
   [MAP_ZIP]  Theorem
      
      ⊢ LENGTH l1 = LENGTH l2 ⇒
        MAP FST (ZIP (l1,l2)) = l1 ∧ MAP SND (ZIP (l1,l2)) = l2 ∧
        MAP (f ∘ FST) (ZIP (l1,l2)) = MAP f l1 ∧
        MAP (g ∘ SND) (ZIP (l1,l2)) = MAP g l2
   
   [MAP_ZIP_SAME]  Theorem
      
      ⊢ ∀ls f. MAP f (ZIP (ls,ls)) = MAP (λx. f (x,x)) ls
   
   [MAP_o]  Theorem
      
      ⊢ ∀f g. MAP (f ∘ g) = MAP f ∘ MAP g
   
   [MEM]  Theorem
      
      ⊢ (∀x. MEM x [] ⇔ F) ∧ ∀x h t. MEM x (h::t) ⇔ x = h ∨ MEM x t
   
   [MEM_APPEND]  Theorem
      
      ⊢ ∀e l1 l2. MEM e (l1 ⧺ l2) ⇔ MEM e l1 ∨ MEM e l2
   
   [MEM_APPEND_lemma]  Theorem
      
      ⊢ ∀a b c d x.
            a ⧺ [x] ⧺ b = c ⧺ [x] ⧺ d ∧ ¬MEM x b ∧ ¬MEM x a ⇒ a = c ∧ b = d
   
   [MEM_DROP]  Theorem
      
      ⊢ ∀x ls n.
            MEM x (DROP n ls) ⇔ ∃m. m + n < LENGTH ls ∧ x = EL (m + n) ls
   
   [MEM_EL]  Theorem
      
      ⊢ ∀l x. MEM x l ⇔ ∃n. n < LENGTH l ∧ x = EL n l
   
   [MEM_FILTER]  Theorem
      
      ⊢ ∀P L x. MEM x (FILTER P L) ⇔ P x ∧ MEM x L
   
   [MEM_FLAT]  Theorem
      
      ⊢ ∀x L. MEM x (FLAT L) ⇔ ∃l. MEM l L ∧ MEM x l
   
   [MEM_GENLIST]  Theorem
      
      ⊢ MEM x (GENLIST f n) ⇔ ∃m. m < n ∧ x = f m
   
   [MEM_LUPDATE]  Theorem
      
      ⊢ ∀l x y i.
            MEM x (LUPDATE y i l) ⇔
            i < LENGTH l ∧ x = y ∨ ∃j. j < LENGTH l ∧ i ≠ j ∧ EL j l = x
   
   [MEM_LUPDATE_E]  Theorem
      
      ⊢ ∀l x y i. MEM x (LUPDATE y i l) ⇒ x = y ∨ MEM x l
   
   [MEM_MAP]  Theorem
      
      ⊢ ∀l f x. MEM x (MAP f l) ⇔ ∃y. x = f y ∧ MEM y l
   
   [MEM_REVERSE]  Theorem
      
      ⊢ ∀l x. MEM x (REVERSE l) ⇔ MEM x l
   
   [MEM_SET_TO_LIST]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. MEM x (SET_TO_LIST s) ⇔ x ∈ s
   
   [MEM_SNOC]  Theorem
      
      ⊢ ∀y x l. MEM y (SNOC x l) ⇔ y = x ∨ MEM y l
   
   [MEM_SPLIT]  Theorem
      
      ⊢ ∀x l. MEM x l ⇔ ∃l1 l2. l = l1 ⧺ x::l2
   
   [MEM_SPLIT_APPEND_first]  Theorem
      
      ⊢ MEM e l ⇔ ∃pfx sfx. l = pfx ⧺ [e] ⧺ sfx ∧ ¬MEM e pfx
   
   [MEM_SPLIT_APPEND_last]  Theorem
      
      ⊢ MEM e l ⇔ ∃pfx sfx. l = pfx ⧺ [e] ⧺ sfx ∧ ¬MEM e sfx
   
   [MEM_ZIP]  Theorem
      
      ⊢ ∀l1 l2 p.
            LENGTH l1 = LENGTH l2 ⇒
            (MEM p (ZIP (l1,l2)) ⇔
             ∃n. n < LENGTH l1 ∧ p = (EL n l1,EL n l2))
   
   [MEM_ZIP_MEM_MAP]  Theorem
      
      ⊢ LENGTH (FST ps) = LENGTH (SND ps) ∧ MEM p (ZIP ps) ⇒
        MEM (FST p) (FST ps) ∧ MEM (SND p) (SND ps)
   
   [MEM_dropWhile_IMP]  Theorem
      
      ⊢ ∀P ls x. MEM x (dropWhile P ls) ⇒ MEM x ls
   
   [MONO_EVERY]  Theorem
      
      ⊢ (∀x. P x ⇒ Q x) ⇒ EVERY P l ⇒ EVERY Q l
   
   [MONO_EXISTS]  Theorem
      
      ⊢ (∀x. P x ⇒ Q x) ⇒ EXISTS P l ⇒ EXISTS Q l
   
   [NOT_CONS_NIL]  Theorem
      
      ⊢ ∀a1 a0. a0::a1 ≠ []
   
   [NOT_EQ_LIST]  Theorem
      
      ⊢ ∀h1 h2. h1 ≠ h2 ⇒ ∀l1 l2. h1::l1 ≠ h2::l2
   
   [NOT_EVERY]  Theorem
      
      ⊢ ∀P l. ¬EVERY P l ⇔ EXISTS ($~ ∘ P) l
   
   [NOT_EXISTS]  Theorem
      
      ⊢ ∀P l. ¬EXISTS P l ⇔ EVERY ($~ ∘ P) l
   
   [NOT_NIL_CONS]  Theorem
      
      ⊢ ∀a1 a0. [] ≠ a0::a1
   
   [NOT_NIL_EQ_LENGTH_NOT_0]  Theorem
      
      ⊢ x ≠ [] ⇔ 0 < LENGTH x
   
   [NOT_NULL_MEM]  Theorem
      
      ⊢ ∀l. ¬NULL l ⇔ ∃e. MEM e l
   
   [NRC_LRC]  Theorem
      
      ⊢ NRC R n x y ⇔ ∃ls. LRC R ls x y ∧ LENGTH ls = n
   
   [NULL]  Theorem
      
      ⊢ NULL [] ∧ ∀h t. ¬NULL (h::t)
   
   [NULL_APPEND]  Theorem
      
      ⊢ NULL (l1 ⧺ l2) ⇔ NULL l1 ∧ NULL l2
   
   [NULL_EQ]  Theorem
      
      ⊢ ∀l. NULL l ⇔ l = []
   
   [NULL_FILTER]  Theorem
      
      ⊢ ∀P ls. NULL (FILTER P ls) ⇔ ∀x. MEM x ls ⇒ ¬P x
   
   [NULL_GENLIST]  Theorem
      
      ⊢ ∀n f. NULL (GENLIST f n) ⇔ n = 0
   
   [NULL_LENGTH]  Theorem
      
      ⊢ ∀l. NULL l ⇔ LENGTH l = 0
   
   [OPT_MMAP_cong]  Theorem
      
      ⊢ ∀f1 f2 x1 x2.
            x1 = x2 ∧ (∀a. MEM a x2 ⇒ f1 a = f2 a) ⇒
            OPT_MMAP f1 x1 = OPT_MMAP f2 x2
   
   [REVERSE_11]  Theorem
      
      ⊢ ∀l1 l2. REVERSE l1 = REVERSE l2 ⇔ l1 = l2
   
   [REVERSE_APPEND]  Theorem
      
      ⊢ ∀l1 l2. REVERSE (l1 ⧺ l2) = REVERSE l2 ⧺ REVERSE l1
   
   [REVERSE_EQ_NIL]  Theorem
      
      ⊢ REVERSE l = [] ⇔ l = []
   
   [REVERSE_EQ_SING]  Theorem
      
      ⊢ REVERSE l = [e] ⇔ l = [e]
   
   [REVERSE_GENLIST]  Theorem
      
      ⊢ REVERSE (GENLIST f n) = GENLIST (λm. f (PRE n − m)) n
   
   [REVERSE_REV]  Theorem
      
      ⊢ ∀L. REVERSE L = REV L []
   
   [REVERSE_REVERSE]  Theorem
      
      ⊢ ∀l. REVERSE (REVERSE l) = l
   
   [REVERSE_SNOC]  Theorem
      
      ⊢ ∀x l. REVERSE (SNOC x l) = x::REVERSE l
   
   [REVERSE_SNOC_DEF]  Theorem
      
      ⊢ REVERSE [] = [] ∧ ∀x l. REVERSE (x::l) = SNOC x (REVERSE l)
   
   [REVERSE_o_REVERSE]  Theorem
      
      ⊢ REVERSE ∘ REVERSE ∘ f = f
   
   [REV_REVERSE_LEM]  Theorem
      
      ⊢ ∀L1 L2. REV L1 L2 = REVERSE L1 ⧺ L2
   
   [SET_TO_LIST_CARD]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ LENGTH (SET_TO_LIST s) = CARD s
   
   [SET_TO_LIST_EMPTY]  Theorem
      
      ⊢ SET_TO_LIST ∅ = []
   
   [SET_TO_LIST_IND]  Theorem
      
      ⊢ ∀P. (∀s. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s)) ⇒ P s) ⇒ ∀v. P v
   
   [SET_TO_LIST_INV]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ set (SET_TO_LIST s) = s
   
   [SET_TO_LIST_IN_MEM]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇔ MEM x (SET_TO_LIST s)
   
   [SET_TO_LIST_SING]  Theorem
      
      ⊢ SET_TO_LIST {x} = [x]
   
   [SET_TO_LIST_THM]  Theorem
      
      ⊢ FINITE s ⇒
        SET_TO_LIST s =
        if s = ∅ then [] else CHOICE s::SET_TO_LIST (REST s)
   
   [SHORTLEX_LENGTH_LE]  Theorem
      
      ⊢ ∀l1 l2. SHORTLEX R l1 l2 ⇒ LENGTH l1 ≤ LENGTH l2
   
   [SHORTLEX_MONO]  Theorem
      
      ⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ SHORTLEX R1 x y ⇒ SHORTLEX R2 x y
   
   [SHORTLEX_NIL2]  Theorem
      
      ⊢ ¬SHORTLEX R l []
   
   [SHORTLEX_THM]  Theorem
      
      ⊢ (¬SHORTLEX R [] [] ∧ ¬SHORTLEX R (h1::t1) []) ∧
        SHORTLEX R [] (h2::t2) ∧
        (SHORTLEX R (h1::t1) (h2::t2) ⇔
         LENGTH t1 < LENGTH t2 ∨
         LENGTH t1 = LENGTH t2 ∧ (R h1 h2 ∨ h1 = h2 ∧ SHORTLEX R t1 t2))
   
   [SHORTLEX_total]  Theorem
      
      ⊢ total (RC R) ⇒ total (RC (SHORTLEX R))
   
   [SHORTLEX_transitive]  Theorem
      
      ⊢ transitive R ⇒ transitive (SHORTLEX R)
   
   [SINGL_APPLY_MAP]  Theorem
      
      ⊢ [f] <*> l = MAP f l
   
   [SINGL_APPLY_PERMUTE]  Theorem
      
      ⊢ fs <*> [x] = [(λf. f x)] <*> fs
   
   [SINGL_LIST_APPLY_L]  Theorem
      
      ⊢ LIST_BIND [x] f = f x
   
   [SINGL_LIST_APPLY_R]  Theorem
      
      ⊢ LIST_BIND l (λx. [x]) = l
   
   [SINGL_SINGL_APPLY]  Theorem
      
      ⊢ [f] <*> [x] = [f x]
   
   [SING_HD]  Theorem
      
      ⊢ ([HD xs] = xs ⇔ LENGTH xs = 1) ∧ (xs = [HD xs] ⇔ LENGTH xs = 1)
   
   [SNOC_11]  Theorem
      
      ⊢ ∀x y a b. SNOC x y = SNOC a b ⇔ x = a ∧ y = b
   
   [SNOC_APPEND]  Theorem
      
      ⊢ ∀x l. SNOC x l = l ⧺ [x]
   
   [SNOC_Axiom]  Theorem
      
      ⊢ ∀e f. ∃fn. fn [] = e ∧ ∀x l. fn (SNOC x l) = f x l (fn l)
   
   [SNOC_CASES]  Theorem
      
      ⊢ ∀ll. ll = [] ∨ ∃x l. ll = SNOC x l
   
   [SNOC_INDUCT]  Theorem
      
      ⊢ ∀P. P [] ∧ (∀l. P l ⇒ ∀x. P (SNOC x l)) ⇒ ∀l. P l
   
   [SUM_ACC_SUM_LEM]  Theorem
      
      ⊢ ∀L n. SUM_ACC L n = SUM L + n
   
   [SUM_APPEND]  Theorem
      
      ⊢ ∀l1 l2. SUM (l1 ⧺ l2) = SUM l1 + SUM l2
   
   [SUM_IMAGE_LIST_TO_SET_upper_bound]  Theorem
      
      ⊢ ∀ls. ∑ f (set ls) ≤ SUM (MAP f ls)
   
   [SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST]  Theorem
      
      ⊢ FINITE s ⇒ ∑ f s = SUM (MAP f (SET_TO_LIST s))
   
   [SUM_MAP_FOLDL]  Theorem
      
      ⊢ ∀ls. SUM (MAP f ls) = FOLDL (λa e. a + f e) 0 ls
   
   [SUM_MAP_MEM_bound]  Theorem
      
      ⊢ ∀f x ls. MEM x ls ⇒ f x ≤ SUM (MAP f ls)
   
   [SUM_MAP_PLUS]  Theorem
      
      ⊢ ∀f g ls.
            SUM (MAP (λx. f x + g x) ls) = SUM (MAP f ls) + SUM (MAP g ls)
   
   [SUM_MAP_PLUS_ZIP]  Theorem
      
      ⊢ ∀ls1 ls2.
            LENGTH ls1 = LENGTH ls2 ∧ (∀x y. f (x,y) = g x + h y) ⇒
            SUM (MAP f (ZIP (ls1,ls2))) = SUM (MAP g ls1) + SUM (MAP h ls2)
   
   [SUM_SNOC]  Theorem
      
      ⊢ ∀x l. SUM (SNOC x l) = SUM l + x
   
   [SUM_SUM_ACC]  Theorem
      
      ⊢ ∀L. SUM L = SUM_ACC L 0
   
   [SUM_eq_0]  Theorem
      
      ⊢ ∀ls. SUM ls = 0 ⇔ ∀x. MEM x ls ⇒ x = 0
   
   [SWAP_REVERSE]  Theorem
      
      ⊢ ∀l1 l2. l1 = REVERSE l2 ⇔ l2 = REVERSE l1
   
   [SWAP_REVERSE_SYM]  Theorem
      
      ⊢ ∀l1 l2. REVERSE l1 = l2 ⇔ l1 = REVERSE l2
   
   [TAKE1]  Theorem
      
      ⊢ ∀l. l ≠ [] ⇒ TAKE 1 l = [EL 0 l]
   
   [TAKE1_DROP]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ TAKE 1 (DROP n l) = [EL n l]
   
   [TAKE_0]  Theorem
      
      ⊢ TAKE 0 l = []
   
   [TAKE_APPEND1]  Theorem
      
      ⊢ ∀n. n ≤ LENGTH l1 ⇒ TAKE n (l1 ⧺ l2) = TAKE n l1
   
   [TAKE_APPEND2]  Theorem
      
      ⊢ ∀n. LENGTH l1 < n ⇒ TAKE n (l1 ⧺ l2) = l1 ⧺ TAKE (n − LENGTH l1) l2
   
   [TAKE_DROP]  Theorem
      
      ⊢ ∀n l. TAKE n l ⧺ DROP n l = l
   
   [TAKE_EQ_NIL]  Theorem
      
      ⊢ TAKE n l = [] ⇔ n = 0 ∨ l = []
   
   [TAKE_GENLIST]  Theorem
      
      ⊢ TAKE n (GENLIST f m) = GENLIST f (MIN n m)
   
   [TAKE_LENGTH_ID]  Theorem
      
      ⊢ ∀l. TAKE (LENGTH l) l = l
   
   [TAKE_LENGTH_ID_rwt]  Theorem
      
      ⊢ ∀l m. m = LENGTH l ⇒ TAKE m l = l
   
   [TAKE_LENGTH_TOO_LONG]  Theorem
      
      ⊢ ∀l n. LENGTH l ≤ n ⇒ TAKE n l = l
   
   [TAKE_SUM]  Theorem
      
      ⊢ ∀n m l. TAKE (n + m) l = TAKE n l ⧺ TAKE m (DROP n l)
   
   [TAKE_TAKE_MIN]  Theorem
      
      ⊢ ∀m n. TAKE n (TAKE m l) = TAKE (MIN n m) l
   
   [TAKE_compute]  Theorem
      
      ⊢ (∀l. TAKE 0 l = []) ∧ (∀n. TAKE (NUMERAL (BIT1 n)) [] = []) ∧
        (∀n. TAKE (NUMERAL (BIT2 n)) [] = []) ∧
        (∀n h t.
             TAKE (NUMERAL (BIT1 n)) (h::t) =
             h::TAKE (NUMERAL (BIT1 n) − 1) t) ∧
        ∀n h t.
            TAKE (NUMERAL (BIT2 n)) (h::t) = h::TAKE (NUMERAL (BIT1 n)) t
   
   [TAKE_cons]  Theorem
      
      ⊢ 0 < n ⇒ TAKE n (x::xs) = x::TAKE (n − 1) xs
   
   [TAKE_nil]  Theorem
      
      ⊢ ∀n. TAKE n [] = []
   
   [TAKE_splitAtPki]  Theorem
      
      ⊢ TAKE n l = splitAtPki (K ∘ $= n) K l
   
   [TL]  Theorem
      
      ⊢ ∀h t. TL (h::t) = t
   
   [TL_GENLIST]  Theorem
      
      ⊢ ∀f n. TL (GENLIST f (SUC n)) = GENLIST (f ∘ SUC) n
   
   [UNION_APPEND]  Theorem
      
      ⊢ ∀l1 l2. set l1 ∪ set l2 = set (l1 ⧺ l2)
   
   [UNIQUE_FILTER]  Theorem
      
      ⊢ ∀e L. UNIQUE e L ⇔ FILTER ($= e) L = [e]
   
   [UNIQUE_LENGTH_FILTER]  Theorem
      
      ⊢ ∀e L. UNIQUE e L ⇔ LENGTH (FILTER ($= e) L) = 1
   
   [UNZIP_MAP]  Theorem
      
      ⊢ ∀L. UNZIP L = (MAP FST L,MAP SND L)
   
   [UNZIP_THM]  Theorem
      
      ⊢ UNZIP [] = ([],[]) ∧
        UNZIP ((x,y)::t) = (let (L1,L2) = UNZIP t in (x::L1,y::L2))
   
   [UNZIP_ZIP]  Theorem
      
      ⊢ ∀l1 l2. LENGTH l1 = LENGTH l2 ⇒ UNZIP (ZIP (l1,l2)) = (l1,l2)
   
   [WF_LIST_PRED]  Theorem
      
      ⊢ WF (λL1 L2. ∃h. L2 = h::L1)
   
   [WF_SHORTLEX]  Theorem
      
      ⊢ WF R ⇒ WF (SHORTLEX R)
   
   [WF_SHORTLEX_same_lengths]  Theorem
      
      ⊢ WF R ⇒
        ∀l s.
            (∀d. d ∈ s ⇒ LENGTH d = l) ∧ (∃a. a ∈ s) ⇒
            ∃b. b ∈ s ∧ ∀c. SHORTLEX R c b ⇒ c ∉ s
   
   [ZIP]  Theorem
      
      ⊢ ZIP ([],[]) = [] ∧
        ∀x1 l1 x2 l2. ZIP (x1::l1,x2::l2) = (x1,x2)::ZIP (l1,l2)
   
   [ZIP_DROP]  Theorem
      
      ⊢ ∀a b n.
            n ≤ LENGTH a ∧ LENGTH a = LENGTH b ⇒
            ZIP (DROP n a,DROP n b) = DROP n (ZIP (a,b))
   
   [ZIP_EQ_NIL]  Theorem
      
      ⊢ ∀l1 l2.
            LENGTH l1 = LENGTH l2 ⇒ (ZIP (l1,l2) = [] ⇔ l1 = [] ∧ l2 = [])
   
   [ZIP_GENLIST]  Theorem
      
      ⊢ ∀l f n.
            LENGTH l = n ⇒
            ZIP (l,GENLIST f n) = GENLIST (λx. (EL x l,f x)) n
   
   [ZIP_MAP]  Theorem
      
      ⊢ ∀l1 l2 f1 f2.
            LENGTH l1 = LENGTH l2 ⇒
            ZIP (MAP f1 l1,l2) = MAP (λp. (f1 (FST p),SND p)) (ZIP (l1,l2)) ∧
            ZIP (l1,MAP f2 l2) = MAP (λp. (FST p,f2 (SND p))) (ZIP (l1,l2))
   
   [ZIP_UNZIP]  Theorem
      
      ⊢ ∀l. ZIP (UNZIP l) = l
   
   [all_distinct_nub]  Theorem
      
      ⊢ ∀l. ALL_DISTINCT (nub l)
   
   [datatype_list]  Theorem
      
      ⊢ DATATYPE (list [] CONS)
   
   [dropWhile_APPEND_EVERY]  Theorem
      
      ⊢ ∀P l1 l2. EVERY P l1 ⇒ dropWhile P (l1 ⧺ l2) = dropWhile P l2
   
   [dropWhile_APPEND_EXISTS]  Theorem
      
      ⊢ ∀P l1 l2.
            EXISTS ($~ ∘ P) l1 ⇒
            dropWhile P (l1 ⧺ l2) = dropWhile P l1 ⧺ l2
   
   [dropWhile_eq_nil]  Theorem
      
      ⊢ ∀P ls. dropWhile P ls = [] ⇔ EVERY P ls
   
   [dropWhile_splitAtPki]  Theorem
      
      ⊢ ∀P. dropWhile P = splitAtPki (combin$C (K ∘ $~ ∘ P)) (K I)
   
   [el_append3]  Theorem
      
      ⊢ ∀l1 x l2. EL (LENGTH l1) (l1 ⧺ [x] ⧺ l2) = x
   
   [every_zip_fst]  Theorem
      
      ⊢ ∀l1 l2 P.
            LENGTH l1 = LENGTH l2 ⇒
            (EVERY (λx. P (FST x)) (ZIP (l1,l2)) ⇔ EVERY P l1)
   
   [every_zip_snd]  Theorem
      
      ⊢ ∀l1 l2 P.
            LENGTH l1 = LENGTH l2 ⇒
            (EVERY (λx. P (SND x)) (ZIP (l1,l2)) ⇔ EVERY P l2)
   
   [exists_list_GENLIST]  Theorem
      
      ⊢ (∃ls. P ls) ⇔ ∃n f. P (GENLIST f n)
   
   [isPREFIX_CONSR]  Theorem
      
      ⊢ x ≼ y::ys ⇔ x = [] ∨ ∃xs. x = y::xs ∧ xs ≼ ys
   
   [isPREFIX_NILR]  Theorem
      
      ⊢ x ≼ [] ⇔ x = []
   
   [isPREFIX_THM]  Theorem
      
      ⊢ ([] ≼ l ⇔ T) ∧ (h::t ≼ [] ⇔ F) ∧
        (h1::t1 ≼ h2::t2 ⇔ h1 = h2 ∧ t1 ≼ t2)
   
   [last_drop]  Theorem
      
      ⊢ ∀l n. n < LENGTH l ⇒ LAST (DROP n l) = LAST l
   
   [lazy_list_case_compute]  Theorem
      
      ⊢ list_CASE = (λl b f. if NULL l then b else f (HD l) (TL l))
   
   [length_nub_append]  Theorem
      
      ⊢ ∀l1 l2.
            LENGTH (nub (l1 ⧺ l2)) =
            LENGTH (nub l1) + LENGTH (nub (FILTER (λx. ¬MEM x l1) l2))
   
   [list_11]  Theorem
      
      ⊢ ∀a0 a1 a0' a1'. a0::a1 = a0'::a1' ⇔ a0 = a0' ∧ a1 = a1'
   
   [list_Axiom]  Theorem
      
      ⊢ ∀f0 f1. ∃fn. fn [] = f0 ∧ ∀a0 a1. fn (a0::a1) = f1 a0 a1 (fn a1)
   
   [list_Axiom_old]  Theorem
      
      ⊢ ∀x f. ∃!fn1. fn1 [] = x ∧ ∀h t. fn1 (h::t) = f (fn1 t) h t
   
   [list_CASES]  Theorem
      
      ⊢ ∀l. l = [] ∨ ∃h t. l = h::t
   
   [list_INDUCT]  Theorem
      
      ⊢ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h::t)) ⇒ ∀l. P l
   
   [list_INDUCT0]  Theorem
      
      ⊢ ∀P. P [] ∧ (∀l. P l ⇒ ∀a. P (a::l)) ⇒ ∀l. P l
   
   [list_case_compute]  Theorem
      
      ⊢ ∀l. list_CASE l b f = if NULL l then b else f (HD l) (TL l)
   
   [list_case_cong]  Theorem
      
      ⊢ ∀M M' v f.
            M = M' ∧ (M' = [] ⇒ v = v') ∧
            (∀a0 a1. M' = a0::a1 ⇒ f a0 a1 = f' a0 a1) ⇒
            list_CASE M v f = list_CASE M' v' f'
   
   [list_case_eq]  Theorem
      
      ⊢ list_CASE x v f = v' ⇔
        x = [] ∧ v = v' ∨ ∃a l. x = a::l ∧ f a l = v'
   
   [list_distinct]  Theorem
      
      ⊢ ∀a1 a0. [] ≠ a0::a1
   
   [list_induction]  Theorem
      
      ⊢ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h::t)) ⇒ ∀l. P l
   
   [list_nchotomy]  Theorem
      
      ⊢ ∀l. l = [] ∨ ∃h t. l = h::t
   
   [list_size_cong]  Theorem
      
      ⊢ ∀M N f f'.
            M = N ∧ (∀x. MEM x N ⇒ f x = f' x) ⇒
            list_size f M = list_size f' N
   
   [list_to_set_diff]  Theorem
      
      ⊢ ∀l1 l2. set l2 DIFF set l1 = set (FILTER (λx. ¬MEM x l1) l2)
   
   [lupdate_append]  Theorem
      
      ⊢ ∀x n l1 l2.
            n < LENGTH l1 ⇒ LUPDATE x n (l1 ⧺ l2) = LUPDATE x n l1 ⧺ l2
   
   [lupdate_append2]  Theorem
      
      ⊢ ∀v l1 x l2 l3.
            LUPDATE v (LENGTH l1) (l1 ⧺ [x] ⧺ l2) = l1 ⧺ [v] ⧺ l2
   
   [mem_exists_set]  Theorem
      
      ⊢ ∀x y l. MEM (x,y) l ⇒ ∃z. x = FST z ∧ MEM z l
   
   [nub_append]  Theorem
      
      ⊢ ∀l1 l2. nub (l1 ⧺ l2) = nub (FILTER (λx. ¬MEM x l2) l1) ⧺ nub l2
   
   [nub_set]  Theorem
      
      ⊢ ∀l. set (nub l) = set l
   
   [oEL_DROP]  Theorem
      
      ⊢ oEL n (DROP m xs) = oEL (m + n) xs
   
   [oEL_EQ_EL]  Theorem
      
      ⊢ ∀xs n y. oEL n xs = SOME y ⇔ n < LENGTH xs ∧ y = EL n xs
   
   [oEL_LUPDATE]  Theorem
      
      ⊢ ∀xs i n x.
            oEL n (LUPDATE x i xs) =
            if i ≠ n then oEL n xs
            else if i < LENGTH xs then SOME x
            else NONE
   
   [oEL_TAKE_E]  Theorem
      
      ⊢ oEL n (TAKE m xs) = SOME x ⇒ oEL n xs = SOME x
   
   [oEL_THM]  Theorem
      
      ⊢ ∀xs n. oEL n xs = if n < LENGTH xs then SOME (EL n xs) else NONE
   
   [oHD_thm]  Theorem
      
      ⊢ oHD [] = NONE ∧ oHD (h::t) = SOME h
   
   [splitAtPki_APPEND]  Theorem
      
      ⊢ ∀l1 l2 P k.
            EVERYi (λi. $~ ∘ P i) l1 ∧
            (0 < LENGTH l2 ⇒ P (LENGTH l1) (HD l2)) ⇒
            splitAtPki P k (l1 ⧺ l2) = k l1 l2
   
   [splitAtPki_EQN]  Theorem
      
      ⊢ splitAtPki P k l =
        case OLEAST i. i < LENGTH l ∧ P i (EL i l) of
          NONE => k l []
        | SOME i => k (TAKE i l) (DROP i l)
   
   [splitAtPki_MAP]  Theorem
      
      ⊢ splitAtPki P k (MAP f l) =
        splitAtPki (combin$C ($o ∘ P) f)
          (combin$C ($o ∘ k ∘ MAP f) (MAP f)) l
   
   [splitAtPki_RAND]  Theorem
      
      ⊢ f (splitAtPki P k l) = splitAtPki P ($o f ∘ k) l
   
   [splitAtPki_change_predicate]  Theorem
      
      ⊢ (∀i. i < LENGTH l ⇒ (P1 i (EL i l) ⇔ P2 i (EL i l))) ⇒
        splitAtPki P1 k l = splitAtPki P2 k l
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13