Structure rich_listTheory


Source File Identifier index Theory binding index

signature rich_listTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val AND_EL_DEF : thm
    val BUTLASTN_def : thm
    val COUNT_LIST_AUX_def : thm
    val COUNT_LIST_def : thm
    val ELL : thm
    val IS_SUBLIST : thm
    val IS_SUFFIX : thm
    val LASTN_def : thm
    val LIST_ELEM_COUNT_DEF : thm
    val OR_EL_DEF : thm
    val PREFIX_DEF : thm
    val REPLICATE : thm
    val SCANL : thm
    val SCANR : thm
    val SEG : thm
    val SPLITL_def : thm
    val SPLITP : thm
    val SPLITP_AUX_def : thm
    val SPLITR_def : thm
    val SUFFIX_DEF : thm
    val TL_T_def : thm
    val UNZIP_FST_DEF : thm
    val UNZIP_SND_DEF : thm
    val common_prefixes_def : thm
    val longest_prefix_def : thm
  
  (*  Theorems  *)
    val ALL_DISTINCT_DROP : thm
    val ALL_DISTINCT_MEM_ZIP_MAP : thm
    val ALL_EL_MAP : thm
    val AND_EL_FOLDL : thm
    val AND_EL_FOLDR : thm
    val APPEND_ASSOC_CONS : thm
    val APPEND_BUTLASTN_DROP : thm
    val APPEND_BUTLASTN_LASTN : thm
    val APPEND_FOLDL : thm
    val APPEND_FOLDR : thm
    val APPEND_NIL : thm
    val APPEND_SNOC1 : thm
    val APPEND_TAKE_LASTN : thm
    val ASSOC_APPEND : thm
    val ASSOC_FOLDL_FLAT : thm
    val ASSOC_FOLDR_FLAT : thm
    val BUTLASTN : thm
    val BUTLASTN_1 : thm
    val BUTLASTN_APPEND1 : thm
    val BUTLASTN_APPEND2 : thm
    val BUTLASTN_BUTLASTN : thm
    val BUTLASTN_CONS : thm
    val BUTLASTN_FRONT : thm
    val BUTLASTN_LASTN : thm
    val BUTLASTN_LASTN_NIL : thm
    val BUTLASTN_LENGTH_APPEND : thm
    val BUTLASTN_LENGTH_CONS : thm
    val BUTLASTN_LENGTH_NIL : thm
    val BUTLASTN_MAP : thm
    val BUTLASTN_REVERSE : thm
    val BUTLASTN_SEG : thm
    val BUTLASTN_SUC_FRONT : thm
    val BUTLASTN_TAKE : thm
    val BUTLASTN_compute : thm
    val COMM_ASSOC_FOLDL_REVERSE : thm
    val COMM_ASSOC_FOLDR_REVERSE : thm
    val COMM_MONOID_FOLDL : thm
    val COMM_MONOID_FOLDR : thm
    val CONS_APPEND : thm
    val COUNT_LIST_ADD : thm
    val COUNT_LIST_AUX_compute : thm
    val COUNT_LIST_COUNT : thm
    val COUNT_LIST_GENLIST : thm
    val COUNT_LIST_SNOC : thm
    val COUNT_LIST_compute : thm
    val DROP : thm
    val DROP_APPEND : thm
    val DROP_APPEND1 : thm
    val DROP_APPEND2 : thm
    val DROP_CONS_EL : thm
    val DROP_DROP : thm
    val DROP_DROP_T : thm
    val DROP_EL_CONS : thm
    val DROP_FUNPOW_TL : thm
    val DROP_LASTN : thm
    val DROP_LENGTH_APPEND : thm
    val DROP_LENGTH_NIL : thm
    val DROP_LENGTH_NIL_rwt : thm
    val DROP_REPLICATE : thm
    val DROP_REVERSE : thm
    val DROP_SEG : thm
    val DROP_SNOC : thm
    val ELL_0_SNOC : thm
    val ELL_APPEND1 : thm
    val ELL_APPEND2 : thm
    val ELL_CONS : thm
    val ELL_EL : thm
    val ELL_LAST : thm
    val ELL_LENGTH_APPEND : thm
    val ELL_LENGTH_CONS : thm
    val ELL_LENGTH_SNOC : thm
    val ELL_MAP : thm
    val ELL_MEM : thm
    val ELL_PRE_LENGTH : thm
    val ELL_REVERSE : thm
    val ELL_REVERSE_EL : thm
    val ELL_SEG : thm
    val ELL_SNOC : thm
    val ELL_SUC_SNOC : thm
    val ELL_compute : thm
    val EL_APPEND1 : thm
    val EL_APPEND2 : thm
    val EL_CONS : thm
    val EL_COUNT_LIST : thm
    val EL_ELL : thm
    val EL_FRONT : thm
    val EL_LENGTH_APPEND : thm
    val EL_LENGTH_APPEND_rwt : thm
    val EL_MEM : thm
    val EL_PRE_LENGTH : thm
    val EL_REPLICATE : thm
    val EL_REVERSE_ELL : thm
    val EL_SEG : thm
    val EVERY2_APPEND : thm
    val EVERY2_APPEND_suff : thm
    val EVERY2_DROP : thm
    val EVERY2_REVERSE1 : thm
    val EVERY2_TAKE : thm
    val EVERY_BUTLASTN : thm
    val EVERY_DROP : thm
    val EVERY_FOLDL : thm
    val EVERY_FOLDL_MAP : thm
    val EVERY_FOLDR : thm
    val EVERY_FOLDR_MAP : thm
    val EVERY_LASTN : thm
    val EVERY_REPLICATE : thm
    val EVERY_REVERSE : thm
    val EVERY_SEG : thm
    val EVERY_TAKE : thm
    val EXISTS_BUTLASTN : thm
    val EXISTS_DISJ : thm
    val EXISTS_DROP : thm
    val EXISTS_FOLDL : thm
    val EXISTS_FOLDL_MAP : thm
    val EXISTS_FOLDR : thm
    val EXISTS_FOLDR_MAP : thm
    val EXISTS_LASTN : thm
    val EXISTS_REVERSE : thm
    val EXISTS_SEG : thm
    val EXISTS_TAKE : thm
    val FCOMM_FOLDL_APPEND : thm
    val FCOMM_FOLDL_FLAT : thm
    val FCOMM_FOLDR_APPEND : thm
    val FCOMM_FOLDR_FLAT : thm
    val FILTER_COMM : thm
    val FILTER_EQ : thm
    val FILTER_FILTER : thm
    val FILTER_FLAT : thm
    val FILTER_FOLDL : thm
    val FILTER_FOLDR : thm
    val FILTER_IDEM : thm
    val FILTER_MAP : thm
    val FILTER_SNOC : thm
    val FINITE_common_prefixes : thm
    val FINITE_prefix : thm
    val FLAT_FLAT : thm
    val FLAT_FOLDL : thm
    val FLAT_FOLDR : thm
    val FLAT_REVERSE : thm
    val FLAT_SNOC : thm
    val FOLDL_APPEND : thm
    val FOLDL_FILTER : thm
    val FOLDL_FOLDR_REVERSE : thm
    val FOLDL_MAP : thm
    val FOLDL_MAP2 : thm
    val FOLDL_REVERSE : thm
    val FOLDL_SINGLE : thm
    val FOLDL_SNOC_NIL : thm
    val FOLDR_APPEND : thm
    val FOLDR_CONS_NIL : thm
    val FOLDR_FILTER : thm
    val FOLDR_FILTER_REVERSE : thm
    val FOLDR_FOLDL : thm
    val FOLDR_FOLDL_REVERSE : thm
    val FOLDR_MAP : thm
    val FOLDR_MAP_REVERSE : thm
    val FOLDR_REVERSE : thm
    val FOLDR_SINGLE : thm
    val FOLDR_SNOC : thm
    val FRONT_APPEND : thm
    val IS_PREFIX : thm
    val IS_PREFIX_ANTISYM : thm
    val IS_PREFIX_APPEND : thm
    val IS_PREFIX_APPEND1 : thm
    val IS_PREFIX_APPEND2 : thm
    val IS_PREFIX_APPEND3 : thm
    val IS_PREFIX_APPENDS : thm
    val IS_PREFIX_BUTLAST : thm
    val IS_PREFIX_IS_SUBLIST : thm
    val IS_PREFIX_LENGTH : thm
    val IS_PREFIX_LENGTH_ANTI : thm
    val IS_PREFIX_NIL : thm
    val IS_PREFIX_PREFIX : thm
    val IS_PREFIX_REFL : thm
    val IS_PREFIX_REVERSE : thm
    val IS_PREFIX_SNOC : thm
    val IS_PREFIX_TRANS : thm
    val IS_SUBLIST_APPEND : thm
    val IS_SUBLIST_REVERSE : thm
    val IS_SUFFIX_APPEND : thm
    val IS_SUFFIX_APPEND1 : thm
    val IS_SUFFIX_CONS : thm
    val IS_SUFFIX_CONS2_E : thm
    val IS_SUFFIX_IS_SUBLIST : thm
    val IS_SUFFIX_REFL : thm
    val IS_SUFFIX_REVERSE : thm
    val IS_SUFFIX_TRANS : thm
    val IS_SUFFIX_compute : thm
    val LASTN : thm
    val LASTN_1 : thm
    val LASTN_APPEND1 : thm
    val LASTN_APPEND2 : thm
    val LASTN_BUTLASTN : thm
    val LASTN_CONS : thm
    val LASTN_DROP : thm
    val LASTN_LASTN : thm
    val LASTN_LENGTH_APPEND : thm
    val LASTN_LENGTH_ID : thm
    val LASTN_MAP : thm
    val LASTN_REVERSE : thm
    val LASTN_SEG : thm
    val LASTN_compute : thm
    val LAST_LASTN_LAST : thm
    val LENGTH_BUTLASTN : thm
    val LENGTH_COUNT_LIST : thm
    val LENGTH_FILTER_LEQ : thm
    val LENGTH_FILTER_LESS : thm
    val LENGTH_FLAT : thm
    val LENGTH_FLAT_REPLICATE : thm
    val LENGTH_FOLDL : thm
    val LENGTH_FOLDR : thm
    val LENGTH_FRONT : thm
    val LENGTH_LASTN : thm
    val LENGTH_NOT_NULL : thm
    val LENGTH_REPLICATE : thm
    val LENGTH_SCANL : thm
    val LENGTH_SCANR : thm
    val LENGTH_SEG : thm
    val LENGTH_UNZIP_FST : thm
    val LENGTH_UNZIP_SND : thm
    val LIST_ELEM_COUNT_CARD_EL : thm
    val LIST_ELEM_COUNT_MEM : thm
    val LIST_ELEM_COUNT_THM : thm
    val LIST_REL_APPEND_SING : thm
    val LIST_REL_GENLIST : thm
    val LIST_REL_REPLICATE_same : thm
    val LIST_REL_REVERSE_EQ : thm
    val LIST_TO_SET_EQ_SING : thm
    val LUPDATE_APPEND1 : thm
    val LUPDATE_APPEND2 : thm
    val MAP_COUNT_LIST : thm
    val MAP_FILTER : thm
    val MAP_FLAT : thm
    val MAP_FOLDL : thm
    val MAP_FOLDR : thm
    val MAP_FST_funs : thm
    val MAP_REVERSE : thm
    val MAP_SND_FILTER_NEQ : thm
    val MEM_BUTLASTN : thm
    val MEM_COUNT_LIST : thm
    val MEM_DROP_IMP : thm
    val MEM_EXISTS : thm
    val MEM_FOLDL : thm
    val MEM_FOLDL_MAP : thm
    val MEM_FOLDR : thm
    val MEM_FOLDR_MAP : thm
    val MEM_FRONT : thm
    val MEM_LAST : thm
    val MEM_LASTN : thm
    val MEM_LAST_FRONT : thm
    val MEM_REPLICATE : thm
    val MEM_SEG : thm
    val MEM_SING_APPEND : thm
    val MEM_TAKE : thm
    val MONOID_APPEND_NIL : thm
    val NIL_IN_common_prefixes : thm
    val NOT_NIL_SNOC : thm
    val NOT_NULL_SNOC : thm
    val NOT_SNOC_NIL : thm
    val NULL_FOLDL : thm
    val NULL_FOLDR : thm
    val OR_EL_FOLDL : thm
    val OR_EL_FOLDR : thm
    val PREFIX : thm
    val PREFIX_FOLDR : thm
    val REPLICATE_APPEND : thm
    val REPLICATE_GENLIST : thm
    val REPLICATE_NIL : thm
    val REPLICATE_compute : thm
    val REVERSE_DROP : thm
    val REVERSE_FLAT : thm
    val REVERSE_FOLDL : thm
    val REVERSE_FOLDR : thm
    val REVERSE_REPLICATE : thm
    val REVERSE_ZIP : thm
    val SEG1 : thm
    val SEG_0_SNOC : thm
    val SEG_APPEND : thm
    val SEG_APPEND1 : thm
    val SEG_APPEND2 : thm
    val SEG_CONS : thm
    val SEG_LASTN_BUTLASTN : thm
    val SEG_LENGTH_ID : thm
    val SEG_LENGTH_SNOC : thm
    val SEG_REVERSE : thm
    val SEG_SEG : thm
    val SEG_SNOC : thm
    val SEG_SUC_CONS : thm
    val SEG_SUC_EL : thm
    val SEG_TAKE_DROP : thm
    val SEG_compute : thm
    val SNOC_EL_TAKE : thm
    val SNOC_EQ_LENGTH_EQ : thm
    val SNOC_FOLDR : thm
    val SNOC_REPLICATE : thm
    val SNOC_REVERSE_CONS : thm
    val SPLITP_APPEND : thm
    val SPLITP_EVERY : thm
    val SPLITP_IMP : thm
    val SPLITP_JOIN : thm
    val SPLITP_LENGTH : thm
    val SPLITP_NIL_FST_IMP : thm
    val SPLITP_NIL_SND_EVERY : thm
    val SPLITP_compute : thm
    val SPLITP_splitAtPki : thm
    val SUM_FLAT : thm
    val SUM_FOLDL : thm
    val SUM_FOLDR : thm
    val SUM_REPLICATE : thm
    val SUM_REVERSE : thm
    val TAKE : thm
    val TAKE_APPEND : thm
    val TAKE_APPEND1 : thm
    val TAKE_APPEND2 : thm
    val TAKE_BUTLASTN : thm
    val TAKE_EL_SNOC : thm
    val TAKE_LENGTH_APPEND : thm
    val TAKE_PRE_LENGTH : thm
    val TAKE_REVERSE : thm
    val TAKE_SEG : thm
    val TAKE_SEG_DROP : thm
    val TAKE_SNOC : thm
    val TAKE_TAKE : thm
    val TAKE_TAKE_T : thm
    val TL_SNOC : thm
    val UNIQUE_LIST_ELEM_COUNT : thm
    val UNZIP_SNOC : thm
    val ZIP_APPEND : thm
    val ZIP_COUNT_LIST : thm
    val ZIP_SNOC : thm
    val ZIP_TAKE : thm
    val ZIP_TAKE_LEQ : thm
    val all_distinct_count_list : thm
    val common_prefixes_BIGINTER : thm
    val common_prefixes_NIL : thm
    val common_prefixes_NONEMPTY : thm
    val common_prefixes_PAIR : thm
    val count_list_sub1 : thm
    val el_map_count : thm
    val every_count_list : thm
    val is_prefix_el : thm
    val list_rel_butlastn : thm
    val list_rel_lastn : thm
    val longest_prefix_EMPTY : thm
    val longest_prefix_NIL : thm
    val longest_prefix_PAIR : thm
    val longest_prefix_SING : thm
    val longest_prefix_UNIQUE : thm
    val map_replicate : thm
    val nub_GENLIST : thm
    val prefixes_is_prefix_total : thm
    val take_drop_partition : thm
    val two_common_prefixes : thm
  
  val rich_list_grammars : type_grammar.grammar * term_grammar.grammar
  
  (* Aliases for legacy theorem names *)
  val ALL_DISTINCT_SNOC : thm
  val ALL_EL : thm
  val ALL_EL_APPEND : thm
  val ALL_EL_BUTFIRSTN : thm
  val ALL_EL_BUTLASTN : thm
  val ALL_EL_CONJ : thm
  val ALL_EL_FIRSTN : thm
  val ALL_EL_FOLDL : thm
  val ALL_EL_FOLDL_MAP : thm
  val ALL_EL_FOLDR : thm
  val ALL_EL_FOLDR_MAP : thm
  val ALL_EL_LASTN : thm
  val ALL_EL_REPLICATE : thm
  val ALL_EL_REVERSE : thm
  val ALL_EL_SEG : thm
  val ALL_EL_SNOC : thm
  val APPEND : thm
  val APPEND_11_LENGTH : thm
  val APPEND_ASSOC : thm
  val APPEND_BUTLASTN_BUTFIRSTN : thm
  val APPEND_BUTLAST_LAST : thm
  val APPEND_FIRSTN_BUTFIRSTN : thm
  val APPEND_FIRSTN_LASTN : thm
  val APPEND_LENGTH_EQ : thm
  val APPEND_SNOC : thm
  val BUTFIRSTN : thm
  val BUTFIRSTN_APPEND1 : thm
  val BUTFIRSTN_APPEND2 : thm
  val BUTFIRSTN_BUTFIRSTN : thm
  val BUTFIRSTN_CONS_EL : thm
  val BUTFIRSTN_LASTN : thm
  val BUTFIRSTN_LENGTH_APPEND : thm
  val BUTFIRSTN_LENGTH_NIL : thm
  val BUTFIRSTN_REVERSE : thm
  val BUTFIRSTN_SEG : thm
  val BUTFIRSTN_SNOC : thm
  val BUTLAST : thm
  val BUTLASTN_BUTLAST : thm
  val BUTLASTN_FIRSTN : thm
  val BUTLASTN_SUC_BUTLAST : thm
  val BUTLAST_CONS : thm
  val CONS : thm
  val CONS_11 : thm
  val EL : thm
  val ELL_IS_EL : thm
  val EL_BUTFIRSTN : thm
  val EL_DROP : thm
  val EL_FIRSTN : thm
  val EL_GENLIST : thm
  val EL_IS_EL : thm
  val EL_LENGTH_SNOC : thm
  val EL_MAP : thm
  val EL_REVERSE : thm
  val EL_SNOC : thm
  val EL_TAKE : thm
  val EQ_LIST : thm
  val EVERY_GENLIST : thm
  val EXISTS_GENLIST : thm
  val FILTER : thm
  val FILTER_APPEND : thm
  val FILTER_REVERSE : thm
  val FIRSTN : thm
  val FIRSTN_APPEND1 : thm
  val FIRSTN_APPEND2 : thm
  val FIRSTN_BUTLASTN : thm
  val FIRSTN_FIRSTN : thm
  val FIRSTN_LENGTH_APPEND : thm
  val FIRSTN_LENGTH_ID : thm
  val FIRSTN_REVERSE : thm
  val FIRSTN_SEG : thm
  val FIRSTN_SNOC : thm
  val FLAT : thm
  val FLAT_APPEND : thm
  val FOLDL : thm
  val FOLDL_SNOC : thm
  val FOLDR : thm
  val GENLIST : thm
  val GENLIST_APPEND : thm
  val GENLIST_CONS : thm
  val GENLIST_FUN_EQ : thm
  val HD : thm
  val HD_GENLIST : thm
  val IS_EL : thm
  val IS_EL_APPEND : thm
  val IS_EL_BUTFIRSTN : thm
  val IS_EL_BUTLASTN : thm
  val IS_EL_DEF : thm
  val IS_EL_FILTER : thm
  val IS_EL_FIRSTN : thm
  val IS_EL_FOLDL : thm
  val IS_EL_FOLDL_MAP : thm
  val IS_EL_FOLDR : thm
  val IS_EL_FOLDR_MAP : thm
  val IS_EL_LASTN : thm
  val IS_EL_REPLICATE : thm
  val IS_EL_REVERSE : thm
  val IS_EL_SEG : thm
  val IS_EL_SNOC : thm
  val IS_EL_SOME_EL : thm
  val LAST : thm
  val LASTN_BUTFIRSTN : thm
  val LAST_APPEND : thm
  val LAST_CONS : thm
  val LENGTH : thm
  val LENGTH_APPEND : thm
  val LENGTH_BUTFIRSTN : thm
  val LENGTH_BUTLAST : thm
  val LENGTH_CONS : thm
  val LENGTH_EQ_NIL : thm
  val LENGTH_FIRSTN : thm
  val LENGTH_GENLIST : thm
  val LENGTH_MAP : thm
  val LENGTH_NIL : thm
  val LENGTH_REVERSE : thm
  val LENGTH_SNOC : thm
  val LENGTH_ZIP : thm
  val LIST_NOT_EQ : thm
  val MAP : thm
  val MAP2 : thm
  val MAP2_ZIP : thm
  val MAP_APPEND : thm
  val MAP_EQ_f : thm
  val MAP_GENLIST : thm
  val MAP_MAP_o : thm
  val MAP_SNOC : thm
  val MAP_o : thm
  val NOT_ALL_EL_SOME_EL : thm
  val NOT_CONS_NIL : thm
  val NOT_EQ_LIST : thm
  val NOT_NIL_CONS : thm
  val NOT_SOME_EL_ALL_EL : thm
  val NULL : thm
  val NULL_DEF : thm
  val NULL_EQ_NIL : thm
  val REVERSE_APPEND : thm
  val REVERSE_EQ_NIL : thm
  val REVERSE_REVERSE : thm
  val REVERSE_SNOC : thm
  val SNOC : thm
  val SNOC_11 : thm
  val SNOC_APPEND : thm
  val SNOC_Axiom : thm
  val SNOC_CASES : thm
  val SNOC_EL_FIRSTN : thm
  val SNOC_INDUCT : thm
  val SOME_EL : thm
  val SOME_EL_APPEND : thm
  val SOME_EL_BUTFIRSTN : thm
  val SOME_EL_BUTLASTN : thm
  val SOME_EL_DISJ : thm
  val SOME_EL_FIRSTN : thm
  val SOME_EL_FOLDL : thm
  val SOME_EL_FOLDL_MAP : thm
  val SOME_EL_FOLDR : thm
  val SOME_EL_FOLDR_MAP : thm
  val SOME_EL_LASTN : thm
  val SOME_EL_MAP : thm
  val SOME_EL_REVERSE : thm
  val SOME_EL_SEG : thm
  val SOME_EL_SNOC : thm
  val SUM : thm
  val SUM_APPEND : thm
  val SUM_SNOC : thm
  val TL : thm
  val TL_GENLIST : thm
  val UNZIP : thm
  val UNZIP_ZIP : thm
  val ZIP : thm
  val ZIP_FIRSTN : thm
  val ZIP_FIRSTN_LEQ : thm
  val ZIP_GENLIST : thm
  val ZIP_UNZIP : thm
(*
   [list] Parent theory of "rich_list"
   
   [AND_EL_DEF]  Definition
      
      ⊢ AND_EL = EVERY I
   
   [BUTLASTN_def]  Definition
      
      ⊢ ∀n xs. BUTLASTN n xs = REVERSE (DROP n (REVERSE xs))
   
   [COUNT_LIST_AUX_def]  Definition
      
      ⊢ (∀l. COUNT_LIST_AUX 0 l = l) ∧
        ∀n l. COUNT_LIST_AUX (SUC n) l = COUNT_LIST_AUX n (n::l)
   
   [COUNT_LIST_def]  Definition
      
      ⊢ COUNT_LIST 0 = [] ∧
        ∀n. COUNT_LIST (SUC n) = 0::MAP SUC (COUNT_LIST n)
   
   [ELL]  Definition
      
      ⊢ (∀l. ELL 0 l = LAST l) ∧ ∀n l. ELL (SUC n) l = ELL n (FRONT l)
   
   [IS_SUBLIST]  Definition
      
      ⊢ (∀l. IS_SUBLIST l [] ⇔ T) ∧ (∀x l. IS_SUBLIST [] (x::l) ⇔ F) ∧
        ∀x1 l1 x2 l2.
          IS_SUBLIST (x1::l1) (x2::l2) ⇔
          x1 = x2 ∧ l2 ≼ l1 ∨ IS_SUBLIST l1 (x2::l2)
   
   [IS_SUFFIX]  Definition
      
      ⊢ (∀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
   
   [LASTN_def]  Definition
      
      ⊢ ∀n xs. LASTN n xs = REVERSE (TAKE n (REVERSE xs))
   
   [LIST_ELEM_COUNT_DEF]  Definition
      
      ⊢ ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)
   
   [OR_EL_DEF]  Definition
      
      ⊢ OR_EL = EXISTS I
   
   [PREFIX_DEF]  Definition
      
      ⊢ ∀P l. PREFIX P l = FST (SPLITP ($¬ ∘ P) l)
   
   [REPLICATE]  Definition
      
      ⊢ (∀x. REPLICATE 0 x = []) ∧
        ∀n x. REPLICATE (SUC n) x = x::REPLICATE n x
   
   [SCANL]  Definition
      
      ⊢ (∀f e. SCANL f e [] = [e]) ∧
        ∀f e x l. SCANL f e (x::l) = e::SCANL f (f e x) l
   
   [SCANR]  Definition
      
      ⊢ (∀f e. SCANR f e [] = [e]) ∧
        ∀f e x l. SCANR f e (x::l) = f x (HD (SCANR f e l))::SCANR f e l
   
   [SEG]  Definition
      
      ⊢ (∀k l. SEG 0 k l = []) ∧
        (∀m x l. SEG (SUC m) 0 (x::l) = x::SEG m 0 l) ∧
        ∀m k x l. SEG (SUC m) (SUC k) (x::l) = SEG (SUC m) k l
   
   [SPLITL_def]  Definition
      
      ⊢ ∀P. SPLITL P = SPLITP ($¬ ∘ P)
   
   [SPLITP]  Definition
      
      ⊢ (∀P. SPLITP P [] = ([],[])) ∧
        ∀P x l.
          SPLITP P (x::l) =
          if P x then ([],x::l) else (x::FST (SPLITP P l),SND (SPLITP P l))
   
   [SPLITP_AUX_def]  Definition
      
      ⊢ (∀acc P. SPLITP_AUX acc P [] = (acc,[])) ∧
        ∀acc P h t.
          SPLITP_AUX acc P (h::t) =
          if P h then (acc,h::t) else SPLITP_AUX (acc ⧺ [h]) P t
   
   [SPLITR_def]  Definition
      
      ⊢ ∀P l.
          SPLITR P l =
          (let
             (a,b) = SPLITP ($¬ ∘ P) (REVERSE l)
           in
             (REVERSE b,REVERSE a))
   
   [SUFFIX_DEF]  Definition
      
      ⊢ ∀P l.
          SUFFIX P l = FOLDL (λl' x. if P x then SNOC x l' else []) [] l
   
   [TL_T_def]  Definition
      
      ⊢ TL_T [] = [] ∧ ∀h t. TL_T (h::t) = t
   
   [UNZIP_FST_DEF]  Definition
      
      ⊢ ∀l. UNZIP_FST l = FST (UNZIP l)
   
   [UNZIP_SND_DEF]  Definition
      
      ⊢ ∀l. UNZIP_SND l = SND (UNZIP l)
   
   [common_prefixes_def]  Definition
      
      ⊢ ∀s. common_prefixes s = {p | ∀m. m ∈ s ⇒ p ≼ m}
   
   [longest_prefix_def]  Definition
      
      ⊢ ∀s. longest_prefix s =
            if s = ∅ then []
            else @x. is_measure_maximal LENGTH (common_prefixes s) x
   
   [ALL_DISTINCT_DROP]  Theorem
      
      ⊢ ∀ls n. ALL_DISTINCT ls ⇒ ALL_DISTINCT (DROP n ls)
   
   [ALL_DISTINCT_MEM_ZIP_MAP]  Theorem
      
      ⊢ ∀f x ls.
          ALL_DISTINCT ls ⇒
          (MEM x (ZIP (ls,MAP f ls)) ⇔ MEM (FST x) ls ∧ SND x = f (FST x))
   
   [ALL_EL_MAP]  Theorem
      
      ⊢ ∀P f l. EVERY P (MAP f l) ⇔ EVERY (P ∘ f) l
   
   [AND_EL_FOLDL]  Theorem
      
      ⊢ ∀l. AND_EL l ⇔ FOLDL $/\ T l
   
   [AND_EL_FOLDR]  Theorem
      
      ⊢ ∀l. AND_EL l ⇔ FOLDR $/\ T l
   
   [APPEND_ASSOC_CONS]  Theorem
      
      ⊢ ∀l1 h l2 l3. l1 ⧺ h::l2 ⧺ l3 = l1 ⧺ h::(l2 ⧺ l3)
   
   [APPEND_BUTLASTN_DROP]  Theorem
      
      ⊢ ∀m n l. m + n = LENGTH l ⇒ BUTLASTN m l ⧺ DROP n l = l
   
   [APPEND_BUTLASTN_LASTN]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n l ⧺ LASTN n l = l
   
   [APPEND_FOLDL]  Theorem
      
      ⊢ ∀l1 l2. l1 ⧺ l2 = FOLDL (λl' x. SNOC x l') l1 l2
   
   [APPEND_FOLDR]  Theorem
      
      ⊢ ∀l1 l2. l1 ⧺ l2 = FOLDR CONS l2 l1
   
   [APPEND_NIL]  Theorem
      
      ⊢ (∀l. l ⧺ [] = l) ∧ ∀l. [] ⧺ l = l
   
   [APPEND_SNOC1]  Theorem
      
      ⊢ ∀l1 x l2. SNOC x l1 ⧺ l2 = l1 ⧺ x::l2
   
   [APPEND_TAKE_LASTN]  Theorem
      
      ⊢ ∀m n l. m + n = LENGTH l ⇒ TAKE n l ⧺ LASTN m l = l
   
   [ASSOC_APPEND]  Theorem
      
      ⊢ ASSOC $++
   
   [ASSOC_FOLDL_FLAT]  Theorem
      
      ⊢ ∀f. ASSOC f ⇒
            ∀e. RIGHT_ID f e ⇒
                ∀l. FOLDL f e (FLAT l) = FOLDL f e (MAP (FOLDL f e) l)
   
   [ASSOC_FOLDR_FLAT]  Theorem
      
      ⊢ ∀f. ASSOC f ⇒
            ∀e. LEFT_ID f e ⇒
                ∀l. FOLDR f e (FLAT l) = FOLDR f e (MAP (FOLDR f e) l)
   
   [BUTLASTN]  Theorem
      
      ⊢ (∀l. BUTLASTN 0 l = l) ∧
        ∀n x l. BUTLASTN (SUC n) (SNOC x l) = BUTLASTN n l
   
   [BUTLASTN_1]  Theorem
      
      ⊢ ∀l. l ≠ [] ⇒ BUTLASTN 1 l = FRONT l
   
   [BUTLASTN_APPEND1]  Theorem
      
      ⊢ ∀l2 n.
          LENGTH l2 ≤ n ⇒
          ∀l1. BUTLASTN n (l1 ⧺ l2) = BUTLASTN (n − LENGTH l2) l1
   
   [BUTLASTN_APPEND2]  Theorem
      
      ⊢ ∀n l1 l2. n ≤ LENGTH l2 ⇒ BUTLASTN n (l1 ⧺ l2) = l1 ⧺ BUTLASTN n l2
   
   [BUTLASTN_BUTLASTN]  Theorem
      
      ⊢ ∀m n l.
          n + m ≤ LENGTH l ⇒ BUTLASTN n (BUTLASTN m l) = BUTLASTN (n + m) l
   
   [BUTLASTN_CONS]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. BUTLASTN n (x::l) = x::BUTLASTN n l
   
   [BUTLASTN_FRONT]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ BUTLASTN n (FRONT l) = FRONT (BUTLASTN n l)
   
   [BUTLASTN_LASTN]  Theorem
      
      ⊢ ∀m n l.
          m ≤ n ∧ n ≤ LENGTH l ⇒
          BUTLASTN m (LASTN n l) = LASTN (n − m) (BUTLASTN m l)
   
   [BUTLASTN_LASTN_NIL]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n (LASTN n l) = []
   
   [BUTLASTN_LENGTH_APPEND]  Theorem
      
      ⊢ ∀l2 l1. BUTLASTN (LENGTH l2) (l1 ⧺ l2) = l1
   
   [BUTLASTN_LENGTH_CONS]  Theorem
      
      ⊢ ∀l x. BUTLASTN (LENGTH l) (x::l) = [x]
   
   [BUTLASTN_LENGTH_NIL]  Theorem
      
      ⊢ ∀l. BUTLASTN (LENGTH l) l = []
   
   [BUTLASTN_MAP]  Theorem
      
      ⊢ ∀n l.
          n ≤ LENGTH l ⇒ ∀f. BUTLASTN n (MAP f l) = MAP f (BUTLASTN n l)
   
   [BUTLASTN_REVERSE]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n (REVERSE l) = REVERSE (DROP n l)
   
   [BUTLASTN_SEG]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n l = SEG (LENGTH l − n) 0 l
   
   [BUTLASTN_SUC_FRONT]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ BUTLASTN (SUC n) l = BUTLASTN n (FRONT l)
   
   [BUTLASTN_TAKE]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n l = TAKE (LENGTH l − n) l
   
   [BUTLASTN_compute]  Theorem
      
      ⊢ ∀n l.
          BUTLASTN n l =
          (let
             m = LENGTH l
           in
             if n ≤ m then TAKE (m − n) l
             else FAIL BUTLASTN $var$(longer than list) n l)
   
   [COMM_ASSOC_FOLDL_REVERSE]  Theorem
      
      ⊢ ∀f. COMM f ⇒ ASSOC f ⇒ ∀e l. FOLDL f e (REVERSE l) = FOLDL f e l
   
   [COMM_ASSOC_FOLDR_REVERSE]  Theorem
      
      ⊢ ∀f. COMM f ⇒ ASSOC f ⇒ ∀e l. FOLDR f e (REVERSE l) = FOLDR f e l
   
   [COMM_MONOID_FOLDL]  Theorem
      
      ⊢ ∀f. COMM f ⇒
            ∀e'. MONOID f e' ⇒ ∀e l. FOLDL f e l = f e (FOLDL f e' l)
   
   [COMM_MONOID_FOLDR]  Theorem
      
      ⊢ ∀f. COMM f ⇒
            ∀e'. MONOID f e' ⇒ ∀e l. FOLDR f e l = f e (FOLDR f e' l)
   
   [CONS_APPEND]  Theorem
      
      ⊢ ∀x l. x::l = [x] ⧺ l
   
   [COUNT_LIST_ADD]  Theorem
      
      ⊢ ∀n m.
          COUNT_LIST (n + m) =
          COUNT_LIST n ⧺ MAP (λn'. n' + n) (COUNT_LIST m)
   
   [COUNT_LIST_AUX_compute]  Theorem
      
      ⊢ (∀l. COUNT_LIST_AUX 0 l = l) ∧
        (∀n l.
           COUNT_LIST_AUX (NUMERAL (BIT1 n)) l =
           COUNT_LIST_AUX (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 n) − 1::l)) ∧
        ∀n l.
          COUNT_LIST_AUX (NUMERAL (BIT2 n)) l =
          COUNT_LIST_AUX (NUMERAL (BIT1 n)) (NUMERAL (BIT1 n)::l)
   
   [COUNT_LIST_COUNT]  Theorem
      
      ⊢ ∀n. set (COUNT_LIST n) = count n
   
   [COUNT_LIST_GENLIST]  Theorem
      
      ⊢ ∀n. COUNT_LIST n = GENLIST I n
   
   [COUNT_LIST_SNOC]  Theorem
      
      ⊢ COUNT_LIST 0 = [] ∧ ∀n. COUNT_LIST (SUC n) = SNOC n (COUNT_LIST n)
   
   [COUNT_LIST_compute]  Theorem
      
      ⊢ ∀n. COUNT_LIST n = COUNT_LIST_AUX n []
   
   [DROP]  Theorem
      
      ⊢ (∀l. DROP 0 l = l) ∧ ∀n x l. DROP (SUC n) (x::l) = DROP n l
   
   [DROP_APPEND]  Theorem
      
      ⊢ ∀n l1 l2. DROP n (l1 ⧺ l2) = DROP n l1 ⧺ DROP (n − LENGTH l1) l2
   
   [DROP_APPEND1]  Theorem
      
      ⊢ ∀n l1. n ≤ LENGTH l1 ⇒ ∀l2. DROP n (l1 ⧺ l2) = DROP n l1 ⧺ l2
   
   [DROP_APPEND2]  Theorem
      
      ⊢ ∀l1 n.
          LENGTH l1 ≤ n ⇒ ∀l2. DROP n (l1 ⧺ l2) = DROP (n − LENGTH l1) l2
   
   [DROP_CONS_EL]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ DROP n l = EL n l::DROP (SUC n) l
   
   [DROP_DROP]  Theorem
      
      ⊢ ∀n m l. n + m ≤ LENGTH l ⇒ DROP n (DROP m l) = DROP (n + m) l
   
   [DROP_DROP_T]  Theorem
      
      ⊢ ∀n m l. DROP n (DROP m l) = DROP (n + m) l
   
   [DROP_EL_CONS]  Theorem
      
      ⊢ ∀ls n. n < LENGTH ls ⇒ DROP n ls = EL n ls::DROP (n + 1) ls
   
   [DROP_FUNPOW_TL]  Theorem
      
      ⊢ ∀n l. DROP n l = FUNPOW TL_T n l
   
   [DROP_LASTN]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n l = LASTN (LENGTH l − n) l
   
   [DROP_LENGTH_APPEND]  Theorem
      
      ⊢ ∀l1 l2. DROP (LENGTH l1) (l1 ⧺ l2) = l2
   
   [DROP_LENGTH_NIL]  Theorem
      
      ⊢ ∀l. DROP (LENGTH l) l = []
   
   [DROP_LENGTH_NIL_rwt]  Theorem
      
      ⊢ ∀l m. m = LENGTH l ⇒ DROP m l = []
   
   [DROP_REPLICATE]  Theorem
      
      ⊢ DROP n (REPLICATE m a) = REPLICATE (m − n) a
   
   [DROP_REVERSE]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n (REVERSE l) = REVERSE (BUTLASTN n l)
   
   [DROP_SEG]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n l = SEG (LENGTH l − n) n l
   
   [DROP_SNOC]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. DROP n (SNOC x l) = SNOC x (DROP n l)
   
   [ELL_0_SNOC]  Theorem
      
      ⊢ ∀l x. ELL 0 (SNOC x l) = x
   
   [ELL_APPEND1]  Theorem
      
      ⊢ ∀l2 n.
          LENGTH l2 ≤ n ⇒ ∀l1. ELL n (l1 ⧺ l2) = ELL (n − LENGTH l2) l1
   
   [ELL_APPEND2]  Theorem
      
      ⊢ ∀n l2. n < LENGTH l2 ⇒ ∀l1. ELL n (l1 ⧺ l2) = ELL n l2
   
   [ELL_CONS]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ ∀x. ELL n (x::l) = ELL n l
   
   [ELL_EL]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ ELL n l = EL (PRE (LENGTH l − n)) l
   
   [ELL_LAST]  Theorem
      
      ⊢ ∀l. ¬NULL l ⇒ ELL 0 l = LAST l
   
   [ELL_LENGTH_APPEND]  Theorem
      
      ⊢ ∀l1 l2. ¬NULL l1 ⇒ ELL (LENGTH l2) (l1 ⧺ l2) = LAST l1
   
   [ELL_LENGTH_CONS]  Theorem
      
      ⊢ ∀l x. ELL (LENGTH l) (x::l) = x
   
   [ELL_LENGTH_SNOC]  Theorem
      
      ⊢ ∀l x. ELL (LENGTH l) (SNOC x l) = if NULL l then x else HD l
   
   [ELL_MAP]  Theorem
      
      ⊢ ∀n l f. n < LENGTH l ⇒ ELL n (MAP f l) = f (ELL n l)
   
   [ELL_MEM]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ MEM (ELL n l) l
   
   [ELL_PRE_LENGTH]  Theorem
      
      ⊢ ∀l. l ≠ [] ⇒ ELL (PRE (LENGTH l)) l = HD l
   
   [ELL_REVERSE]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ ELL n (REVERSE l) = ELL (PRE (LENGTH l − n)) l
   
   [ELL_REVERSE_EL]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ ELL n (REVERSE l) = EL n l
   
   [ELL_SEG]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ ELL n l = HD (SEG 1 (PRE (LENGTH l − n)) l)
   
   [ELL_SNOC]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀x l. ELL n (SNOC x l) = ELL (PRE n) l
   
   [ELL_SUC_SNOC]  Theorem
      
      ⊢ ∀n x l. ELL (SUC n) (SNOC x l) = ELL n l
   
   [ELL_compute]  Theorem
      
      ⊢ (∀l. ELL 0 l = LAST l) ∧
        (∀n l.
           ELL (NUMERAL (BIT1 n)) l = ELL (NUMERAL (BIT1 n) − 1) (FRONT l)) ∧
        ∀n l. ELL (NUMERAL (BIT2 n)) l = ELL (NUMERAL (BIT1 n)) (FRONT l)
   
   [EL_APPEND1]  Theorem
      
      ⊢ ∀n l1 l2. n < LENGTH l1 ⇒ EL n (l1 ⧺ l2) = EL n l1
   
   [EL_APPEND2]  Theorem
      
      ⊢ ∀l1 n. LENGTH l1 ≤ n ⇒ ∀l2. EL n (l1 ⧺ l2) = EL (n − LENGTH l1) l2
   
   [EL_CONS]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀x l. EL n (x::l) = EL (PRE n) l
   
   [EL_COUNT_LIST]  Theorem
      
      ⊢ ∀m n. m < n ⇒ EL m (COUNT_LIST n) = m
   
   [EL_ELL]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ EL n l = ELL (PRE (LENGTH l − n)) l
   
   [EL_FRONT]  Theorem
      
      ⊢ ∀l n. n < LENGTH (FRONT l) ∧ ¬NULL l ⇒ EL n (FRONT l) = EL n l
   
   [EL_LENGTH_APPEND]  Theorem
      
      ⊢ ∀l2 l1. ¬NULL l2 ⇒ EL (LENGTH l1) (l1 ⧺ l2) = HD l2
   
   [EL_LENGTH_APPEND_rwt]  Theorem
      
      ⊢ ¬NULL l2 ∧ n = LENGTH l1 ⇒ EL n (l1 ⧺ l2) = HD l2
   
   [EL_MEM]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ MEM (EL n l) l
   
   [EL_PRE_LENGTH]  Theorem
      
      ⊢ ∀l. l ≠ [] ⇒ EL (PRE (LENGTH l)) l = LAST l
   
   [EL_REPLICATE]  Theorem
      
      ⊢ ∀n1 n2 x. n1 < n2 ⇒ EL n1 (REPLICATE n2 x) = x
   
   [EL_REVERSE_ELL]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ EL n (REVERSE l) = ELL n l
   
   [EL_SEG]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ EL n l = HD (SEG 1 n l)
   
   [EVERY2_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
   
   [EVERY2_APPEND_suff]  Theorem
      
      ⊢ LIST_REL R l1 l2 ∧ LIST_REL R l3 l4 ⇒
        LIST_REL R (l1 ⧺ l3) (l2 ⧺ l4)
   
   [EVERY2_DROP]  Theorem
      
      ⊢ ∀R l1 l2 n. LIST_REL R l1 l2 ⇒ LIST_REL R (DROP n l1) (DROP n l2)
   
   [EVERY2_REVERSE1]  Theorem
      
      ⊢ ∀l1 l2. LIST_REL R l1 (REVERSE l2) ⇔ LIST_REL R (REVERSE l1) l2
   
   [EVERY2_TAKE]  Theorem
      
      ⊢ ∀P xs ys n. LIST_REL P xs ys ⇒ LIST_REL P (TAKE n xs) (TAKE n ys)
   
   [EVERY_BUTLASTN]  Theorem
      
      ⊢ ∀P l m. EVERY P l ⇒ EVERY P (BUTLASTN m l)
   
   [EVERY_DROP]  Theorem
      
      ⊢ ∀P l m. EVERY P l ⇒ EVERY P (DROP m l)
   
   [EVERY_FOLDL]  Theorem
      
      ⊢ ∀P l. EVERY P l ⇔ FOLDL (λl' x. l' ∧ P x) T l
   
   [EVERY_FOLDL_MAP]  Theorem
      
      ⊢ ∀P l. EVERY P l ⇔ FOLDL $/\ T (MAP P l)
   
   [EVERY_FOLDR]  Theorem
      
      ⊢ ∀P l. EVERY P l ⇔ FOLDR (λx l'. P x ∧ l') T l
   
   [EVERY_FOLDR_MAP]  Theorem
      
      ⊢ ∀P l. EVERY P l ⇔ FOLDR $/\ T (MAP P l)
   
   [EVERY_LASTN]  Theorem
      
      ⊢ ∀P l m. EVERY P l ⇒ EVERY P (LASTN m l)
   
   [EVERY_REPLICATE]  Theorem
      
      ⊢ ∀f n x. EVERY f (REPLICATE n x) ⇔ n = 0 ∨ f x
   
   [EVERY_REVERSE]  Theorem
      
      ⊢ ∀P l. EVERY P (REVERSE l) ⇔ EVERY P l
   
   [EVERY_SEG]  Theorem
      
      ⊢ ∀P l. EVERY P l ⇒ ∀m k. m + k ≤ LENGTH l ⇒ EVERY P (SEG m k l)
   
   [EVERY_TAKE]  Theorem
      
      ⊢ ∀P l m. EVERY P l ⇒ EVERY P (TAKE m l)
   
   [EXISTS_BUTLASTN]  Theorem
      
      ⊢ ∀l m P. EXISTS P (BUTLASTN m l) ⇒ EXISTS P l
   
   [EXISTS_DISJ]  Theorem
      
      ⊢ ∀P Q l. (EXISTS (λx. P x ∨ Q x) l ⇔ EXISTS P l) ∨ EXISTS Q l
   
   [EXISTS_DROP]  Theorem
      
      ⊢ ∀l m P. EXISTS P (DROP m l) ⇒ EXISTS P l
   
   [EXISTS_FOLDL]  Theorem
      
      ⊢ ∀P l. EXISTS P l ⇔ FOLDL (λl' x. l' ∨ P x) F l
   
   [EXISTS_FOLDL_MAP]  Theorem
      
      ⊢ ∀P l. EXISTS P l ⇔ FOLDL $\/ F (MAP P l)
   
   [EXISTS_FOLDR]  Theorem
      
      ⊢ ∀P l. EXISTS P l ⇔ FOLDR (λx l'. P x ∨ l') F l
   
   [EXISTS_FOLDR_MAP]  Theorem
      
      ⊢ ∀P l. EXISTS P l ⇔ FOLDR $\/ F (MAP P l)
   
   [EXISTS_LASTN]  Theorem
      
      ⊢ ∀l m P. EXISTS P (LASTN m l) ⇒ EXISTS P l
   
   [EXISTS_REVERSE]  Theorem
      
      ⊢ ∀P l. EXISTS P (REVERSE l) ⇔ EXISTS P l
   
   [EXISTS_SEG]  Theorem
      
      ⊢ ∀m k l. m + k ≤ LENGTH l ⇒ ∀P. EXISTS P (SEG m k l) ⇒ EXISTS P l
   
   [EXISTS_TAKE]  Theorem
      
      ⊢ ∀l m P. EXISTS P (TAKE m l) ⇒ EXISTS P l
   
   [FCOMM_FOLDL_APPEND]  Theorem
      
      ⊢ ∀f g.
          FCOMM f g ⇒
          ∀e. RIGHT_ID g e ⇒
              ∀l1 l2. FOLDL f e (l1 ⧺ l2) = g (FOLDL f e l1) (FOLDL f e l2)
   
   [FCOMM_FOLDL_FLAT]  Theorem
      
      ⊢ ∀f g.
          FCOMM f g ⇒
          ∀e. RIGHT_ID g e ⇒
              ∀l. FOLDL f e (FLAT l) = FOLDL g e (MAP (FOLDL f e) l)
   
   [FCOMM_FOLDR_APPEND]  Theorem
      
      ⊢ ∀g f.
          FCOMM g f ⇒
          ∀e. LEFT_ID g e ⇒
              ∀l1 l2. FOLDR f e (l1 ⧺ l2) = g (FOLDR f e l1) (FOLDR f e l2)
   
   [FCOMM_FOLDR_FLAT]  Theorem
      
      ⊢ ∀g f.
          FCOMM g f ⇒
          ∀e. LEFT_ID g e ⇒
              ∀l. FOLDR f e (FLAT l) = FOLDR g e (MAP (FOLDR f e) l)
   
   [FILTER_COMM]  Theorem
      
      ⊢ ∀f1 f2 l. FILTER f1 (FILTER f2 l) = FILTER f2 (FILTER f1 l)
   
   [FILTER_EQ]  Theorem
      
      ⊢ ∀P1 P2 l. FILTER P1 l = FILTER P2 l ⇔ ∀x. MEM x l ⇒ (P1 x ⇔ P2 x)
   
   [FILTER_FILTER]  Theorem
      
      ⊢ ∀P Q l. FILTER P (FILTER Q l) = FILTER (λx. P x ∧ Q x) l
   
   [FILTER_FLAT]  Theorem
      
      ⊢ ∀P l. FILTER P (FLAT l) = FLAT (MAP (FILTER P) l)
   
   [FILTER_FOLDL]  Theorem
      
      ⊢ ∀P l.
          FILTER P l = FOLDL (λl' x. if P x then SNOC x l' else l') [] l
   
   [FILTER_FOLDR]  Theorem
      
      ⊢ ∀P l. FILTER P l = FOLDR (λx l'. if P x then x::l' else l') [] l
   
   [FILTER_IDEM]  Theorem
      
      ⊢ ∀f l. FILTER f (FILTER f l) = FILTER f l
   
   [FILTER_MAP]  Theorem
      
      ⊢ ∀f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 ∘ f2) l)
   
   [FILTER_SNOC]  Theorem
      
      ⊢ ∀P x l.
          FILTER P (SNOC x l) =
          if P x then SNOC x (FILTER P l) else FILTER P l
   
   [FINITE_common_prefixes]  Theorem
      
      ⊢ s ≠ ∅ ⇒ FINITE (common_prefixes s)
   
   [FINITE_prefix]  Theorem
      
      ⊢ FINITE {a | a ≼ b}
   
   [FLAT_FLAT]  Theorem
      
      ⊢ ∀l. FLAT (FLAT l) = FLAT (MAP FLAT l)
   
   [FLAT_FOLDL]  Theorem
      
      ⊢ ∀l. FLAT l = FOLDL $++ [] l
   
   [FLAT_FOLDR]  Theorem
      
      ⊢ ∀l. FLAT l = FOLDR $++ [] l
   
   [FLAT_REVERSE]  Theorem
      
      ⊢ ∀l. FLAT (REVERSE l) = REVERSE (FLAT (MAP REVERSE l))
   
   [FLAT_SNOC]  Theorem
      
      ⊢ ∀x l. FLAT (SNOC x l) = FLAT l ⧺ x
   
   [FOLDL_APPEND]  Theorem
      
      ⊢ ∀f e l1 l2. FOLDL f e (l1 ⧺ l2) = FOLDL f (FOLDL f e l1) l2
   
   [FOLDL_FILTER]  Theorem
      
      ⊢ ∀f e P l.
          FOLDL f e (FILTER P l) =
          FOLDL (λx y. if P y then f x y else x) e l
   
   [FOLDL_FOLDR_REVERSE]  Theorem
      
      ⊢ ∀f e l. FOLDL f e l = FOLDR (λx y. f y x) e (REVERSE l)
   
   [FOLDL_MAP]  Theorem
      
      ⊢ ∀f e g l. FOLDL f e (MAP g l) = FOLDL (λx y. f x (g y)) e l
   
   [FOLDL_MAP2]  Theorem
      
      ⊢ ∀f e g l. FOLDL f e (MAP g l) = FOLDL (λx y. f x (g y)) e l
   
   [FOLDL_REVERSE]  Theorem
      
      ⊢ ∀f e l. FOLDL f e (REVERSE l) = FOLDR (λx y. f y x) e l
   
   [FOLDL_SINGLE]  Theorem
      
      ⊢ ∀f e x. FOLDL f e [x] = f e x
   
   [FOLDL_SNOC_NIL]  Theorem
      
      ⊢ ∀l. FOLDL (λxs x. SNOC x xs) [] l = l
   
   [FOLDR_APPEND]  Theorem
      
      ⊢ ∀f e l1 l2. FOLDR f e (l1 ⧺ l2) = FOLDR f (FOLDR f e l2) l1
   
   [FOLDR_CONS_NIL]  Theorem
      
      ⊢ ∀l. FOLDR CONS [] l = l
   
   [FOLDR_FILTER]  Theorem
      
      ⊢ ∀f e P l.
          FOLDR f e (FILTER P l) =
          FOLDR (λx y. if P x then f x y else y) e l
   
   [FOLDR_FILTER_REVERSE]  Theorem
      
      ⊢ ∀f. (∀a b c. f a (f b c) = f b (f a c)) ⇒
            ∀e P l.
              FOLDR f e (FILTER P (REVERSE l)) = FOLDR f e (FILTER P l)
   
   [FOLDR_FOLDL]  Theorem
      
      ⊢ ∀f e. MONOID f e ⇒ ∀l. FOLDR f e l = FOLDL f e l
   
   [FOLDR_FOLDL_REVERSE]  Theorem
      
      ⊢ ∀f e l. FOLDR f e l = FOLDL (λx y. f y x) e (REVERSE l)
   
   [FOLDR_MAP]  Theorem
      
      ⊢ ∀f e g l. FOLDR f e (MAP g l) = FOLDR (λx y. f (g x) y) e l
   
   [FOLDR_MAP_REVERSE]  Theorem
      
      ⊢ ∀f. (∀a b c. f a (f b c) = f b (f a c)) ⇒
            ∀e g l. FOLDR f e (MAP g (REVERSE l)) = FOLDR f e (MAP g l)
   
   [FOLDR_REVERSE]  Theorem
      
      ⊢ ∀f e l. FOLDR f e (REVERSE l) = FOLDL (λx y. f y x) e l
   
   [FOLDR_SINGLE]  Theorem
      
      ⊢ ∀f e x. FOLDR f e [x] = f x e
   
   [FOLDR_SNOC]  Theorem
      
      ⊢ ∀f e x l. FOLDR f e (SNOC x l) = FOLDR f (f x e) l
   
   [FRONT_APPEND]  Theorem
      
      ⊢ ∀l1 l2 e. FRONT (l1 ⧺ e::l2) = l1 ⧺ FRONT (e::l2)
   
   [IS_PREFIX]  Theorem
      
      ⊢ (∀l. [] ≼ l ⇔ T) ∧ (∀x l. x::l ≼ [] ⇔ F) ∧
        ∀x1 l1 x2 l2. x2::l2 ≼ x1::l1 ⇔ x1 = x2 ∧ l2 ≼ l1
   
   [IS_PREFIX_ANTISYM]  Theorem
      
      ⊢ ∀x y. x ≼ y ∧ y ≼ x ⇒ x = y
   
   [IS_PREFIX_APPEND]  Theorem
      
      ⊢ ∀l1 l2. l2 ≼ l1 ⇔ ∃l. l1 = l2 ⧺ l
   
   [IS_PREFIX_APPEND1]  Theorem
      
      ⊢ ∀a b c. a ⧺ b ≼ c ⇒ a ≼ c
   
   [IS_PREFIX_APPEND2]  Theorem
      
      ⊢ ∀a b c. a ≼ b ⧺ c ⇒ a ≼ b ∨ b ≼ a
   
   [IS_PREFIX_APPEND3]  Theorem
      
      ⊢ ∀c a. a ≼ a ⧺ c
   
   [IS_PREFIX_APPENDS]  Theorem
      
      ⊢ ∀a b c. a ⧺ b ≼ a ⧺ c ⇔ b ≼ c
   
   [IS_PREFIX_BUTLAST]  Theorem
      
      ⊢ ∀x y. FRONT (x::y) ≼ x::y
   
   [IS_PREFIX_IS_SUBLIST]  Theorem
      
      ⊢ ∀l1 l2. l2 ≼ l1 ⇒ IS_SUBLIST l1 l2
   
   [IS_PREFIX_LENGTH]  Theorem
      
      ⊢ ∀x y. x ≼ y ⇒ LENGTH x ≤ LENGTH y
   
   [IS_PREFIX_LENGTH_ANTI]  Theorem
      
      ⊢ ∀x y. x ≼ y ∧ LENGTH x = LENGTH y ⇔ x = y
   
   [IS_PREFIX_NIL]  Theorem
      
      ⊢ ∀x. [] ≼ x ∧ (x ≼ [] ⇔ x = [])
   
   [IS_PREFIX_PREFIX]  Theorem
      
      ⊢ ∀P l. PREFIX P l ≼ l
   
   [IS_PREFIX_REFL]  Theorem
      
      ⊢ ∀x. x ≼ x
   
   [IS_PREFIX_REVERSE]  Theorem
      
      ⊢ ∀l1 l2. REVERSE l2 ≼ REVERSE l1 ⇔ IS_SUFFIX l1 l2
   
   [IS_PREFIX_SNOC]  Theorem
      
      ⊢ ∀x y z. z ≼ SNOC x y ⇔ z ≼ y ∨ z = SNOC x y
   
   [IS_PREFIX_TRANS]  Theorem
      
      ⊢ ∀x y z. y ≼ x ∧ z ≼ y ⇒ z ≼ x
   
   [IS_SUBLIST_APPEND]  Theorem
      
      ⊢ ∀l1 l2. IS_SUBLIST l1 l2 ⇔ ∃l l'. l1 = l ⧺ (l2 ⧺ l')
   
   [IS_SUBLIST_REVERSE]  Theorem
      
      ⊢ ∀l1 l2. IS_SUBLIST (REVERSE l1) (REVERSE l2) ⇔ IS_SUBLIST l1 l2
   
   [IS_SUFFIX_APPEND]  Theorem
      
      ⊢ ∀l1 l2. IS_SUFFIX l1 l2 ⇔ ∃l. l1 = l ⧺ l2
   
   [IS_SUFFIX_APPEND1]  Theorem
      
      ⊢ ∀l1 l2 l. IS_SUFFIX l2 l ⇒ IS_SUFFIX (l1 ⧺ l2) l
   
   [IS_SUFFIX_CONS]  Theorem
      
      ⊢ ∀l1 l2 a. IS_SUFFIX l1 l2 ⇒ IS_SUFFIX (a::l1) l2
   
   [IS_SUFFIX_CONS2_E]  Theorem
      
      ⊢ ∀s h t. IS_SUFFIX s (h::t) ⇒ IS_SUFFIX s t
   
   [IS_SUFFIX_IS_SUBLIST]  Theorem
      
      ⊢ ∀l1 l2. IS_SUFFIX l1 l2 ⇒ IS_SUBLIST l1 l2
   
   [IS_SUFFIX_REFL]  Theorem
      
      ⊢ ∀l. IS_SUFFIX l l
   
   [IS_SUFFIX_REVERSE]  Theorem
      
      ⊢ ∀l2 l1. IS_SUFFIX (REVERSE l1) (REVERSE l2) ⇔ l2 ≼ l1
   
   [IS_SUFFIX_TRANS]  Theorem
      
      ⊢ ∀l1 l2 l3. IS_SUFFIX l1 l2 ∧ IS_SUFFIX l2 l3 ⇒ IS_SUFFIX l1 l3
   
   [IS_SUFFIX_compute]  Theorem
      
      ⊢ ∀l1 l2. IS_SUFFIX l1 l2 ⇔ REVERSE l2 ≼ REVERSE l1
   
   [LASTN]  Theorem
      
      ⊢ (∀l. LASTN 0 l = []) ∧
        ∀n x l. LASTN (SUC n) (SNOC x l) = SNOC x (LASTN n l)
   
   [LASTN_1]  Theorem
      
      ⊢ ∀l. l ≠ [] ⇒ LASTN 1 l = [LAST l]
   
   [LASTN_APPEND1]  Theorem
      
      ⊢ ∀l2 n.
          LENGTH l2 ≤ n ⇒
          ∀l1. LASTN n (l1 ⧺ l2) = LASTN (n − LENGTH l2) l1 ⧺ l2
   
   [LASTN_APPEND2]  Theorem
      
      ⊢ ∀n l2. n ≤ LENGTH l2 ⇒ ∀l1. LASTN n (l1 ⧺ l2) = LASTN n l2
   
   [LASTN_BUTLASTN]  Theorem
      
      ⊢ ∀n m l.
          n + m ≤ LENGTH l ⇒
          LASTN n (BUTLASTN m l) = BUTLASTN m (LASTN (n + m) l)
   
   [LASTN_CONS]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. LASTN n (x::l) = LASTN n l
   
   [LASTN_DROP]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ LASTN n l = DROP (LENGTH l − n) l
   
   [LASTN_LASTN]  Theorem
      
      ⊢ ∀l n m. m ≤ LENGTH l ⇒ n ≤ m ⇒ LASTN n (LASTN m l) = LASTN n l
   
   [LASTN_LENGTH_APPEND]  Theorem
      
      ⊢ ∀l2 l1. LASTN (LENGTH l2) (l1 ⧺ l2) = l2
   
   [LASTN_LENGTH_ID]  Theorem
      
      ⊢ ∀l. LASTN (LENGTH l) l = l
   
   [LASTN_MAP]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ ∀f. LASTN n (MAP f l) = MAP f (LASTN n l)
   
   [LASTN_REVERSE]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ LASTN n (REVERSE l) = REVERSE (TAKE n l)
   
   [LASTN_SEG]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ LASTN n l = SEG n (LENGTH l − n) l
   
   [LASTN_compute]  Theorem
      
      ⊢ ∀n l.
          LASTN n l =
          (let
             m = LENGTH l
           in
             if n ≤ m then DROP (m − n) l
             else FAIL LASTN $var$(longer than list) n l)
   
   [LAST_LASTN_LAST]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ 0 < n ⇒ LAST (LASTN n l) = LAST l
   
   [LENGTH_BUTLASTN]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (BUTLASTN n l) = LENGTH l − n
   
   [LENGTH_COUNT_LIST]  Theorem
      
      ⊢ ∀n. LENGTH (COUNT_LIST n) = n
   
   [LENGTH_FILTER_LEQ]  Theorem
      
      ⊢ ∀P l. LENGTH (FILTER P l) ≤ LENGTH l
   
   [LENGTH_FILTER_LESS]  Theorem
      
      ⊢ ∀P ls. EXISTS ($¬ ∘ P) ls ⇒ LENGTH (FILTER P ls) < LENGTH ls
   
   [LENGTH_FLAT]  Theorem
      
      ⊢ ∀l. LENGTH (FLAT l) = SUM (MAP LENGTH l)
   
   [LENGTH_FLAT_REPLICATE]  Theorem
      
      ⊢ ∀n. LENGTH (FLAT (REPLICATE n ls)) = n * LENGTH ls
   
   [LENGTH_FOLDL]  Theorem
      
      ⊢ ∀l. LENGTH l = FOLDL (λl' x. SUC l') 0 l
   
   [LENGTH_FOLDR]  Theorem
      
      ⊢ ∀l. LENGTH l = FOLDR (λx l'. SUC l') 0 l
   
   [LENGTH_FRONT]  Theorem
      
      ⊢ ∀l. l ≠ [] ⇒ LENGTH (FRONT l) = PRE (LENGTH l)
   
   [LENGTH_LASTN]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (LASTN n l) = n
   
   [LENGTH_NOT_NULL]  Theorem
      
      ⊢ ∀l. 0 < LENGTH l ⇔ ¬NULL l
   
   [LENGTH_REPLICATE]  Theorem
      
      ⊢ ∀n x. LENGTH (REPLICATE n x) = n
   
   [LENGTH_SCANL]  Theorem
      
      ⊢ ∀f e l. LENGTH (SCANL f e l) = SUC (LENGTH l)
   
   [LENGTH_SCANR]  Theorem
      
      ⊢ ∀f e l. LENGTH (SCANR f e l) = SUC (LENGTH l)
   
   [LENGTH_SEG]  Theorem
      
      ⊢ ∀n k l. n + k ≤ LENGTH l ⇒ LENGTH (SEG n k l) = n
   
   [LENGTH_UNZIP_FST]  Theorem
      
      ⊢ ∀l. LENGTH (UNZIP_FST l) = LENGTH l
   
   [LENGTH_UNZIP_SND]  Theorem
      
      ⊢ ∀l. LENGTH (UNZIP_SND l) = LENGTH l
   
   [LIST_ELEM_COUNT_CARD_EL]  Theorem
      
      ⊢ ∀ls. LIST_ELEM_COUNT x ls = CARD {n | n < LENGTH ls ∧ EL n ls = x}
   
   [LIST_ELEM_COUNT_MEM]  Theorem
      
      ⊢ ∀e l. LIST_ELEM_COUNT e l > 0 ⇔ MEM e l
   
   [LIST_ELEM_COUNT_THM]  Theorem
      
      ⊢ (∀e. LIST_ELEM_COUNT e [] = 0) ∧
        (∀e l1 l2.
           LIST_ELEM_COUNT e (l1 ⧺ l2) =
           LIST_ELEM_COUNT e l1 + LIST_ELEM_COUNT e l2) ∧
        (∀e h l.
           h = e ⇒ LIST_ELEM_COUNT e (h::l) = SUC (LIST_ELEM_COUNT e l)) ∧
        ∀e h l. h ≠ e ⇒ LIST_ELEM_COUNT e (h::l) = LIST_ELEM_COUNT e l
   
   [LIST_REL_APPEND_SING]  Theorem
      
      ⊢ LIST_REL R (l1 ⧺ [x1]) (l2 ⧺ [x2]) ⇔ LIST_REL R l1 l2 ∧ R x1 x2
   
   [LIST_REL_GENLIST]  Theorem
      
      ⊢ LIST_REL P (GENLIST f l) (GENLIST g l) ⇔ ∀i. i < l ⇒ P (f i) (g i)
   
   [LIST_REL_REPLICATE_same]  Theorem
      
      ⊢ LIST_REL P (REPLICATE n x) (REPLICATE n y) ⇔ n > 0 ⇒ P x y
   
   [LIST_REL_REVERSE_EQ]  Theorem
      
      ⊢ LIST_REL R (REVERSE l1) (REVERSE l2) ⇔ LIST_REL R l1 l2
   
   [LIST_TO_SET_EQ_SING]  Theorem
      
      ⊢ ∀x ls. set ls = {x} ⇔ ls ≠ [] ∧ EVERY ($= x) ls
   
   [LUPDATE_APPEND1]  Theorem
      
      ⊢ ∀l1 l2 n x.
          n < LENGTH l1 ⇒ LUPDATE x n (l1 ⧺ l2) = LUPDATE x n l1 ⧺ l2
   
   [LUPDATE_APPEND2]  Theorem
      
      ⊢ ∀l1 l2 n x.
          LENGTH l1 ≤ n ⇒
          LUPDATE x n (l1 ⧺ l2) = l1 ⧺ LUPDATE x (n − LENGTH l1) l2
   
   [MAP_COUNT_LIST]  Theorem
      
      ⊢ MAP f (COUNT_LIST n) = GENLIST f n
   
   [MAP_FILTER]  Theorem
      
      ⊢ ∀f P l.
          (∀x. P (f x) ⇔ P x) ⇒ MAP f (FILTER P l) = FILTER P (MAP f l)
   
   [MAP_FLAT]  Theorem
      
      ⊢ ∀f l. MAP f (FLAT l) = FLAT (MAP (MAP f) l)
   
   [MAP_FOLDL]  Theorem
      
      ⊢ ∀f l. MAP f l = FOLDL (λl' x. SNOC (f x) l') [] l
   
   [MAP_FOLDR]  Theorem
      
      ⊢ ∀f l. MAP f l = FOLDR (λx l'. f x::l') [] l
   
   [MAP_FST_funs]  Theorem
      
      ⊢ MAP (λ(x,y,z). x) funs = MAP FST funs
   
   [MAP_REVERSE]  Theorem
      
      ⊢ ∀f l. MAP f (REVERSE l) = REVERSE (MAP f l)
   
   [MAP_SND_FILTER_NEQ]  Theorem
      
      ⊢ MAP SND (FILTER (λ(x,y). y ≠ z) ls) =
        FILTER (λy. z ≠ y) (MAP SND ls)
   
   [MEM_BUTLASTN]  Theorem
      
      ⊢ ∀l m x. MEM x (BUTLASTN m l) ⇒ MEM x l
   
   [MEM_COUNT_LIST]  Theorem
      
      ⊢ ∀m n. MEM m (COUNT_LIST n) ⇔ m < n
   
   [MEM_DROP_IMP]  Theorem
      
      ⊢ ∀l m x. MEM x (DROP m l) ⇒ MEM x l
   
   [MEM_EXISTS]  Theorem
      
      ⊢ ∀x l. MEM x l ⇔ EXISTS ($= x) l
   
   [MEM_FOLDL]  Theorem
      
      ⊢ ∀y l. MEM y l ⇔ FOLDL (λl' x. l' ∨ y = x) F l
   
   [MEM_FOLDL_MAP]  Theorem
      
      ⊢ ∀x l. MEM x l ⇔ FOLDL $\/ F (MAP ($= x) l)
   
   [MEM_FOLDR]  Theorem
      
      ⊢ ∀y l. MEM y l ⇔ FOLDR (λx l'. y = x ∨ l') F l
   
   [MEM_FOLDR_MAP]  Theorem
      
      ⊢ ∀x l. MEM x l ⇔ FOLDR $\/ F (MAP ($= x) l)
   
   [MEM_FRONT]  Theorem
      
      ⊢ ∀l e y. MEM y (FRONT (e::l)) ⇒ MEM y (e::l)
   
   [MEM_LAST]  Theorem
      
      ⊢ ∀e l. MEM (LAST (e::l)) (e::l)
   
   [MEM_LASTN]  Theorem
      
      ⊢ ∀m l x. MEM x (LASTN m l) ⇒ MEM x l
   
   [MEM_LAST_FRONT]  Theorem
      
      ⊢ ∀e l h. MEM e l ∧ e ≠ LAST (h::l) ⇒ MEM e (FRONT (h::l))
   
   [MEM_REPLICATE]  Theorem
      
      ⊢ ∀n x y. MEM y (REPLICATE n x) ⇔ x = y ∧ 0 < n
   
   [MEM_SEG]  Theorem
      
      ⊢ ∀n m l. n + m ≤ LENGTH l ⇒ ∀x. MEM x (SEG n m l) ⇒ MEM x l
   
   [MEM_SING_APPEND]  Theorem
      
      ⊢ (∀a c. d ≠ a ⧺ [b] ⧺ c) ⇔ ¬MEM b d
   
   [MEM_TAKE]  Theorem
      
      ⊢ ∀l m x. MEM x (TAKE m l) ⇒ MEM x l
   
   [MONOID_APPEND_NIL]  Theorem
      
      ⊢ MONOID $++ []
   
   [NIL_IN_common_prefixes]  Theorem
      
      ⊢ [] ∈ common_prefixes s
   
   [NOT_NIL_SNOC]  Theorem
      
      ⊢ ∀x l. [] ≠ SNOC x l
   
   [NOT_NULL_SNOC]  Theorem
      
      ⊢ ∀x l. ¬NULL (SNOC x l)
   
   [NOT_SNOC_NIL]  Theorem
      
      ⊢ ∀x l. SNOC x l ≠ []
   
   [NULL_FOLDL]  Theorem
      
      ⊢ ∀l. NULL l ⇔ FOLDL (λx l'. F) T l
   
   [NULL_FOLDR]  Theorem
      
      ⊢ ∀l. NULL l ⇔ FOLDR (λx l'. F) T l
   
   [OR_EL_FOLDL]  Theorem
      
      ⊢ ∀l. OR_EL l ⇔ FOLDL $\/ F l
   
   [OR_EL_FOLDR]  Theorem
      
      ⊢ ∀l. OR_EL l ⇔ FOLDR $\/ F l
   
   [PREFIX]  Theorem
      
      ⊢ (∀P. PREFIX P [] = []) ∧
        ∀P x l. PREFIX P (x::l) = if P x then x::PREFIX P l else []
   
   [PREFIX_FOLDR]  Theorem
      
      ⊢ ∀P l. PREFIX P l = FOLDR (λx l'. if P x then x::l' else []) [] l
   
   [REPLICATE_APPEND]  Theorem
      
      ⊢ REPLICATE n a ⧺ REPLICATE m a = REPLICATE (n + m) a
   
   [REPLICATE_GENLIST]  Theorem
      
      ⊢ ∀n x. REPLICATE n x = GENLIST (K x) n
   
   [REPLICATE_NIL]  Theorem
      
      ⊢ REPLICATE x y = [] ⇔ x = 0
   
   [REPLICATE_compute]  Theorem
      
      ⊢ (∀x. REPLICATE 0 x = []) ∧
        (∀n x.
           REPLICATE (NUMERAL (BIT1 n)) x =
           x::REPLICATE (NUMERAL (BIT1 n) − 1) x) ∧
        ∀n x.
          REPLICATE (NUMERAL (BIT2 n)) x =
          x::REPLICATE (NUMERAL (BIT1 n)) x
   
   [REVERSE_DROP]  Theorem
      
      ⊢ ∀ls n.
          n ≤ LENGTH ls ⇒
          REVERSE (DROP n ls) = REVERSE (LASTN (LENGTH ls − n) ls)
   
   [REVERSE_FLAT]  Theorem
      
      ⊢ ∀l. REVERSE (FLAT l) = FLAT (REVERSE (MAP REVERSE l))
   
   [REVERSE_FOLDL]  Theorem
      
      ⊢ ∀l. REVERSE l = FOLDL (λl' x. x::l') [] l
   
   [REVERSE_FOLDR]  Theorem
      
      ⊢ ∀l. REVERSE l = FOLDR SNOC [] l
   
   [REVERSE_REPLICATE]  Theorem
      
      ⊢ ∀n x. REVERSE (REPLICATE n x) = REPLICATE n x
   
   [REVERSE_ZIP]  Theorem
      
      ⊢ ∀l1 l2.
          LENGTH l1 = LENGTH l2 ⇒
          REVERSE (ZIP (l1,l2)) = ZIP (REVERSE l1,REVERSE l2)
   
   [SEG1]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ SEG 1 n l = [EL n l]
   
   [SEG_0_SNOC]  Theorem
      
      ⊢ ∀m l x. m ≤ LENGTH l ⇒ SEG m 0 (SNOC x l) = SEG m 0 l
   
   [SEG_APPEND]  Theorem
      
      ⊢ ∀m l1 n l2.
          m < LENGTH l1 ∧ LENGTH l1 ≤ n + m ∧ n + m ≤ LENGTH l1 + LENGTH l2 ⇒
          SEG n m (l1 ⧺ l2) =
          SEG (LENGTH l1 − m) m l1 ⧺ SEG (n + m − LENGTH l1) 0 l2
   
   [SEG_APPEND1]  Theorem
      
      ⊢ ∀n m l1. n + m ≤ LENGTH l1 ⇒ ∀l2. SEG n m (l1 ⧺ l2) = SEG n m l1
   
   [SEG_APPEND2]  Theorem
      
      ⊢ ∀l1 m n l2.
          LENGTH l1 ≤ m ∧ n ≤ LENGTH l2 ⇒
          SEG n m (l1 ⧺ l2) = SEG n (m − LENGTH l1) l2
   
   [SEG_CONS]  Theorem
      
      ⊢ ∀j n h t.
          0 < j ∧ n + j ≤ LENGTH t + 1 ⇒ SEG n j (h::t) = SEG n (j − 1) t
   
   [SEG_LASTN_BUTLASTN]  Theorem
      
      ⊢ ∀n m l.
          n + m ≤ LENGTH l ⇒
          SEG n m l = LASTN n (BUTLASTN (LENGTH l − (n + m)) l)
   
   [SEG_LENGTH_ID]  Theorem
      
      ⊢ ∀l. SEG (LENGTH l) 0 l = l
   
   [SEG_LENGTH_SNOC]  Theorem
      
      ⊢ ∀l x. SEG 1 (LENGTH l) (SNOC x l) = [x]
   
   [SEG_REVERSE]  Theorem
      
      ⊢ ∀n m l.
          n + m ≤ LENGTH l ⇒
          SEG n m (REVERSE l) = REVERSE (SEG n (LENGTH l − (n + m)) l)
   
   [SEG_SEG]  Theorem
      
      ⊢ ∀n1 m1 n2 m2 l.
          n1 + m1 ≤ LENGTH l ∧ n2 + m2 ≤ n1 ⇒
          SEG n2 m2 (SEG n1 m1 l) = SEG n2 (m1 + m2) l
   
   [SEG_SNOC]  Theorem
      
      ⊢ ∀n m l. n + m ≤ LENGTH l ⇒ ∀x. SEG n m (SNOC x l) = SEG n m l
   
   [SEG_SUC_CONS]  Theorem
      
      ⊢ ∀m n l x. SEG m (SUC n) (x::l) = SEG m n l
   
   [SEG_SUC_EL]  Theorem
      
      ⊢ ∀n i l.
          i + n < LENGTH l ⇒ SEG (SUC n) i l = EL i l::SEG n (i + 1) l
   
   [SEG_TAKE_DROP]  Theorem
      
      ⊢ ∀n m l. n + m ≤ LENGTH l ⇒ SEG n m l = TAKE n (DROP m l)
   
   [SEG_compute]  Theorem
      
      ⊢ (∀k l. SEG 0 k l = []) ∧
        (∀m x l.
           SEG (NUMERAL (BIT1 m)) 0 (x::l) =
           x::SEG (NUMERAL (BIT1 m) − 1) 0 l) ∧
        (∀m x l.
           SEG (NUMERAL (BIT2 m)) 0 (x::l) = x::SEG (NUMERAL (BIT1 m)) 0 l) ∧
        (∀m k x l.
           SEG (NUMERAL (BIT1 m)) (NUMERAL (BIT1 k)) (x::l) =
           SEG (NUMERAL (BIT1 m)) (NUMERAL (BIT1 k) − 1) l) ∧
        (∀m k x l.
           SEG (NUMERAL (BIT2 m)) (NUMERAL (BIT1 k)) (x::l) =
           SEG (NUMERAL (BIT2 m)) (NUMERAL (BIT1 k) − 1) l) ∧
        (∀m k x l.
           SEG (NUMERAL (BIT1 m)) (NUMERAL (BIT2 k)) (x::l) =
           SEG (NUMERAL (BIT1 m)) (NUMERAL (BIT1 k)) l) ∧
        ∀m k x l.
          SEG (NUMERAL (BIT2 m)) (NUMERAL (BIT2 k)) (x::l) =
          SEG (NUMERAL (BIT2 m)) (NUMERAL (BIT1 k)) l
   
   [SNOC_EL_TAKE]  Theorem
      
      ⊢ ∀n l. n < LENGTH l ⇒ SNOC (EL n l) (TAKE n l) = TAKE (SUC n) l
   
   [SNOC_EQ_LENGTH_EQ]  Theorem
      
      ⊢ ∀x1 l1 x2 l2. SNOC x1 l1 = SNOC x2 l2 ⇒ LENGTH l1 = LENGTH l2
   
   [SNOC_FOLDR]  Theorem
      
      ⊢ ∀x l. SNOC x l = FOLDR CONS [x] l
   
   [SNOC_REPLICATE]  Theorem
      
      ⊢ ∀n x. SNOC x (REPLICATE n x) = REPLICATE (SUC n) x
   
   [SNOC_REVERSE_CONS]  Theorem
      
      ⊢ ∀x l. SNOC x l = REVERSE (x::REVERSE l)
   
   [SPLITP_APPEND]  Theorem
      
      ⊢ ∀l1 l2.
          SPLITP P (l1 ⧺ l2) =
          if EXISTS P l1 then (FST (SPLITP P l1),SND (SPLITP P l1) ⧺ l2)
          else (l1 ⧺ FST (SPLITP P l2),SND (SPLITP P l2))
   
   [SPLITP_EVERY]  Theorem
      
      ⊢ ∀P l. EVERY (λx. ¬P x) l ⇒ SPLITP P l = (l,[])
   
   [SPLITP_IMP]  Theorem
      
      ⊢ ∀P ls l r.
          SPLITP P ls = (l,r) ⇒ EVERY ($¬ ∘ P) l ∧ (¬NULL r ⇒ P (HD r))
   
   [SPLITP_JOIN]  Theorem
      
      ⊢ ∀ls l r. SPLITP P ls = (l,r) ⇒ ls = l ⧺ r
   
   [SPLITP_LENGTH]  Theorem
      
      ⊢ ∀l. LENGTH (FST (SPLITP P l)) + LENGTH (SND (SPLITP P l)) =
            LENGTH l
   
   [SPLITP_NIL_FST_IMP]  Theorem
      
      ⊢ ∀ls r. SPLITP P ls = ([],r) ⇒ r = ls
   
   [SPLITP_NIL_SND_EVERY]  Theorem
      
      ⊢ ∀ls r. SPLITP P ls = (r,[]) ⇔ r = ls ∧ EVERY ($¬ ∘ P) ls
   
   [SPLITP_compute]  Theorem
      
      ⊢ SPLITP = SPLITP_AUX []
   
   [SPLITP_splitAtPki]  Theorem
      
      ⊢ SPLITP P = splitAtPki (K P) $,
   
   [SUM_FLAT]  Theorem
      
      ⊢ ∀l. SUM (FLAT l) = SUM (MAP SUM l)
   
   [SUM_FOLDL]  Theorem
      
      ⊢ ∀l. SUM l = FOLDL $+ 0 l
   
   [SUM_FOLDR]  Theorem
      
      ⊢ ∀l. SUM l = FOLDR $+ 0 l
   
   [SUM_REPLICATE]  Theorem
      
      ⊢ ∀n k. SUM (REPLICATE n k) = n * k
   
   [SUM_REVERSE]  Theorem
      
      ⊢ ∀l. SUM (REVERSE l) = SUM l
   
   [TAKE]  Theorem
      
      ⊢ (∀l. TAKE 0 l = []) ∧ ∀n x l. TAKE (SUC n) (x::l) = x::TAKE n l
   
   [TAKE_APPEND]  Theorem
      
      ⊢ ∀n l1 l2. TAKE n (l1 ⧺ l2) = TAKE n l1 ⧺ TAKE (n − LENGTH l1) l2
   
   [TAKE_APPEND1]  Theorem
      
      ⊢ ∀n l1. n ≤ LENGTH l1 ⇒ ∀l2. TAKE n (l1 ⧺ l2) = TAKE n l1
   
   [TAKE_APPEND2]  Theorem
      
      ⊢ ∀l1 n.
          LENGTH l1 ≤ n ⇒
          ∀l2. TAKE n (l1 ⧺ l2) = l1 ⧺ TAKE (n − LENGTH l1) l2
   
   [TAKE_BUTLASTN]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n l = BUTLASTN (LENGTH l − n) l
   
   [TAKE_EL_SNOC]  Theorem
      
      ⊢ ∀ls n. n < LENGTH ls ⇒ TAKE (n + 1) ls = SNOC (EL n ls) (TAKE n ls)
   
   [TAKE_LENGTH_APPEND]  Theorem
      
      ⊢ ∀l1 l2. TAKE (LENGTH l1) (l1 ⧺ l2) = l1
   
   [TAKE_PRE_LENGTH]  Theorem
      
      ⊢ ∀ls. ls ≠ [] ⇒ TAKE (PRE (LENGTH ls)) ls = FRONT ls
   
   [TAKE_REVERSE]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n (REVERSE l) = REVERSE (LASTN n l)
   
   [TAKE_SEG]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n l = SEG n 0 l
   
   [TAKE_SEG_DROP]  Theorem
      
      ⊢ ∀n i l.
          i + n ≤ LENGTH l ⇒ TAKE i l ⧺ SEG n i l ⧺ DROP (i + n) l = l
   
   [TAKE_SNOC]  Theorem
      
      ⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. TAKE n (SNOC x l) = TAKE n l
   
   [TAKE_TAKE]  Theorem
      
      ⊢ ∀m l. m ≤ LENGTH l ⇒ ∀n. n ≤ m ⇒ TAKE n (TAKE m l) = TAKE n l
   
   [TAKE_TAKE_T]  Theorem
      
      ⊢ ∀m l n. n ≤ m ⇒ TAKE n (TAKE m l) = TAKE n l
   
   [TL_SNOC]  Theorem
      
      ⊢ ∀x l. TL (SNOC x l) = if NULL l then [] else SNOC x (TL l)
   
   [UNIQUE_LIST_ELEM_COUNT]  Theorem
      
      ⊢ ∀e L. UNIQUE e L ⇔ LIST_ELEM_COUNT e L = 1
   
   [UNZIP_SNOC]  Theorem
      
      ⊢ ∀x l.
          UNZIP (SNOC x l) =
          (SNOC (FST x) (FST (UNZIP l)),SNOC (SND x) (SND (UNZIP l)))
   
   [ZIP_APPEND]  Theorem
      
      ⊢ ∀a b c d.
          LENGTH a = LENGTH b ∧ LENGTH c = LENGTH d ⇒
          ZIP (a,b) ⧺ ZIP (c,d) = ZIP (a ⧺ c,b ⧺ d)
   
   [ZIP_COUNT_LIST]  Theorem
      
      ⊢ n = LENGTH l1 ⇒
        ZIP (l1,COUNT_LIST n) = GENLIST (λn. (EL n l1,n)) (LENGTH l1)
   
   [ZIP_SNOC]  Theorem
      
      ⊢ ∀l1 l2.
          LENGTH l1 = LENGTH l2 ⇒
          ∀x1 x2. ZIP (SNOC x1 l1,SNOC x2 l2) = SNOC (x1,x2) (ZIP (l1,l2))
   
   [ZIP_TAKE]  Theorem
      
      ⊢ ∀n a b.
          n ≤ LENGTH a ∧ LENGTH a = LENGTH b ⇒
          ZIP (TAKE n a,TAKE n b) = TAKE n (ZIP (a,b))
   
   [ZIP_TAKE_LEQ]  Theorem
      
      ⊢ ∀n a b.
          n ≤ LENGTH a ∧ LENGTH a ≤ LENGTH b ⇒
          ZIP (TAKE n a,TAKE n b) = TAKE n (ZIP (a,TAKE (LENGTH a) b))
   
   [all_distinct_count_list]  Theorem
      
      ⊢ ∀n. ALL_DISTINCT (COUNT_LIST n)
   
   [common_prefixes_BIGINTER]  Theorem
      
      ⊢ common_prefixes s = BIGINTER (IMAGE (λl. {p | p ≼ l}) s)
   
   [common_prefixes_NIL]  Theorem
      
      ⊢ [] ∈ s ⇒ common_prefixes s = {[]}
   
   [common_prefixes_NONEMPTY]  Theorem
      
      ⊢ common_prefixes s ≠ ∅
   
   [common_prefixes_PAIR]  Theorem
      
      ⊢ common_prefixes {[]; x} = {[]} ∧ common_prefixes {x; []} = {[]} ∧
        common_prefixes {a::xs; b::ys} =
        [] INSERT
        if a = b then IMAGE (CONS a) (common_prefixes {xs; ys}) else ∅
   
   [count_list_sub1]  Theorem
      
      ⊢ ∀n. n ≠ 0 ⇒ COUNT_LIST n = 0::MAP SUC (COUNT_LIST (n − 1))
   
   [el_map_count]  Theorem
      
      ⊢ ∀n f m. n < m ⇒ EL n (MAP f (COUNT_LIST m)) = f n
   
   [every_count_list]  Theorem
      
      ⊢ ∀P n. EVERY P (COUNT_LIST n) ⇔ ∀m. m < n ⇒ P m
   
   [is_prefix_el]  Theorem
      
      ⊢ ∀n l1 l2.
          l1 ≼ l2 ∧ n < LENGTH l1 ∧ n < LENGTH l2 ⇒ EL n l1 = EL n l2
   
   [list_rel_butlastn]  Theorem
      
      ⊢ ∀f l1 l2 n.
          n ≤ LENGTH l1 ∧ LIST_REL f l1 l2 ⇒
          LIST_REL f (BUTLASTN n l1) (BUTLASTN n l2)
   
   [list_rel_lastn]  Theorem
      
      ⊢ ∀f l1 l2 n.
          n ≤ LENGTH l1 ∧ LIST_REL f l1 l2 ⇒
          LIST_REL f (LASTN n l1) (LASTN n l2)
   
   [longest_prefix_EMPTY]  Theorem
      
      ⊢ longest_prefix ∅ = []
   
   [longest_prefix_NIL]  Theorem
      
      ⊢ [] ∈ s ⇒ longest_prefix s = []
   
   [longest_prefix_PAIR]  Theorem
      
      ⊢ longest_prefix {[]; ys} = [] ∧ longest_prefix {xs; []} = [] ∧
        longest_prefix {x::xs; y::ys} =
        if x = y then x::longest_prefix {xs; ys} else []
   
   [longest_prefix_SING]  Theorem
      
      ⊢ longest_prefix {s} = s
   
   [longest_prefix_UNIQUE]  Theorem
      
      ⊢ s ≠ ∅ ∧ is_measure_maximal LENGTH (common_prefixes s) x ∧
        is_measure_maximal LENGTH (common_prefixes s) y ⇒
        x = y
   
   [map_replicate]  Theorem
      
      ⊢ ∀f n x. MAP f (REPLICATE n x) = REPLICATE n (f x)
   
   [nub_GENLIST]  Theorem
      
      ⊢ nub (GENLIST f n) =
        MAP f (FILTER (λi. ∀j. i < j ∧ j < n ⇒ f i ≠ f j) (COUNT_LIST n))
   
   [prefixes_is_prefix_total]  Theorem
      
      ⊢ ∀l l1 l2. l1 ≼ l ∧ l2 ≼ l ⇒ l1 ≼ l2 ∨ l2 ≼ l1
   
   [take_drop_partition]  Theorem
      
      ⊢ ∀n m l. m ≤ n ⇒ TAKE m l ⧺ TAKE (n − m) (DROP m l) = TAKE n l
   
   [two_common_prefixes]  Theorem
      
      ⊢ s ≠ ∅ ∧ p1 ∈ common_prefixes s ∧ p2 ∈ common_prefixes s ⇒
        p1 ≼ p2 ∨ p2 ≼ p1
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14