Structure rich_listTheory
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 DELETE_ELEMENT : thm
val ELL : thm
val IS_SUBLIST : thm
val IS_SUFFIX : thm
val LASTN_def : thm
val LIST_ELEM_COUNT_DEF : thm
val MAX_LIST_def : thm
val MIN_LIST_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 chunks_tr_def : thm
val common_prefixes_def : thm
val longest_prefix_def : thm
(* Theorems *)
val ALL_DISTINCT_APPEND_3 : thm
val ALL_DISTINCT_EL_APPEND : thm
val ALL_DISTINCT_FRONT : thm
val ALL_DISTINCT_LAST_EL_IFF : thm
val ALL_DISTINCT_MEM_ZIP_MAP : thm
val ALL_DISTINCT_SNOC : thm
val ALL_DISTINCT_SWAP : thm
val ALL_DISTINCT_TAKE : thm
val ALL_DISTINCT_TAKE_DROP : 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_MAP : thm
val ALL_EL_REPLICATE : thm
val ALL_EL_REVERSE : thm
val ALL_EL_SEG : thm
val ALL_EL_SNOC : thm
val AND_EL_FOLDL : thm
val AND_EL_FOLDR : thm
val APPEND : thm
val APPEND_11_LENGTH : thm
val APPEND_ASSOC : thm
val APPEND_ASSOC_CONS : thm
val APPEND_BUTLASTN_BUTFIRSTN : thm
val APPEND_BUTLASTN_DROP : thm
val APPEND_BUTLASTN_LASTN : thm
val APPEND_BUTLAST_LAST : thm
val APPEND_EQ_APPEND_EQ : thm
val APPEND_FIRSTN_BUTFIRSTN : thm
val APPEND_FIRSTN_LASTN : thm
val APPEND_FOLDL : thm
val APPEND_FOLDR : thm
val APPEND_LENGTH_EQ : thm
val APPEND_NIL : thm
val APPEND_SNOC : 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 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 : thm
val BUTLASTN_1 : thm
val BUTLASTN_APPEND1 : thm
val BUTLASTN_APPEND2 : thm
val BUTLASTN_BUTLAST : thm
val BUTLASTN_BUTLASTN : thm
val BUTLASTN_CONS : thm
val BUTLASTN_FIRSTN : 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_BUTLAST : thm
val BUTLASTN_SUC_FRONT : thm
val BUTLASTN_TAKE : thm
val BUTLASTN_TAKE_UNCOND : thm
val BUTLASTN_compute : thm
val BUTLAST_CONS : 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 : thm
val CONS_11 : 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 DELETE_ELEMENT_APPEND : thm
val DELETE_ELEMENT_FILTER : thm
val DISTINCT_LIST_TO_SET_EQ_SING : thm
val DROP : thm
val DROP_1 : thm
val DROP_1_APPEND : thm
val DROP_APPEND : thm
val DROP_APPEND1 : thm
val DROP_APPEND2 : thm
val DROP_BY_DROP_SUC : 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_HEAD_ELEMENT : thm
val DROP_LASTN : thm
val DROP_LENGTH_APPEND : thm
val DROP_LENGTH_NIL : thm
val DROP_LENGTH_NIL_rwt : thm
val DROP_PREn_LAST_CONS : thm
val DROP_REPLICATE : thm
val DROP_REVERSE : thm
val DROP_SEG : thm
val DROP_SNOC : thm
val DROP_SUC : thm
val DROP_TAKE_EQ_NIL : thm
val EL : thm
val ELL_0_SNOC : thm
val ELL_APPEND1 : thm
val ELL_APPEND2 : thm
val ELL_CONS : thm
val ELL_EL : thm
val ELL_IS_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_APPEND : thm
val EL_APPEND1 : thm
val EL_APPEND2 : thm
val EL_BUTFIRSTN : thm
val EL_CONS : thm
val EL_COUNT_LIST : thm
val EL_DROP : thm
val EL_ELL : thm
val EL_FIRSTN : thm
val EL_FRONT : thm
val EL_GENLIST : thm
val EL_IS_EL : thm
val EL_LENGTH_APPEND : thm
val EL_LENGTH_APPEND_0 : thm
val EL_LENGTH_APPEND_1 : thm
val EL_LENGTH_APPEND_rwt : thm
val EL_LENGTH_SNOC : thm
val EL_MAP : thm
val EL_MEM : thm
val EL_PRE_LENGTH : thm
val EL_REPLICATE : thm
val EL_REVERSE : thm
val EL_REVERSE_ELL : thm
val EL_SEG : thm
val EL_SNOC : thm
val EL_SPLIT : thm
val EL_SPLIT_2 : thm
val EL_TAIL : thm
val EL_TAKE : thm
val EL_chunks : thm
val EQ_LIST : 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_DELETE_ELEMENT : 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_GENLIST : 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_GENLIST : 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 : thm
val FILTER_APPEND : thm
val FILTER_COMM : thm
val FILTER_EL_IFF : thm
val FILTER_EL_IMP : thm
val FILTER_EL_NEXT : thm
val FILTER_EL_NEXT_IFF : thm
val FILTER_EQ : thm
val FILTER_FILTER : thm
val FILTER_FLAT : thm
val FILTER_FOLDL : thm
val FILTER_FOLDR : thm
val FILTER_HD : thm
val FILTER_HD_IFF : thm
val FILTER_IDEM : thm
val FILTER_LAST : thm
val FILTER_LAST_IFF : thm
val FILTER_MAP : thm
val FILTER_MONO_DEC : thm
val FILTER_MONO_INC : thm
val FILTER_REVERSE : thm
val FILTER_SNOC : thm
val FILTER_sublist : thm
val FINITE_common_prefixes : thm
val FINITE_prefix : 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 FLAT_FLAT : thm
val FLAT_FOLDL : thm
val FLAT_FOLDR : thm
val FLAT_REVERSE : thm
val FLAT_SNOC : thm
val FLAT_chunks : thm
val FOLDL : thm
val FOLDL_APPEND : thm
val FOLDL_CONG_invariant : 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 : thm
val FOLDL_SNOC_NIL : thm
val FOLDR : 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 FRONT_APPEND_NOT_NIL : thm
val FRONT_BY_TAKE : thm
val FRONT_EL : thm
val FRONT_EQ_NIL : thm
val FRONT_LENGTH : thm
val FRONT_NON_NIL : thm
val FRONT_SING : thm
val GENLIST : thm
val GENLIST_APPEND : thm
val GENLIST_CONS : thm
val GENLIST_FUN_EQ : thm
val GENLIST_K_ADD : thm
val GENLIST_K_APPEND : thm
val GENLIST_K_APPEND_K : thm
val GENLIST_K_CONS : thm
val GENLIST_K_LESS : thm
val GENLIST_K_MEM : thm
val GENLIST_K_RANGE : thm
val GENLIST_K_SET : thm
val HD : thm
val HD_APPEND : thm
val HD_APPEND_NOT_NIL : thm
val HD_GENLIST : thm
val HEAD_MEM : 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 IS_PREFIX : thm
val IS_PREFIX_ALL_DISTINCT : 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_BUTLAST' : thm
val IS_PREFIX_EQ_REWRITE : thm
val IS_PREFIX_EQ_TAKE : thm
val IS_PREFIX_EQ_TAKE' : thm
val IS_PREFIX_FRONT_CASES : thm
val IS_PREFIX_FRONT_MONO : thm
val IS_PREFIX_GENLIST : thm
val IS_PREFIX_IMP_TAKE : 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_ALL_DISTINCT : 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_EQ_DROP : thm
val IS_SUFFIX_EQ_DROP' : thm
val IS_SUFFIX_IMP_DROP : thm
val IS_SUFFIX_IMP_LASTN : 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 IS_SUFFIX_dropWhile : thm
val ITSET_TO_FOLDR : thm
val LAST : thm
val LASTN : thm
val LASTN_1 : thm
val LASTN_APPEND1 : thm
val LASTN_APPEND2 : thm
val LASTN_BUTFIRSTN : thm
val LASTN_BUTLASTN : thm
val LASTN_CONS : thm
val LASTN_DROP : thm
val LASTN_DROP_UNCOND : 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_APPEND : thm
val LAST_APPEND_NOT_NIL : thm
val LAST_CONS : thm
val LAST_EL_CONS : thm
val LAST_EQ_HD : thm
val LAST_LASTN_LAST : thm
val LAST_MEM : thm
val LENGTH : thm
val LENGTH_APPEND : thm
val LENGTH_BUTFIRSTN : thm
val LENGTH_BUTLAST : thm
val LENGTH_BUTLASTN : thm
val LENGTH_CONS : thm
val LENGTH_COUNT_LIST : thm
val LENGTH_DELETE_ELEMENT_LE : thm
val LENGTH_DELETE_ELEMENT_LEQ : thm
val LENGTH_EQ_NIL : thm
val LENGTH_FILTER_LEQ : thm
val LENGTH_FILTER_LESS : thm
val LENGTH_FIRSTN : thm
val LENGTH_FLAT : thm
val LENGTH_FLAT_REPLICATE : thm
val LENGTH_FOLDL : thm
val LENGTH_FOLDR : thm
val LENGTH_FRONT : thm
val LENGTH_GENLIST : thm
val LENGTH_LASTN : thm
val LENGTH_MAP : thm
val LENGTH_NIL : thm
val LENGTH_NOT_NULL : thm
val LENGTH_REPLICATE : thm
val LENGTH_REVERSE : thm
val LENGTH_SCANL : thm
val LENGTH_SCANR : thm
val LENGTH_SEG : thm
val LENGTH_SING : thm
val LENGTH_SNOC : thm
val LENGTH_TAKE_LE : thm
val LENGTH_TL_LT : thm
val LENGTH_UNZIP_FST : thm
val LENGTH_UNZIP_SND : thm
val LENGTH_ZIP : thm
val LENGTH_chunks : thm
val LENGTH_dropWhile_id : thm
val LIST_ELEM_COUNT_CARD_EL : thm
val LIST_ELEM_COUNT_MEM : thm
val LIST_ELEM_COUNT_THM : thm
val LIST_EQ_HEAD_TAIL : thm
val LIST_HEAD_TAIL : thm
val LIST_NOT_EQ : 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_SING_EQ : thm
val LIST_TO_SET_EQ_SING : thm
val LIST_TO_SET_PREFIX : thm
val LIST_TO_SET_SING_IFF : thm
val LIST_TO_SET_SUFFIX : thm
val LUPDATE_APPEND1 : thm
val LUPDATE_APPEND2 : thm
val MAP : thm
val MAP2 : thm
val MAP2_MAP_MAP : thm
val MAP2_ZIP : thm
val MAP_APPEND : thm
val MAP_COUNT_LIST : thm
val MAP_EQ_f : thm
val MAP_FILTER : thm
val MAP_FLAT : thm
val MAP_FOLDL : thm
val MAP_FOLDR : thm
val MAP_FST_funs : thm
val MAP_GENLIST : thm
val MAP_HD : thm
val MAP_MAP_o : thm
val MAP_REVERSE : thm
val MAP_SING : thm
val MAP_SND_FILTER_NEQ : thm
val MAP_SNOC : thm
val MAP_SUBLIST : thm
val MAP_o : thm
val MAX_LIST_CONS : thm
val MAX_LIST_EQ_0 : thm
val MAX_LIST_LE : thm
val MAX_LIST_MAP_LE : thm
val MAX_LIST_MEM : thm
val MAX_LIST_MONO_DEC : thm
val MAX_LIST_MONO_INC : thm
val MAX_LIST_NIL : thm
val MAX_LIST_PROPERTY : thm
val MAX_LIST_SING : thm
val MAX_LIST_TEST : thm
val MEM_APPEND_3 : 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_FRONT_NOT_LAST : thm
val MEM_FRONT_NOT_NIL : thm
val MEM_LAST : thm
val MEM_LASTN : thm
val MEM_LAST_FRONT : thm
val MEM_LAST_NOT_NIL : thm
val MEM_REPLICATE : thm
val MEM_SEG : thm
val MEM_SING_APPEND : thm
val MEM_SPLIT_APPEND_distinct : thm
val MEM_SPLIT_TAKE_DROP_distinct : thm
val MEM_SPLIT_TAKE_DROP_first : thm
val MEM_SPLIT_TAKE_DROP_last : thm
val MEM_TAKE : thm
val MIN_LIST_CONS : thm
val MIN_LIST_LE : thm
val MIN_LIST_LE_MAX_LIST : thm
val MIN_LIST_MAP_LE : thm
val MIN_LIST_MEM : thm
val MIN_LIST_MONO_DEC : thm
val MIN_LIST_MONO_INC : thm
val MIN_LIST_PROPERTY : thm
val MIN_LIST_SING : thm
val MIN_LIST_TEST : thm
val MONOID_APPEND_NIL : thm
val MONOLIST_EQ : thm
val MONOLIST_SET_SING : thm
val MONO_DEC_CONS : thm
val MONO_DEC_HD : thm
val MONO_DEC_NIL : thm
val MONO_INC_CONS : thm
val MONO_INC_HD : thm
val MONO_INC_NIL : thm
val NIL_IN_common_prefixes : thm
val NIL_NO_MEM : thm
val NON_MONO_TAIL_PROPERTY : thm
val NOT_ALL_EL_SOME_EL : thm
val NOT_CONS_NIL : thm
val NOT_EQ_LIST : thm
val NOT_IN_DELETE_ELEMENT : thm
val NOT_NIL_CONS : thm
val NOT_NIL_SNOC : thm
val NOT_NULL_SNOC : thm
val NOT_SNOC_NIL : thm
val NOT_SOME_EL_ALL_EL : thm
val NULL : thm
val NULL_DEF : thm
val NULL_EQ_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_EQ_CONS : thm
val REPLICATE_GENLIST : thm
val REPLICATE_NIL : thm
val REPLICATE_compute : thm
val REVERSE_APPEND : thm
val REVERSE_DROP : thm
val REVERSE_EQ_NIL : thm
val REVERSE_FLAT : thm
val REVERSE_FOLDL : thm
val REVERSE_FOLDR : thm
val REVERSE_HD : thm
val REVERSE_REPLICATE : thm
val REVERSE_REVERSE : thm
val REVERSE_SING : thm
val REVERSE_SNOC : thm
val REVERSE_TL : 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 SING_LIST_TO_SET : thm
val SNOC : thm
val SNOC_11 : thm
val SNOC_ACYCLIC : thm
val SNOC_APPEND : thm
val SNOC_Axiom : thm
val SNOC_CASES : thm
val SNOC_EL_FIRSTN : thm
val SNOC_EL_TAKE : thm
val SNOC_EQ_LENGTH_EQ : thm
val SNOC_FOLDR : thm
val SNOC_INDUCT : thm
val SNOC_LASTN : thm
val SNOC_LAST_FRONT' : thm
val SNOC_REPLICATE : thm
val SNOC_REVERSE_CONS : 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 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 : thm
val SUM_APPEND : thm
val SUM_FLAT : thm
val SUM_FOLDL : thm
val SUM_FOLDR : thm
val SUM_IMAGE_count_MULT : thm
val SUM_IMAGE_count_SUM_GENLIST : thm
val SUM_REPLICATE : thm
val SUM_REVERSE : thm
val SUM_SNOC : thm
val SUM_SUBLIST : thm
val TAIL_BY_DROP : thm
val TAKE : thm
val TAKE_1_APPEND : thm
val TAKE_APPEND : thm
val TAKE_APPEND1 : thm
val TAKE_APPEND2 : thm
val TAKE_BUTLASTN : thm
val TAKE_DROP_SUC : thm
val TAKE_DROP_SWAP : thm
val TAKE_EL_SNOC : thm
val TAKE_FRONT : thm
val TAKE_LENGTH_APPEND : thm
val TAKE_LENGTH_APPEND2 : 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_SUC : thm
val TAKE_SUC_BY_TAKE : thm
val TAKE_TAKE : thm
val TAKE_TAKE_T : thm
val TL : thm
val TL_DROP : thm
val TL_GENLIST : thm
val TL_SNOC : thm
val UNIQUE_LIST_ELEM_COUNT : thm
val UNZIP : thm
val UNZIP_SNOC : thm
val UNZIP_ZIP : thm
val ZIP : thm
val ZIP_APPEND : thm
val ZIP_COUNT_LIST : thm
val ZIP_FIRSTN : thm
val ZIP_FIRSTN_LEQ : thm
val ZIP_GENLIST : thm
val ZIP_MAP_MAP : thm
val ZIP_SNOC : thm
val ZIP_TAKE : thm
val ZIP_TAKE_LEQ : thm
val ZIP_UNZIP : thm
val all_distinct_count_list : thm
val all_distinct_list_el_inj : thm
val chunks_0 : thm
val chunks_MAP : thm
val chunks_NIL : thm
val chunks_TAKE : thm
val chunks_ZIP : thm
val chunks_append_divides : thm
val chunks_def : thm
val chunks_ind : thm
val chunks_length : thm
val chunks_not_nil : thm
val chunks_tr_aux_def : thm
val chunks_tr_aux_ind : thm
val chunks_tr_aux_thm : thm
val chunks_tr_thm : 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 divides_EVERY_LENGTH_chunks : 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 list_to_set_eq_el_image : 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 set_list_eq_count : thm
val sublist_ALL_DISTINCT : thm
val sublist_MONO_DEC : thm
val sublist_MONO_INC : thm
val sublist_antisym : thm
val sublist_append_extend : thm
val sublist_append_if : thm
val sublist_append_iff : thm
val sublist_append_include : thm
val sublist_append_only_if : thm
val sublist_append_pair : thm
val sublist_append_prefix : thm
val sublist_append_remove : thm
val sublist_append_suffix : thm
val sublist_cons : thm
val sublist_cons_eq : thm
val sublist_cons_include : thm
val sublist_cons_remove : thm
val sublist_def : thm
val sublist_drop : thm
val sublist_every : thm
val sublist_front : thm
val sublist_head_sing : thm
val sublist_ind : thm
val sublist_induct : thm
val sublist_last_sing : thm
val sublist_length : thm
val sublist_mem : thm
val sublist_member_sing : thm
val sublist_nil : thm
val sublist_of_nil : thm
val sublist_order : thm
val sublist_prefix : thm
val sublist_prefix_nil : thm
val sublist_refl : thm
val sublist_snoc : thm
val sublist_subset : thm
val sublist_suffix : thm
val sublist_tail : thm
val sublist_take : thm
val sublist_trans : thm
val sum_of_sums : thm
val take_drop_partition : thm
val two_common_prefixes : 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)
[DELETE_ELEMENT] Definition
⊢ (∀e. DELETE_ELEMENT e [] = []) ∧
∀e x l.
DELETE_ELEMENT e (x::l) =
if e = x then DELETE_ELEMENT e l else x::DELETE_ELEMENT e l
[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)
[MAX_LIST_def] Definition
⊢ MAX_LIST [] = 0 ∧ ∀h t. MAX_LIST (h::t) = MAX h (MAX_LIST t)
[MIN_LIST_def] Definition
⊢ ∀h t. MIN_LIST (h::t) = if t = [] then h else MIN h (MIN_LIST t)
[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)
[chunks_tr_def] Definition
⊢ ∀n ls.
chunks_tr n ls =
if n = 0 then [ls] else chunks_tr_aux (n − 1) ls []
[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_APPEND_3] Theorem
⊢ ∀l1 x l2.
ALL_DISTINCT (l1 ⧺ [x] ⧺ l2) ⇔ ALL_DISTINCT (x::(l1 ⧺ l2))
[ALL_DISTINCT_EL_APPEND] Theorem
⊢ ∀ls l1 l2 j.
ALL_DISTINCT ls ∧ j < LENGTH ls ∧ ls = l1 ⧺ [EL j ls] ⧺ l2 ⇒
j = LENGTH l1
[ALL_DISTINCT_FRONT] Theorem
⊢ ∀l. l ≠ [] ∧ ALL_DISTINCT l ⇒ ALL_DISTINCT (FRONT l)
[ALL_DISTINCT_LAST_EL_IFF] Theorem
⊢ ∀ls j.
ALL_DISTINCT ls ∧ ls ≠ [] ∧ j < LENGTH ls ⇒
(EL j ls = LAST ls ⇔ j + 1 = LENGTH 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_DISTINCT_SNOC] Theorem
⊢ ∀x l. ALL_DISTINCT (SNOC x l) ⇔ ¬MEM x l ∧ ALL_DISTINCT l
[ALL_DISTINCT_SWAP] Theorem
⊢ ∀ls x y. ALL_DISTINCT (x::y::ls) ⇔ ALL_DISTINCT (y::x::ls)
[ALL_DISTINCT_TAKE] Theorem
⊢ ∀ls n. ALL_DISTINCT ls ⇒ ALL_DISTINCT (TAKE n ls)
[ALL_DISTINCT_TAKE_DROP] Theorem
⊢ ∀ls.
ALL_DISTINCT ls ⇒ ∀k e. MEM e (TAKE k ls) ∧ MEM e (DROP k ls) ⇒ F
[ALL_EL] Theorem
⊢ (∀P. EVERY P [] ⇔ T) ∧ ∀P h t. EVERY P (h::t) ⇔ P h ∧ EVERY P t
[ALL_EL_APPEND] Theorem
⊢ ∀P l1 l2. EVERY P (l1 ⧺ l2) ⇔ EVERY P l1 ∧ EVERY P l2
[ALL_EL_BUTFIRSTN] Theorem
⊢ ∀P l m. EVERY P l ⇒ EVERY P (DROP m l)
[ALL_EL_BUTLASTN] Theorem
⊢ ∀P l m. EVERY P l ⇒ EVERY P (BUTLASTN m l)
[ALL_EL_CONJ] Theorem
⊢ ∀P Q l. EVERY (λx. P x ∧ Q x) l ⇔ EVERY P l ∧ EVERY Q l
[ALL_EL_FIRSTN] Theorem
⊢ ∀P l m. EVERY P l ⇒ EVERY P (TAKE m l)
[ALL_EL_FOLDL] Theorem
⊢ ∀P l. EVERY P l ⇔ FOLDL (λl' x. l' ∧ P x) T l
[ALL_EL_FOLDL_MAP] Theorem
⊢ ∀P l. EVERY P l ⇔ FOLDL $/\ T (MAP P l)
[ALL_EL_FOLDR] Theorem
⊢ ∀P l. EVERY P l ⇔ FOLDR (λx l'. P x ∧ l') T l
[ALL_EL_FOLDR_MAP] Theorem
⊢ ∀P l. EVERY P l ⇔ FOLDR $/\ T (MAP P l)
[ALL_EL_LASTN] Theorem
⊢ ∀P l m. EVERY P l ⇒ EVERY P (LASTN m l)
[ALL_EL_MAP] Theorem
⊢ ∀P f l. EVERY P (MAP f l) ⇔ EVERY (P ∘ f) l
[ALL_EL_REPLICATE] Theorem
⊢ ∀f n x. EVERY f (REPLICATE n x) ⇔ n = 0 ∨ f x
[ALL_EL_REVERSE] Theorem
⊢ ∀P l. EVERY P (REVERSE l) ⇔ EVERY P l
[ALL_EL_SEG] Theorem
⊢ ∀P l. EVERY P l ⇒ ∀m k. m + k ≤ LENGTH l ⇒ EVERY P (SEG m k l)
[ALL_EL_SNOC] Theorem
⊢ ∀P x l. EVERY P (SNOC x l) ⇔ EVERY P l ∧ P x
[AND_EL_FOLDL] Theorem
⊢ ∀l. AND_EL l ⇔ FOLDL $/\ T l
[AND_EL_FOLDR] Theorem
⊢ ∀l. AND_EL l ⇔ FOLDR $/\ T l
[APPEND] Theorem
⊢ (∀l. [] ⧺ l = l) ∧ ∀l1 l2 h. h::l1 ⧺ l2 = h::(l1 ⧺ l2)
[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_ASSOC_CONS] Theorem
⊢ ∀l1 h l2 l3. l1 ⧺ h::l2 ⧺ l3 = l1 ⧺ h::(l2 ⧺ l3)
[APPEND_BUTLASTN_BUTFIRSTN] Theorem
⊢ ∀m n l. m + n = LENGTH l ⇒ BUTLASTN m l ⧺ DROP n l = l
[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_BUTLAST_LAST] Theorem
⊢ ∀l. l ≠ [] ⇒ FRONT l ⧺ [LAST l] = l
[APPEND_EQ_APPEND_EQ] Theorem
⊢ ∀l1 l2 m1 m2.
l1 ⧺ l2 = m1 ⧺ m2 ∧ LENGTH l1 = LENGTH m1 ⇔ l1 = m1 ∧ l2 = m2
[APPEND_FIRSTN_BUTFIRSTN] Theorem
⊢ ∀n l. TAKE n l ⧺ DROP n l = l
[APPEND_FIRSTN_LASTN] Theorem
⊢ ∀m n l. m + n = LENGTH l ⇒ TAKE n l ⧺ LASTN m 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_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) ∧ ∀l. [] ⧺ l = l
[APPEND_SNOC] Theorem
⊢ ∀l1 x l2. l1 ⧺ SNOC x l2 = SNOC x (l1 ⧺ l2)
[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)
[BUTFIRSTN] Theorem
⊢ (∀l. DROP 0 l = l) ∧ ∀n x l. DROP (SUC n) (x::l) = DROP n l
[BUTFIRSTN_APPEND1] Theorem
⊢ ∀n l1. n ≤ LENGTH l1 ⇒ ∀l2. DROP n (l1 ⧺ l2) = DROP n l1 ⧺ l2
[BUTFIRSTN_APPEND2] Theorem
⊢ ∀l1 n.
LENGTH l1 ≤ n ⇒ ∀l2. DROP n (l1 ⧺ l2) = DROP (n − LENGTH l1) l2
[BUTFIRSTN_BUTFIRSTN] Theorem
⊢ ∀n m l. n + m ≤ LENGTH l ⇒ DROP n (DROP m l) = DROP (n + m) l
[BUTFIRSTN_CONS_EL] Theorem
⊢ ∀n l. n < LENGTH l ⇒ DROP n l = EL n l::DROP (SUC n) l
[BUTFIRSTN_LASTN] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n l = LASTN (LENGTH l − n) l
[BUTFIRSTN_LENGTH_APPEND] Theorem
⊢ ∀l1 l2. DROP (LENGTH l1) (l1 ⧺ l2) = l2
[BUTFIRSTN_LENGTH_NIL] Theorem
⊢ ∀l. DROP (LENGTH l) l = []
[BUTFIRSTN_REVERSE] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n (REVERSE l) = REVERSE (BUTLASTN n l)
[BUTFIRSTN_SEG] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n l = SEG (LENGTH l − n) n l
[BUTFIRSTN_SNOC] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. DROP n (SNOC x l) = SNOC x (DROP n l)
[BUTLAST] Theorem
⊢ ∀x l. FRONT (SNOC x l) = 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_BUTLAST] Theorem
⊢ ∀n l. n < LENGTH l ⇒ BUTLASTN n (FRONT l) = FRONT (BUTLASTN n l)
[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_FIRSTN] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n l = TAKE (LENGTH l − 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_BUTLAST] Theorem
⊢ ∀n l. n < LENGTH l ⇒ BUTLASTN (SUC n) l = BUTLASTN n (FRONT 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_TAKE_UNCOND] Theorem
⊢ ∀n 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)
[BUTLAST_CONS] Theorem
⊢ (∀x. FRONT [x] = []) ∧ ∀x y z. FRONT (x::y::z) = x::FRONT (y::z)
[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] 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_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 <..num comp'n..> l =
COUNT_LIST_AUX (<..num comp'n..> − 1) (<..num comp'n..> − 1::l)) ∧
∀n l.
COUNT_LIST_AUX <..num comp'n..> l =
COUNT_LIST_AUX <..num comp'n..> (<..num comp'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 []
[DELETE_ELEMENT_APPEND] Theorem
⊢ ∀a L L'.
DELETE_ELEMENT a (L ⧺ L') =
DELETE_ELEMENT a L ⧺ DELETE_ELEMENT a L'
[DELETE_ELEMENT_FILTER] Theorem
⊢ ∀e L. DELETE_ELEMENT e L = FILTER (λy. e ≠ y) L
[DISTINCT_LIST_TO_SET_EQ_SING] Theorem
⊢ ∀l x. ALL_DISTINCT l ∧ set l = {x} ⇔ l = [x]
[DROP] Theorem
⊢ (∀l. DROP 0 l = l) ∧ ∀n x l. DROP (SUC n) (x::l) = DROP n l
[DROP_1] Theorem
⊢ ∀h t. DROP 1 (h::t) = t
[DROP_1_APPEND] Theorem
⊢ ∀x y. x ≠ [] ⇒ DROP 1 (x ⧺ y) = DROP 1 x ⧺ y
[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_BY_DROP_SUC] Theorem
⊢ ∀k x. k < LENGTH x ⇒ DROP k x = EL k x::DROP (SUC k) x
[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_HEAD_ELEMENT] Theorem
⊢ ∀ls n. n < LENGTH ls ⇒ ∃u. DROP n ls = [EL n ls] ⧺ u
[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_PREn_LAST_CONS] Theorem
⊢ ∀l n.
0 < n ∧ n ≤ LENGTH l ⇒ DROP (n − 1) l = LAST (TAKE n l)::DROP n 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)
[DROP_SUC] Theorem
⊢ ∀n x. DROP (SUC n) x = DROP 1 (DROP n x)
[DROP_TAKE_EQ_NIL] Theorem
⊢ ∀ls n. DROP n (TAKE n ls) = []
[EL] Theorem
⊢ (∀l. EL 0 l = HD l) ∧ ∀l n. EL (SUC n) l = EL n (TL 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_IS_EL] Theorem
⊢ ∀n l. n < LENGTH l ⇒ MEM (ELL n l) 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 <..num comp'n..> l = ELL (<..num comp'n..> − 1) (FRONT l)) ∧
∀n l. ELL <..num comp'n..> l = ELL <..num comp'n..> (FRONT l)
[EL_APPEND] Theorem
⊢ ∀n l1 l2.
EL n (l1 ⧺ l2) =
if n < LENGTH l1 then EL n l1 else EL (n − LENGTH l1) l2
[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_BUTFIRSTN] Theorem
⊢ ∀m n l. m + n < LENGTH l ⇒ EL m (DROP n l) = EL (m + n) l
[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_DROP] Theorem
⊢ ∀m n l. m + n < LENGTH l ⇒ EL m (DROP n l) = EL (m + n) l
[EL_ELL] Theorem
⊢ ∀n l. n < LENGTH l ⇒ EL n l = ELL (PRE (LENGTH l − n)) l
[EL_FIRSTN] Theorem
⊢ ∀n x l. x < n ⇒ EL x (TAKE n l) = EL x l
[EL_FRONT] Theorem
⊢ ∀l n. n < LENGTH (FRONT l) ∧ ¬NULL l ⇒ EL n (FRONT l) = EL n l
[EL_GENLIST] Theorem
⊢ ∀f n x. x < n ⇒ EL x (GENLIST f n) = f x
[EL_IS_EL] Theorem
⊢ ∀n l. n < LENGTH l ⇒ MEM (EL n l) l
[EL_LENGTH_APPEND] Theorem
⊢ ∀l2 l1. ¬NULL l2 ⇒ EL (LENGTH l1) (l1 ⧺ l2) = HD l2
[EL_LENGTH_APPEND_0] Theorem
⊢ ∀ls h t. EL (LENGTH ls) (ls ⧺ h::t) = h
[EL_LENGTH_APPEND_1] Theorem
⊢ ∀ls h k t. EL (LENGTH ls + 1) (ls ⧺ h::k::t) = k
[EL_LENGTH_APPEND_rwt] Theorem
⊢ ¬NULL l2 ∧ n = LENGTH l1 ⇒ EL n (l1 ⧺ l2) = HD l2
[EL_LENGTH_SNOC] Theorem
⊢ ∀l x. EL (LENGTH l) (SNOC x l) = x
[EL_MAP] Theorem
⊢ ∀n l. n < LENGTH l ⇒ ∀f. EL n (MAP f l) = f (EL n l)
[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] Theorem
⊢ ∀n l. n < LENGTH l ⇒ EL n (REVERSE l) = EL (PRE (LENGTH l − n)) l
[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)
[EL_SNOC] Theorem
⊢ ∀n l. n < LENGTH l ⇒ ∀x. EL n (SNOC x l) = EL n l
[EL_SPLIT] Theorem
⊢ ∀ls j. j < LENGTH ls ⇒ ∃l1 l2. ls = l1 ⧺ EL j ls::l2
[EL_SPLIT_2] Theorem
⊢ ∀ls j k.
j < k ∧ k < LENGTH ls ⇒
∃l1 l2 l3. ls = l1 ⧺ EL j ls::l2 ⧺ EL k ls::l3
[EL_TAIL] Theorem
⊢ ∀h t n. 0 ≠ n ⇒ EL (n − 1) t = EL n (h::t)
[EL_TAKE] Theorem
⊢ ∀n x l. x < n ⇒ EL x (TAKE n l) = EL x l
[EL_chunks] Theorem
⊢ ∀k ls n.
n < LENGTH (chunks k ls) ∧ 0 < k ∧ ¬NULL ls ⇒
EL n (chunks k ls) = TAKE k (DROP (n * k) ls)
[EQ_LIST] Theorem
⊢ ∀h1 h2. h1 = h2 ⇒ ∀l1 l2. l1 = l2 ⇒ h1::l1 = h2::l2
[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_DELETE_ELEMENT] Theorem
⊢ ∀e L P. P e ∧ EVERY P (DELETE_ELEMENT e L) ⇒ EVERY P 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_GENLIST] Theorem
⊢ ∀n. EVERY P (GENLIST f n) ⇔ ∀i. i < n ⇒ P (f i)
[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_GENLIST] Theorem
⊢ ∀n. EXISTS P (GENLIST f n) ⇔ ∃i. i < n ∧ P (f i)
[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] Theorem
⊢ (∀P. FILTER P [] = []) ∧
∀P h t. FILTER P (h::t) = if P h then h::FILTER P t else FILTER P t
[FILTER_APPEND] Theorem
⊢ ∀P L M. FILTER P (L ⧺ M) = FILTER P L ⧺ FILTER P M
[FILTER_COMM] Theorem
⊢ ∀f1 f2 l. FILTER f1 (FILTER f2 l) = FILTER f2 (FILTER f1 l)
[FILTER_EL_IFF] Theorem
⊢ ∀P ls l1 l2 x j.
(let
fs = FILTER P ls
in
ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ∧ j < LENGTH fs ⇒
(x = EL j fs ⇔ P x ∧ j = LENGTH (FILTER P l1)))
[FILTER_EL_IMP] Theorem
⊢ ∀P ls l1 l2 x.
(let
fs = FILTER P ls
in
ls = l1 ⧺ x::l2 ∧ P x ⇒ x = EL (LENGTH (FILTER P l1)) fs)
[FILTER_EL_NEXT] Theorem
⊢ ∀P ls l1 l2 l3 x y.
(let
fs = FILTER P ls;
j = LENGTH (FILTER P l1)
in
ls = l1 ⧺ x::l2 ⧺ y::l3 ∧ P x ∧ P y ∧ FILTER P l2 = [] ⇒
x = EL j fs ∧ y = EL (j + 1) fs)
[FILTER_EL_NEXT_IFF] Theorem
⊢ ∀P ls l1 l2 l3 x y.
(let
fs = FILTER P ls;
j = LENGTH (FILTER P l1)
in
ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ⧺ y::l3 ∧ P x ∧ P y ⇒
(x = EL j fs ∧ y = EL (j + 1) fs ⇔ FILTER P l2 = []))
[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_HD] Theorem
⊢ ∀P ls l1 l2 x.
ls = l1 ⧺ x::l2 ∧ P x ∧ FILTER P l1 = [] ⇒ x = HD (FILTER P ls)
[FILTER_HD_IFF] Theorem
⊢ ∀P ls l1 l2 x.
ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ∧ P x ⇒
(x = HD (FILTER P ls) ⇔ FILTER P l1 = [])
[FILTER_IDEM] Theorem
⊢ ∀f l. FILTER f (FILTER f l) = FILTER f l
[FILTER_LAST] Theorem
⊢ ∀P ls l1 l2 x.
ls = l1 ⧺ x::l2 ∧ P x ∧ FILTER P l2 = [] ⇒ x = LAST (FILTER P ls)
[FILTER_LAST_IFF] Theorem
⊢ ∀P ls l1 l2 x.
ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ∧ P x ⇒
(x = LAST (FILTER P ls) ⇔ FILTER P l2 = [])
[FILTER_MAP] Theorem
⊢ ∀f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 ∘ f2) l)
[FILTER_MONO_DEC] Theorem
⊢ ∀P ls. MONO_DEC ls ⇒ MONO_DEC (FILTER P ls)
[FILTER_MONO_INC] Theorem
⊢ ∀P ls. MONO_INC ls ⇒ MONO_INC (FILTER P ls)
[FILTER_REVERSE] Theorem
⊢ ∀l P. FILTER P (REVERSE l) = REVERSE (FILTER P 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
[FILTER_sublist] Theorem
⊢ ∀P ls. FILTER P ls ≤ ls
[FINITE_common_prefixes] Theorem
⊢ s ≠ ∅ ⇒ FINITE (common_prefixes s)
[FINITE_prefix] Theorem
⊢ FINITE {a | a ≼ b}
[FIRSTN] Theorem
⊢ (∀l. TAKE 0 l = []) ∧ ∀n x l. TAKE (SUC n) (x::l) = x::TAKE n l
[FIRSTN_APPEND1] Theorem
⊢ ∀n l1. n ≤ LENGTH l1 ⇒ ∀l2. TAKE n (l1 ⧺ l2) = TAKE n l1
[FIRSTN_APPEND2] Theorem
⊢ ∀l1 n.
LENGTH l1 ≤ n ⇒
∀l2. TAKE n (l1 ⧺ l2) = l1 ⧺ TAKE (n − LENGTH l1) l2
[FIRSTN_BUTLASTN] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n l = BUTLASTN (LENGTH l − n) l
[FIRSTN_FIRSTN] Theorem
⊢ ∀m l. m ≤ LENGTH l ⇒ ∀n. n ≤ m ⇒ TAKE n (TAKE m l) = TAKE n l
[FIRSTN_LENGTH_APPEND] Theorem
⊢ ∀l1 l2. TAKE (LENGTH l1) (l1 ⧺ l2) = l1
[FIRSTN_LENGTH_ID] Theorem
⊢ ∀l. TAKE (LENGTH l) l = l
[FIRSTN_REVERSE] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n (REVERSE l) = REVERSE (LASTN n l)
[FIRSTN_SEG] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n l = SEG n 0 l
[FIRSTN_SNOC] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. TAKE n (SNOC x l) = TAKE n l
[FLAT] Theorem
⊢ FLAT [] = [] ∧ ∀h t. FLAT (h::t) = h ⧺ FLAT t
[FLAT_APPEND] Theorem
⊢ ∀l1 l2. FLAT (l1 ⧺ l2) = FLAT l1 ⧺ FLAT l2
[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
[FLAT_chunks] Theorem
⊢ FLAT (chunks n ls) = ls
[FOLDL] Theorem
⊢ (∀f e. FOLDL f e [] = e) ∧
∀f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l
[FOLDL_APPEND] Theorem
⊢ ∀f e l1 l2. FOLDL f e (l1 ⧺ l2) = FOLDL f (FOLDL f e l1) l2
[FOLDL_CONG_invariant] Theorem
⊢ ∀P f1 f2 l e.
P e ∧ (∀x a. MEM x l ∧ P a ⇒ f1 a x = f2 a x ∧ P (f2 a x)) ⇒
FOLDL f1 e l = FOLDL f2 e l ∧ P (FOLDL f2 e l)
[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] Theorem
⊢ ∀f e x l. FOLDL f e (SNOC x l) = f (FOLDL f e l) x
[FOLDL_SNOC_NIL] Theorem
⊢ ∀l. FOLDL (λxs x. SNOC x xs) [] l = l
[FOLDR] Theorem
⊢ (∀f e. FOLDR f e [] = e) ∧
∀f e x l. FOLDR f e (x::l) = f x (FOLDR f e 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)
[FRONT_APPEND_NOT_NIL] Theorem
⊢ ∀l1 l2. l2 ≠ [] ⇒ FRONT (l1 ⧺ l2) = l1 ⧺ FRONT l2
[FRONT_BY_TAKE] Theorem
⊢ ∀ls. ls ≠ [] ⇒ FRONT ls = TAKE (LENGTH ls − 1) ls
[FRONT_EL] Theorem
⊢ ∀l n. l ≠ [] ∧ n < LENGTH (FRONT l) ⇒ EL n (FRONT l) = EL n l
[FRONT_EQ_NIL] Theorem
⊢ ∀l. LENGTH l = 1 ⇒ FRONT l = []
[FRONT_LENGTH] Theorem
⊢ ∀l. l ≠ [] ⇒ LENGTH (FRONT l) = PRE (LENGTH l)
[FRONT_NON_NIL] Theorem
⊢ ∀l. 1 < LENGTH l ⇒ FRONT l ≠ []
[FRONT_SING] Theorem
⊢ ∀x. FRONT [x] = []
[GENLIST] Theorem
⊢ (∀f. GENLIST f 0 = []) ∧
∀f n. GENLIST f (SUC n) = SNOC (f n) (GENLIST f n)
[GENLIST_APPEND] Theorem
⊢ ∀f a b. GENLIST f (a + b) = GENLIST f b ⧺ GENLIST (λt. f (t + b)) a
[GENLIST_CONS] Theorem
⊢ GENLIST f (SUC n) = f 0::GENLIST (f ∘ SUC) n
[GENLIST_FUN_EQ] Theorem
⊢ ∀n f g. GENLIST f n = GENLIST g n ⇔ ∀x. x < n ⇒ f x = g x
[GENLIST_K_ADD] Theorem
⊢ ∀e n m. GENLIST (K e) (n + m) = GENLIST (K e) m ⧺ GENLIST (K e) n
[GENLIST_K_APPEND] Theorem
⊢ ∀a b c. GENLIST (K c) a ⧺ GENLIST (K c) b = GENLIST (K c) (a + b)
[GENLIST_K_APPEND_K] Theorem
⊢ ∀c n. GENLIST (K c) n ⧺ [c] = [c] ⧺ GENLIST (K c) n
[GENLIST_K_CONS] Theorem
⊢ ∀e n. GENLIST (K e) (SUC n) = e::GENLIST (K e) n
[GENLIST_K_LESS] Theorem
⊢ ∀f e n. (∀k. k < n ⇒ f k = e) ⇒ GENLIST f n = GENLIST (K e) n
[GENLIST_K_MEM] Theorem
⊢ ∀x c n. 0 < n ⇒ (MEM x (GENLIST (K c) n) ⇔ x = c)
[GENLIST_K_RANGE] Theorem
⊢ ∀f e n.
(∀k. 0 < k ∧ k ≤ n ⇒ f k = e) ⇒
GENLIST (f ∘ SUC) n = GENLIST (K e) n
[GENLIST_K_SET] Theorem
⊢ ∀c n. 0 < n ⇒ set (GENLIST (K c) n) = {c}
[HD] Theorem
⊢ ∀h t. HD (h::t) = h
[HD_APPEND] Theorem
⊢ ∀h t ls. HD (h::t ⧺ ls) = h
[HD_APPEND_NOT_NIL] Theorem
⊢ ∀l1 l2. l1 ≠ [] ⇒ HD (l1 ⧺ l2) = HD l1
[HD_GENLIST] Theorem
⊢ HD (GENLIST f (SUC n)) = f 0
[HEAD_MEM] Theorem
⊢ ∀ls. ls ≠ [] ⇒ MEM (HD ls) ls
[IS_EL] Theorem
⊢ (∀x. MEM x [] ⇔ F) ∧ ∀x h t. MEM x (h::t) ⇔ x = h ∨ MEM x t
[IS_EL_APPEND] Theorem
⊢ ∀e l1 l2. MEM e (l1 ⧺ l2) ⇔ MEM e l1 ∨ MEM e l2
[IS_EL_BUTFIRSTN] Theorem
⊢ ∀l m x. MEM x (DROP m l) ⇒ MEM x l
[IS_EL_BUTLASTN] Theorem
⊢ ∀l m x. MEM x (BUTLASTN m l) ⇒ MEM x l
[IS_EL_DEF] Theorem
⊢ ∀x l. MEM x l ⇔ EXISTS ($= x) l
[IS_EL_FILTER] Theorem
⊢ ∀P L x. MEM x (FILTER P L) ⇔ P x ∧ MEM x L
[IS_EL_FIRSTN] Theorem
⊢ ∀l m x. MEM x (TAKE m l) ⇒ MEM x l
[IS_EL_FOLDL] Theorem
⊢ ∀y l. MEM y l ⇔ FOLDL (λl' x. l' ∨ y = x) F l
[IS_EL_FOLDL_MAP] Theorem
⊢ ∀x l. MEM x l ⇔ FOLDL $\/ F (MAP ($= x) l)
[IS_EL_FOLDR] Theorem
⊢ ∀y l. MEM y l ⇔ FOLDR (λx l'. y = x ∨ l') F l
[IS_EL_FOLDR_MAP] Theorem
⊢ ∀x l. MEM x l ⇔ FOLDR $\/ F (MAP ($= x) l)
[IS_EL_LASTN] Theorem
⊢ ∀m l x. MEM x (LASTN m l) ⇒ MEM x l
[IS_EL_REPLICATE] Theorem
⊢ ∀n x y. MEM y (REPLICATE n x) ⇔ x = y ∧ 0 < n
[IS_EL_REVERSE] Theorem
⊢ ∀l x. MEM x (REVERSE l) ⇔ MEM x l
[IS_EL_SEG] Theorem
⊢ ∀n m l. n + m ≤ LENGTH l ⇒ ∀x. MEM x (SEG n m l) ⇒ MEM x l
[IS_EL_SNOC] Theorem
⊢ ∀y x l. MEM y (SNOC x l) ⇔ y = x ∨ MEM y l
[IS_EL_SOME_EL] Theorem
⊢ ∀x l. MEM x l ⇔ EXISTS ($= x) l
[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_ALL_DISTINCT] Theorem
⊢ ∀l l1. l1 ≼ l ∧ ALL_DISTINCT l ⇒ ALL_DISTINCT 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_BUTLAST'] Theorem
⊢ ∀l. l ≠ [] ⇒ FRONT l ≼ l
[IS_PREFIX_EQ_REWRITE] Theorem
⊢ ∀l1 l2 l. l1 ≼ l ∧ l2 ≼ l ⇒ (l1 = l2 ⇔ LENGTH l1 = LENGTH l2)
[IS_PREFIX_EQ_TAKE] Theorem
⊢ ∀l l1. l1 ≼ l ⇔ ∃n. n ≤ LENGTH l ∧ l1 = TAKE n l
[IS_PREFIX_EQ_TAKE'] Theorem
⊢ ∀l l1. l1 ≼ l ⇔ ∃n. l1 = TAKE n l
[IS_PREFIX_FRONT_CASES] Theorem
⊢ ∀l l1. l ≠ [] ⇒ (l1 ≼ l ⇔ l = l1 ∨ l1 ≼ FRONT l)
[IS_PREFIX_FRONT_MONO] Theorem
⊢ ∀l1 l2. l1 ≠ [] ∧ l2 ≠ [] ∧ l1 ≼ l2 ⇒ FRONT l1 ≼ FRONT l2
[IS_PREFIX_GENLIST] Theorem
⊢ ∀f m n. GENLIST f m ≼ GENLIST f n ⇔ m ≤ n
[IS_PREFIX_IMP_TAKE] Theorem
⊢ ∀l l1. l1 ≼ l ⇒ l1 = TAKE (LENGTH l1) l
[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
⊢ l ≼ SNOC x l
[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_ALL_DISTINCT] Theorem
⊢ ∀l l1. IS_SUFFIX l l1 ∧ ALL_DISTINCT l ⇒ ALL_DISTINCT l1
[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_EQ_DROP] Theorem
⊢ ∀l l1. IS_SUFFIX l l1 ⇔ ∃n. n ≤ LENGTH l ∧ l1 = DROP n l
[IS_SUFFIX_EQ_DROP'] Theorem
⊢ ∀l l1. IS_SUFFIX l l1 ⇔ ∃n. l1 = DROP n l
[IS_SUFFIX_IMP_DROP] Theorem
⊢ ∀l l1. IS_SUFFIX l l1 ⇒ l1 = DROP (LENGTH l − LENGTH l1) l
[IS_SUFFIX_IMP_LASTN] Theorem
⊢ ∀l l1. IS_SUFFIX l l1 ⇒ l1 = LASTN (LENGTH l1) l
[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
[IS_SUFFIX_dropWhile] Theorem
⊢ IS_SUFFIX ls (dropWhile P ls)
[ITSET_TO_FOLDR] Theorem
⊢ ∀f s b.
FINITE s ⇒ ITSET f s b = FOLDR f b (REVERSE (SET_TO_LIST s))
[LAST] Theorem
⊢ ∀x l. LAST (SNOC x l) = x
[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_BUTFIRSTN] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ LASTN n l = DROP (LENGTH l − n) l
[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_DROP_UNCOND] Theorem
⊢ ∀n 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_APPEND] Theorem
⊢ ∀h l1 l2. LAST (l1 ⧺ h::l2) = LAST (h::l2)
[LAST_APPEND_NOT_NIL] Theorem
⊢ ∀l1 l2. l2 ≠ [] ⇒ LAST (l1 ⧺ l2) = LAST l2
[LAST_CONS] Theorem
⊢ (∀x. LAST [x] = x) ∧ ∀x y z. LAST (x::y::z) = LAST (y::z)
[LAST_EL_CONS] Theorem
⊢ ∀h t. t ≠ [] ⇒ LAST t = EL (LENGTH t) (h::t)
[LAST_EQ_HD] Theorem
⊢ ∀h t. ¬MEM h t ∧ LAST (h::t) = h ⇔ t = []
[LAST_LASTN_LAST] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ 0 < n ⇒ LAST (LASTN n l) = LAST l
[LAST_MEM] Theorem
⊢ ∀ls. ls ≠ [] ⇒ MEM (LAST ls) ls
[LENGTH] Theorem
⊢ LENGTH [] = 0 ∧ ∀h t. LENGTH (h::t) = SUC (LENGTH t)
[LENGTH_APPEND] Theorem
⊢ ∀l1 l2. LENGTH (l1 ⧺ l2) = LENGTH l1 + LENGTH l2
[LENGTH_BUTFIRSTN] Theorem
⊢ ∀n l. LENGTH (DROP n l) = LENGTH l − n
[LENGTH_BUTLAST] Theorem
⊢ ∀l. l ≠ [] ⇒ LENGTH (FRONT l) = PRE (LENGTH l)
[LENGTH_BUTLASTN] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (BUTLASTN n l) = LENGTH l − n
[LENGTH_CONS] Theorem
⊢ ∀l n. LENGTH l = SUC n ⇔ ∃h l'. LENGTH l' = n ∧ l = h::l'
[LENGTH_COUNT_LIST] Theorem
⊢ ∀n. LENGTH (COUNT_LIST n) = n
[LENGTH_DELETE_ELEMENT_LE] Theorem
⊢ ∀e L. MEM e L ⇒ LENGTH (DELETE_ELEMENT e L) < LENGTH L
[LENGTH_DELETE_ELEMENT_LEQ] Theorem
⊢ ∀e L. LENGTH (DELETE_ELEMENT e L) ≤ LENGTH L
[LENGTH_EQ_NIL] Theorem
⊢ ∀P. (∀l. LENGTH l = 0 ⇒ P l) ⇔ P []
[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_FIRSTN] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (TAKE n l) = n
[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_GENLIST] Theorem
⊢ ∀f n. LENGTH (GENLIST f n) = n
[LENGTH_LASTN] Theorem
⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (LASTN n l) = n
[LENGTH_MAP] Theorem
⊢ ∀l f. LENGTH (MAP f l) = LENGTH l
[LENGTH_NIL] Theorem
⊢ ∀l. LENGTH l = 0 ⇔ l = []
[LENGTH_NOT_NULL] Theorem
⊢ ∀l. 0 < LENGTH l ⇔ ¬NULL l
[LENGTH_REPLICATE] Theorem
⊢ ∀n x. LENGTH (REPLICATE n x) = n
[LENGTH_REVERSE] Theorem
⊢ ∀l. LENGTH (REVERSE l) = LENGTH l
[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_SING] Theorem
⊢ ∀x. LENGTH [x] = 1
[LENGTH_SNOC] Theorem
⊢ ∀x l. LENGTH (SNOC x l) = SUC (LENGTH l)
[LENGTH_TAKE_LE] Theorem
⊢ ∀n l. LENGTH (TAKE n l) ≤ LENGTH l
[LENGTH_TL_LT] Theorem
⊢ ∀ls. ls ≠ [] ⇒ LENGTH (TL ls) < LENGTH ls
[LENGTH_UNZIP_FST] Theorem
⊢ ∀l. LENGTH (UNZIP_FST l) = LENGTH l
[LENGTH_UNZIP_SND] Theorem
⊢ ∀l. LENGTH (UNZIP_SND l) = LENGTH l
[LENGTH_ZIP] Theorem
⊢ ∀l1 l2.
LENGTH l1 = LENGTH l2 ⇒
LENGTH (ZIP (l1,l2)) = LENGTH l1 ∧
LENGTH (ZIP (l1,l2)) = LENGTH l2
[LENGTH_chunks] Theorem
⊢ ∀n ls.
0 < n ∧ ¬NULL ls ⇒
LENGTH (chunks n ls) =
LENGTH ls DIV n + bool_to_bit (¬divides n (LENGTH ls))
[LENGTH_dropWhile_id] Theorem
⊢ LENGTH (dropWhile P ls) = LENGTH ls ⇔ dropWhile P ls = ls
[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_EQ_HEAD_TAIL] Theorem
⊢ ∀p q. p ≠ [] ∧ q ≠ [] ⇒ (p = q ⇔ HD p = HD q ∧ TL p = TL q)
[LIST_HEAD_TAIL] Theorem
⊢ ∀ls. 0 < LENGTH ls ⇔ ls = HD ls::TL ls
[LIST_NOT_EQ] Theorem
⊢ ∀l1 l2. l1 ≠ l2 ⇒ ∀h1 h2. h1::l1 ≠ h2::l2
[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) ⇔ 0 < n ⇒ P x y
[LIST_REL_REVERSE_EQ] Theorem
⊢ LIST_REL R (REVERSE l1) (REVERSE l2) ⇔ LIST_REL R l1 l2
[LIST_SING_EQ] Theorem
⊢ ∀x y. [x] = [y] ⇔ x = y
[LIST_TO_SET_EQ_SING] Theorem
⊢ ∀x ls. set ls = {x} ⇔ ls ≠ [] ∧ EVERY ($= x) ls
[LIST_TO_SET_PREFIX] Theorem
⊢ ∀l l1. l1 ≼ l ⇒ set l1 ⊆ set l
[LIST_TO_SET_SING_IFF] Theorem
⊢ ∀ls. ls ≠ [] ⇒ (SING (set ls) ⇔ ∃c. ls = GENLIST (K c) (LENGTH ls))
[LIST_TO_SET_SUFFIX] Theorem
⊢ ∀l l1. IS_SUFFIX l l1 ⇒ set l1 ⊆ set l
[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] Theorem
⊢ (∀f. MAP f [] = []) ∧ ∀f h t. MAP f (h::t) = f h::MAP f t
[MAP2] Theorem
⊢ (∀f. MAP2 f [] [] = []) ∧
∀f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2
[MAP2_MAP_MAP] Theorem
⊢ ∀ls f g1 g2.
MAP2 f (MAP g1 ls) (MAP g2 ls) = MAP (λx. f (g1 x) (g2 x)) ls
[MAP2_ZIP] Theorem
⊢ ∀l1 l2.
LENGTH l1 = LENGTH l2 ⇒
∀f. MAP2 f l1 l2 = MAP (UNCURRY f) (ZIP (l1,l2))
[MAP_APPEND] Theorem
⊢ ∀f l1 l2. MAP f (l1 ⧺ l2) = MAP f l1 ⧺ MAP f l2
[MAP_COUNT_LIST] Theorem
⊢ MAP f (COUNT_LIST n) = GENLIST f n
[MAP_EQ_f] Theorem
⊢ ∀f1 f2 l. MAP f1 l = MAP f2 l ⇔ ∀e. MEM e l ⇒ f1 e = f2 e
[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_GENLIST] Theorem
⊢ ∀f g n. MAP f (GENLIST g n) = GENLIST (f ∘ g) n
[MAP_HD] Theorem
⊢ ∀ls f. ls ≠ [] ⇒ HD (MAP f ls) = f (HD ls)
[MAP_MAP_o] Theorem
⊢ ∀f g l. MAP f (MAP g l) = MAP (f ∘ g) l
[MAP_REVERSE] Theorem
⊢ ∀f l. MAP f (REVERSE l) = REVERSE (MAP f l)
[MAP_SING] Theorem
⊢ ∀f x. MAP f [x] = [f x]
[MAP_SND_FILTER_NEQ] Theorem
⊢ MAP SND (FILTER (λ(x,y). y ≠ z) ls) =
FILTER (λy. z ≠ y) (MAP SND ls)
[MAP_SNOC] Theorem
⊢ ∀f x l. MAP f (SNOC x l) = SNOC (f x) (MAP f l)
[MAP_SUBLIST] Theorem
⊢ ∀f p q. p ≤ q ⇒ MAP f p ≤ MAP f q
[MAP_o] Theorem
⊢ ∀f g. MAP (f ∘ g) = MAP f ∘ MAP g
[MAX_LIST_CONS] Theorem
⊢ ∀h t. MAX_LIST (h::t) = MAX h (MAX_LIST t)
[MAX_LIST_EQ_0] Theorem
⊢ ∀l. MAX_LIST l = 0 ⇔ EVERY (λx. x = 0) l
[MAX_LIST_LE] Theorem
⊢ ∀h t. MAX_LIST t ≤ MAX_LIST (h::t)
[MAX_LIST_MAP_LE] Theorem
⊢ ∀f g.
(∀x. f x ≤ g x) ⇒ ∀ls. MAX_LIST (MAP f ls) ≤ MAX_LIST (MAP g ls)
[MAX_LIST_MEM] Theorem
⊢ ∀l. l ≠ [] ⇒ MEM (MAX_LIST l) l
[MAX_LIST_MONO_DEC] Theorem
⊢ ∀ls. ls ≠ [] ∧ MONO_DEC ls ⇒ MAX_LIST ls = HD ls
[MAX_LIST_MONO_INC] Theorem
⊢ ∀ls. ls ≠ [] ∧ MONO_INC ls ⇒ MAX_LIST ls = LAST ls
[MAX_LIST_NIL] Theorem
⊢ MAX_LIST [] = 0
[MAX_LIST_PROPERTY] Theorem
⊢ ∀l x. MEM x l ⇒ x ≤ MAX_LIST l
[MAX_LIST_SING] Theorem
⊢ ∀x. MAX_LIST [x] = x
[MAX_LIST_TEST] Theorem
⊢ ∀l. l ≠ [] ⇒ ∀x. MEM x l ∧ (∀y. MEM y l ⇒ y ≤ x) ⇒ x = MAX_LIST l
[MEM_APPEND_3] Theorem
⊢ ∀l1 x l2 h. MEM h (l1 ⧺ [x] ⧺ l2) ⇔ MEM h (x::(l1 ⧺ l2))
[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_FRONT_NOT_LAST] Theorem
⊢ ∀ls. ls ≠ [] ∧ ALL_DISTINCT ls ⇒ ¬MEM (LAST ls) (FRONT ls)
[MEM_FRONT_NOT_NIL] Theorem
⊢ ∀l y. l ≠ [] ∧ MEM y (FRONT l) ⇒ MEM y 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_LAST_NOT_NIL] Theorem
⊢ ∀e l. l ≠ [] ⇒ MEM (LAST l) 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_SPLIT_APPEND_distinct] Theorem
⊢ ∀l. ALL_DISTINCT l ⇒
∀x. MEM x l ⇔ ∃p1 p2. l = p1 ⧺ [x] ⧺ p2 ∧ ¬MEM x p1 ∧ ¬MEM x p2
[MEM_SPLIT_TAKE_DROP_distinct] Theorem
⊢ ∀ls.
ALL_DISTINCT ls ⇒
∀x. MEM x ls ⇔
∃k. k < LENGTH ls ∧ x = EL k ls ∧
ls = TAKE k ls ⧺ x::DROP (k + 1) ls ∧
¬MEM x (TAKE k ls) ∧ ¬MEM x (DROP (k + 1) ls)
[MEM_SPLIT_TAKE_DROP_first] Theorem
⊢ ∀ls x.
MEM x ls ⇔
∃k. k < LENGTH ls ∧ x = EL k ls ∧
ls = TAKE k ls ⧺ x::DROP (k + 1) ls ∧ ¬MEM x (TAKE k ls)
[MEM_SPLIT_TAKE_DROP_last] Theorem
⊢ ∀ls x.
MEM x ls ⇔
∃k. k < LENGTH ls ∧ x = EL k ls ∧
ls = TAKE k ls ⧺ x::DROP (k + 1) ls ∧
¬MEM x (DROP (k + 1) ls)
[MEM_TAKE] Theorem
⊢ ∀l m x. MEM x (TAKE m l) ⇒ MEM x l
[MIN_LIST_CONS] Theorem
⊢ ∀h t. t ≠ [] ⇒ MIN_LIST (h::t) = MIN h (MIN_LIST t)
[MIN_LIST_LE] Theorem
⊢ ∀h t. t ≠ [] ⇒ MIN_LIST (h::t) ≤ MIN_LIST t
[MIN_LIST_LE_MAX_LIST] Theorem
⊢ ∀l. l ≠ [] ⇒ MIN_LIST l ≤ MAX_LIST l
[MIN_LIST_MAP_LE] Theorem
⊢ ∀f g.
(∀x. f x ≤ g x) ⇒ ∀ls. MIN_LIST (MAP f ls) ≤ MIN_LIST (MAP g ls)
[MIN_LIST_MEM] Theorem
⊢ ∀l. l ≠ [] ⇒ MEM (MIN_LIST l) l
[MIN_LIST_MONO_DEC] Theorem
⊢ ∀ls. ls ≠ [] ∧ MONO_DEC ls ⇒ MIN_LIST ls = LAST ls
[MIN_LIST_MONO_INC] Theorem
⊢ ∀ls. ls ≠ [] ∧ MONO_INC ls ⇒ MIN_LIST ls = HD ls
[MIN_LIST_PROPERTY] Theorem
⊢ ∀l. l ≠ [] ⇒ ∀x. MEM x l ⇒ MIN_LIST l ≤ x
[MIN_LIST_SING] Theorem
⊢ ∀x. MIN_LIST [x] = x
[MIN_LIST_TEST] Theorem
⊢ ∀l. l ≠ [] ⇒ ∀x. MEM x l ∧ (∀y. MEM y l ⇒ x ≤ y) ⇒ x = MIN_LIST l
[MONOID_APPEND_NIL] Theorem
⊢ MONOID $++ []
[MONOLIST_EQ] Theorem
⊢ ∀l1 l2.
SING (set l1) ∧ SING (set l2) ⇒
(l1 = l2 ⇔ LENGTH l1 = LENGTH l2 ∧ set l1 = set l2)
[MONOLIST_SET_SING] Theorem
⊢ ∀c ls. ls ≠ [] ∧ EVERY ($= c) ls ⇒ SING (set ls)
[MONO_DEC_CONS] Theorem
⊢ ∀h t. MONO_DEC (h::t) ⇒ MONO_DEC t
[MONO_DEC_HD] Theorem
⊢ ∀h t x. MONO_DEC (h::t) ∧ MEM x t ⇒ x ≤ h
[MONO_DEC_NIL] Theorem
⊢ MONO_DEC []
[MONO_INC_CONS] Theorem
⊢ ∀h t. MONO_INC (h::t) ⇒ MONO_INC t
[MONO_INC_HD] Theorem
⊢ ∀h t x. MONO_INC (h::t) ∧ MEM x t ⇒ h ≤ x
[MONO_INC_NIL] Theorem
⊢ MONO_INC []
[NIL_IN_common_prefixes] Theorem
⊢ [] ∈ common_prefixes s
[NIL_NO_MEM] Theorem
⊢ ∀ls. ls = [] ⇔ ∀x. ¬MEM x ls
[NON_MONO_TAIL_PROPERTY] Theorem
⊢ ∀l. ¬SING (set (h::t)) ⇒ ∃h'. MEM h' t ∧ h' ≠ h
[NOT_ALL_EL_SOME_EL] Theorem
⊢ ∀P l. ¬EVERY P l ⇔ EXISTS ($¬ ∘ P) l
[NOT_CONS_NIL] Theorem
⊢ ∀a1 a0. a0::a1 ≠ []
[NOT_EQ_LIST] Theorem
⊢ ∀h1 h2. h1 ≠ h2 ⇒ ∀l1 l2. h1::l1 ≠ h2::l2
[NOT_IN_DELETE_ELEMENT] Theorem
⊢ ∀e L. ¬MEM e (DELETE_ELEMENT e L)
[NOT_NIL_CONS] Theorem
⊢ ∀a1 a0. [] ≠ a0::a1
[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 ≠ []
[NOT_SOME_EL_ALL_EL] Theorem
⊢ ∀P l. ¬EXISTS P l ⇔ EVERY ($¬ ∘ P) l
[NULL] Theorem
⊢ NULL [] ∧ ∀h t. ¬NULL (h::t)
[NULL_DEF] Theorem
⊢ (NULL [] ⇔ T) ∧ ∀h t. NULL (h::t) ⇔ F
[NULL_EQ_NIL] Theorem
⊢ ∀l. NULL l ⇔ 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_EQ_CONS] Theorem
⊢ REPLICATE n x = y::r ⇔ y = x ∧ ∃m. n = SUC m ∧ r = REPLICATE m x
[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 <..num comp'n..> x =
x::REPLICATE (<..num comp'n..> − 1) x) ∧
∀n x.
REPLICATE <..num comp'n..> x = x::REPLICATE <..num comp'n..> x
[REVERSE_APPEND] Theorem
⊢ ∀l1 l2. REVERSE (l1 ⧺ l2) = REVERSE l2 ⧺ REVERSE l1
[REVERSE_DROP] Theorem
⊢ ∀ls n.
n ≤ LENGTH ls ⇒
REVERSE (DROP n ls) = REVERSE (LASTN (LENGTH ls − n) ls)
[REVERSE_EQ_NIL] Theorem
⊢ REVERSE l = [] ⇔ l = []
[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_HD] Theorem
⊢ ∀ls. ls ≠ [] ⇒ HD (REVERSE ls) = LAST ls
[REVERSE_REPLICATE] Theorem
⊢ ∀n x. REVERSE (REPLICATE n x) = REPLICATE n x
[REVERSE_REVERSE] Theorem
⊢ ∀l. REVERSE (REVERSE l) = l
[REVERSE_SING] Theorem
⊢ ∀x. REVERSE [x] = [x]
[REVERSE_SNOC] Theorem
⊢ ∀x l. REVERSE (SNOC x l) = x::REVERSE l
[REVERSE_TL] Theorem
⊢ ∀ls. ls ≠ [] ⇒ TL (REVERSE ls) = REVERSE (FRONT ls)
[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 <..num comp'n..> 0 (x::l) =
x::SEG (<..num comp'n..> − 1) 0 l) ∧
(∀m x l.
SEG <..num comp'n..> 0 (x::l) = x::SEG <..num comp'n..> 0 l) ∧
(∀m k x l.
SEG <..num comp'n..> <..num comp'n..> (x::l) =
SEG <..num comp'n..> (<..num comp'n..> − 1) l) ∧
(∀m k x l.
SEG <..num comp'n..> <..num comp'n..> (x::l) =
SEG <..num comp'n..> (<..num comp'n..> − 1) l) ∧
(∀m k x l.
SEG <..num comp'n..> <..num comp'n..> (x::l) =
SEG <..num comp'n..> <..num comp'n..> l) ∧
∀m k x l.
SEG <..num comp'n..> <..num comp'n..> (x::l) =
SEG <..num comp'n..> <..num comp'n..> l
[SING_LIST_TO_SET] Theorem
⊢ ∀l. LENGTH l = 1 ⇒ SING (set l)
[SNOC] Theorem
⊢ (∀x. SNOC x [] = [x]) ∧ ∀x x' l. SNOC x (x'::l) = x'::SNOC x l
[SNOC_11] Theorem
⊢ ∀x y a b. SNOC x y = SNOC a b ⇔ x = a ∧ y = b
[SNOC_ACYCLIC] Theorem
⊢ l ≠ SNOC x l ∧ SNOC x l ≠ l
[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_EL_FIRSTN] Theorem
⊢ ∀n l. n < LENGTH l ⇒ SNOC (EL n l) (TAKE n l) = TAKE (SUC n) 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_INDUCT] Theorem
⊢ ∀P. P [] ∧ (∀l. P l ⇒ ∀x. P (SNOC x l)) ⇒ ∀l. P l
[SNOC_LASTN] Theorem
⊢ ∀l x n. LASTN (SUC n) (SNOC x l) = SNOC x (LASTN n l)
[SNOC_LAST_FRONT'] Theorem
⊢ ∀l. l ≠ [] ⇒ l = SNOC (LAST l) (FRONT 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)
[SOME_EL] Theorem
⊢ (∀P. EXISTS P [] ⇔ F) ∧ ∀P h t. EXISTS P (h::t) ⇔ P h ∨ EXISTS P t
[SOME_EL_APPEND] Theorem
⊢ ∀P l1 l2. EXISTS P (l1 ⧺ l2) ⇔ EXISTS P l1 ∨ EXISTS P l2
[SOME_EL_BUTFIRSTN] Theorem
⊢ ∀l m P. EXISTS P (DROP m l) ⇒ EXISTS P l
[SOME_EL_BUTLASTN] Theorem
⊢ ∀l m P. EXISTS P (BUTLASTN m l) ⇒ EXISTS P l
[SOME_EL_DISJ] Theorem
⊢ ∀P Q l. (EXISTS (λx. P x ∨ Q x) l ⇔ EXISTS P l) ∨ EXISTS Q l
[SOME_EL_FIRSTN] Theorem
⊢ ∀l m P. EXISTS P (TAKE m l) ⇒ EXISTS P l
[SOME_EL_FOLDL] Theorem
⊢ ∀P l. EXISTS P l ⇔ FOLDL (λl' x. l' ∨ P x) F l
[SOME_EL_FOLDL_MAP] Theorem
⊢ ∀P l. EXISTS P l ⇔ FOLDL $\/ F (MAP P l)
[SOME_EL_FOLDR] Theorem
⊢ ∀P l. EXISTS P l ⇔ FOLDR (λx l'. P x ∨ l') F l
[SOME_EL_FOLDR_MAP] Theorem
⊢ ∀P l. EXISTS P l ⇔ FOLDR $\/ F (MAP P l)
[SOME_EL_LASTN] Theorem
⊢ ∀l m P. EXISTS P (LASTN m l) ⇒ EXISTS P l
[SOME_EL_MAP] Theorem
⊢ ∀P f l. EXISTS P (MAP f l) ⇔ EXISTS (λx. P (f x)) l
[SOME_EL_REVERSE] Theorem
⊢ ∀P l. EXISTS P (REVERSE l) ⇔ EXISTS P l
[SOME_EL_SEG] Theorem
⊢ ∀m k l. m + k ≤ LENGTH l ⇒ ∀P. EXISTS P (SEG m k l) ⇒ EXISTS P l
[SOME_EL_SNOC] Theorem
⊢ ∀P x l. EXISTS P (SNOC x l) ⇔ P x ∨ EXISTS P 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] Theorem
⊢ SUM [] = 0 ∧ ∀h t. SUM (h::t) = h + SUM t
[SUM_APPEND] Theorem
⊢ ∀l1 l2. SUM (l1 ⧺ l2) = SUM l1 + SUM l2
[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_IMAGE_count_MULT] Theorem
⊢ (∀m. m < n ⇒ g m = ∑ (λx. f (x + k * m)) (count k)) ⇒
∑ f (count (k * n)) = ∑ g (count n)
[SUM_IMAGE_count_SUM_GENLIST] Theorem
⊢ ∑ f (count n) = SUM (GENLIST f n)
[SUM_REPLICATE] Theorem
⊢ ∀n k. SUM (REPLICATE n k) = n * k
[SUM_REVERSE] Theorem
⊢ ∀l. SUM (REVERSE l) = SUM l
[SUM_SNOC] Theorem
⊢ ∀x l. SUM (SNOC x l) = SUM l + x
[SUM_SUBLIST] Theorem
⊢ ∀p q. p ≤ q ⇒ SUM p ≤ SUM q
[TAIL_BY_DROP] Theorem
⊢ ∀ls. ls ≠ [] ⇒ TL ls = DROP 1 ls
[TAKE] Theorem
⊢ (∀l. TAKE 0 l = []) ∧ ∀n x l. TAKE (SUC n) (x::l) = x::TAKE n l
[TAKE_1_APPEND] Theorem
⊢ ∀x y. x ≠ [] ⇒ TAKE 1 (x ⧺ y) = TAKE 1 x
[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_DROP_SUC] Theorem
⊢ ∀n l. n < LENGTH l ⇒ TAKE n l ⧺ [EL n l] ⧺ DROP (SUC n) l = l
[TAKE_DROP_SWAP] Theorem
⊢ ∀ls m n. TAKE m (DROP n ls) = DROP n (TAKE (n + m) ls)
[TAKE_EL_SNOC] Theorem
⊢ ∀ls n. n < LENGTH ls ⇒ TAKE (n + 1) ls = SNOC (EL n ls) (TAKE n ls)
[TAKE_FRONT] Theorem
⊢ ∀l n. l ≠ [] ∧ n < LENGTH l ⇒ TAKE n (FRONT l) = TAKE n l
[TAKE_LENGTH_APPEND] Theorem
⊢ ∀l1 l2. TAKE (LENGTH l1) (l1 ⧺ l2) = l1
[TAKE_LENGTH_APPEND2] Theorem
⊢ ∀l1 l2 x k.
TAKE (LENGTH l1) (LUPDATE x (LENGTH l1 + k) (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_SUC] Theorem
⊢ ∀n x. TAKE (SUC n) x = TAKE n x ⧺ TAKE 1 (DROP n x)
[TAKE_SUC_BY_TAKE] Theorem
⊢ ∀k x. k < LENGTH x ⇒ TAKE (SUC k) x = SNOC (EL k x) (TAKE k x)
[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] Theorem
⊢ ∀h t. TL (h::t) = t
[TL_DROP] Theorem
⊢ ∀ls n. n < LENGTH ls ⇒ TL (DROP n ls) = DROP n (TL ls)
[TL_GENLIST] Theorem
⊢ ∀f n. TL (GENLIST f (SUC n)) = GENLIST (f ∘ SUC) n
[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] Theorem
⊢ UNZIP [] = ([],[]) ∧
∀x l. UNZIP (x::l) = (FST x::FST (UNZIP l),SND x::SND (UNZIP l))
[UNZIP_SNOC] Theorem
⊢ ∀x l.
UNZIP (SNOC x l) =
(SNOC (FST x) (FST (UNZIP l)),SNOC (SND x) (SND (UNZIP l)))
[UNZIP_ZIP] Theorem
⊢ ∀l1 l2. LENGTH l1 = LENGTH l2 ⇒ UNZIP (ZIP (l1,l2)) = (l1,l2)
[ZIP] Theorem
⊢ ZIP ([],[]) = [] ∧
∀x1 l1 x2 l2. ZIP (x1::l1,x2::l2) = (x1,x2)::ZIP (l1,l2)
[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_FIRSTN] Theorem
⊢ ∀n a b.
n ≤ LENGTH a ∧ LENGTH a = LENGTH b ⇒
ZIP (TAKE n a,TAKE n b) = TAKE n (ZIP (a,b))
[ZIP_FIRSTN_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))
[ZIP_GENLIST] Theorem
⊢ ∀l f n.
LENGTH l = n ⇒ ZIP (l,GENLIST f n) = GENLIST (λx. (EL x l,f x)) n
[ZIP_MAP_MAP] Theorem
⊢ ∀ls f g. ZIP (MAP f ls,MAP g ls) = MAP (λx. (f x,g x)) ls
[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))
[ZIP_UNZIP] Theorem
⊢ ∀l. ZIP (UNZIP l) = l
[all_distinct_count_list] Theorem
⊢ ∀n. ALL_DISTINCT (COUNT_LIST n)
[all_distinct_list_el_inj] Theorem
⊢ ∀ls. ALL_DISTINCT ls ⇒ INJ (λj. EL j ls) (count (LENGTH ls)) 𝕌(:α)
[chunks_0] Theorem
⊢ chunks 0 ls = [ls]
[chunks_MAP] Theorem
⊢ ∀n ls. chunks n (MAP f ls) = MAP (MAP f) (chunks n ls)
[chunks_NIL] Theorem
⊢ chunks n [] = [[]]
[chunks_TAKE] Theorem
⊢ ∀n ls m.
divides n m ∧ 0 < m ⇒
chunks n (TAKE m ls) = TAKE (m DIV n) (chunks n ls)
[chunks_ZIP] Theorem
⊢ ∀n ls l2.
LENGTH ls = LENGTH l2 ⇒
chunks n (ZIP (ls,l2)) = MAP ZIP (ZIP (chunks n ls,chunks n l2))
[chunks_append_divides] Theorem
⊢ ∀n l1 l2.
0 < n ∧ divides n (LENGTH l1) ∧ ¬NULL l1 ∧ ¬NULL l2 ⇒
chunks n (l1 ⧺ l2) = chunks n l1 ⧺ chunks n l2
[chunks_def] Theorem
⊢ ∀n ls.
chunks n ls =
if LENGTH ls ≤ n ∨ n = 0 then [ls]
else TAKE n ls::chunks n (DROP n ls)
[chunks_ind] Theorem
⊢ ∀P. (∀n ls. (¬(LENGTH ls ≤ n ∨ n = 0) ⇒ P n (DROP n ls)) ⇒ P n ls) ⇒
∀v v1. P v v1
[chunks_length] Theorem
⊢ chunks (LENGTH ls) ls = [ls]
[chunks_not_nil] Theorem
⊢ ∀n ls. chunks n ls ≠ []
[chunks_tr_aux_def] Theorem
⊢ ∀n ls acc.
chunks_tr_aux n ls acc =
if LENGTH ls ≤ SUC n then REVERSE (ls::acc)
else chunks_tr_aux n (DROP (SUC n) ls) (TAKE (SUC n) ls::acc)
[chunks_tr_aux_ind] Theorem
⊢ ∀P. (∀n ls acc.
(¬(LENGTH ls ≤ SUC n) ⇒
P n (DROP (SUC n) ls) (TAKE (SUC n) ls::acc)) ⇒
P n ls acc) ⇒
∀v v1 v2. P v v1 v2
[chunks_tr_aux_thm] Theorem
⊢ ∀n ls acc. chunks_tr_aux n ls acc = REVERSE acc ⧺ chunks (SUC n) ls
[chunks_tr_thm] Theorem
⊢ chunks_tr = chunks
[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))
[divides_EVERY_LENGTH_chunks] Theorem
⊢ ∀n ls.
ls ≠ [] ∧ divides n (LENGTH ls) ⇒
EVERY ($= n ∘ LENGTH) (chunks n ls)
[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)
[list_to_set_eq_el_image] Theorem
⊢ ∀ls. set ls = IMAGE (λj. EL j ls) (count (LENGTH ls))
[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
[set_list_eq_count] Theorem
⊢ ∀ls n. set ls = count n ⇒ ∀j. j < LENGTH ls ⇒ EL j ls < n
[sublist_ALL_DISTINCT] Theorem
⊢ ∀p q. p ≤ q ∧ ALL_DISTINCT q ⇒ ALL_DISTINCT p
[sublist_MONO_DEC] Theorem
⊢ ∀ls sl. sl ≤ ls ∧ MONO_DEC ls ⇒ MONO_DEC sl
[sublist_MONO_INC] Theorem
⊢ ∀ls sl. sl ≤ ls ∧ MONO_INC ls ⇒ MONO_INC sl
[sublist_antisym] Theorem
⊢ ∀p q. p ≤ q ∧ q ≤ p ⇒ p = q
[sublist_append_extend] Theorem
⊢ ∀h t q. h::t ≤ q ⇔ ∃x y. q = x ⧺ h::y ∧ t ≤ y
[sublist_append_if] Theorem
⊢ ∀p q h. p ≤ q ⇒ p ⧺ [h] ≤ q ⧺ [h]
[sublist_append_iff] Theorem
⊢ ∀p q h. p ≤ q ⇔ p ⧺ [h] ≤ q ⧺ [h]
[sublist_append_include] Theorem
⊢ ∀p q x. p ≤ q ⇒ p ≤ x ⧺ q
[sublist_append_only_if] Theorem
⊢ ∀p q h. p ⧺ [h] ≤ q ⧺ [h] ⇒ p ≤ q
[sublist_append_pair] Theorem
⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ a ⧺ c ≤ b ⧺ d
[sublist_append_prefix] Theorem
⊢ ∀p q. p ≤ q ⧺ p
[sublist_append_remove] Theorem
⊢ ∀p q x. x ⧺ p ≤ q ⇒ p ≤ q
[sublist_append_suffix] Theorem
⊢ ∀p q. p ≤ p ⧺ q
[sublist_cons] Theorem
⊢ ∀h p q. p ≤ q ⇔ h::p ≤ h::q
[sublist_cons_eq] Theorem
⊢ ∀h. (∀p q. h::p ≤ q ⇒ p ≤ q) ⇔ ∀p q. p ≤ q ⇒ p ≤ h::q
[sublist_cons_include] Theorem
⊢ ∀h p q. p ≤ q ⇒ p ≤ h::q
[sublist_cons_remove] Theorem
⊢ ∀h p q. h::p ≤ q ⇒ p ≤ q
[sublist_def] Theorem
⊢ (∀x. [] ≤ x ⇔ T) ∧ (∀t1 h1. h1::t1 ≤ [] ⇔ F) ∧
∀t2 t1 h2 h1.
h1::t1 ≤ h2::t2 ⇔ h1 = h2 ∧ t1 ≤ t2 ∨ h1 ≠ h2 ∧ h1::t1 ≤ t2
[sublist_drop] Theorem
⊢ ∀ls n. DROP n ls ≤ ls
[sublist_every] Theorem
⊢ ∀l ls. l ≤ ls ⇒ ∀P. EVERY P ls ⇒ EVERY P l
[sublist_front] Theorem
⊢ ∀ls. ls ≠ [] ⇒ FRONT ls ≤ ls
[sublist_head_sing] Theorem
⊢ ∀ls. ls ≠ [] ⇒ [HD ls] ≤ ls
[sublist_ind] Theorem
⊢ ∀P. (∀x. P [] x) ∧ (∀h1 t1. P (h1::t1) []) ∧
(∀h1 t1 h2 t2. P t1 t2 ∧ P (h1::t1) t2 ⇒ P (h1::t1) (h2::t2)) ⇒
∀v v1. P v v1
[sublist_induct] Theorem
⊢ ∀P. (∀y. P [] y) ∧ (∀h x y. P x y ∧ x ≤ y ⇒ P (h::x) (h::y)) ∧
(∀h x y. P x y ∧ x ≤ y ⇒ P x (h::y)) ⇒
∀x y. x ≤ y ⇒ P x y
[sublist_last_sing] Theorem
⊢ ∀ls. ls ≠ [] ⇒ [LAST ls] ≤ ls
[sublist_length] Theorem
⊢ ∀p q. p ≤ q ⇒ LENGTH p ≤ LENGTH q
[sublist_mem] Theorem
⊢ ∀p q x. p ≤ q ∧ MEM x p ⇒ MEM x q
[sublist_member_sing] Theorem
⊢ ∀ls x. MEM x ls ⇒ [x] ≤ ls
[sublist_nil] Theorem
⊢ ∀p. [] ≤ p
[sublist_of_nil] Theorem
⊢ ∀p. p ≤ [] ⇔ p = []
[sublist_order] Theorem
⊢ ∀ls sl x.
sl ≤ ls ∧ MEM x sl ⇒
∃l1 l2 l3 l4.
ls = l1 ⧺ [x] ⧺ l2 ∧ sl = l3 ⧺ [x] ⧺ l4 ∧ l3 ≤ l1 ∧ l4 ≤ l2
[sublist_prefix] Theorem
⊢ ∀x p q. p ≤ q ⇔ x ⧺ p ≤ x ⧺ q
[sublist_prefix_nil] Theorem
⊢ ∀p q. p ⧺ q ≤ q ⇒ p = []
[sublist_refl] Theorem
⊢ ∀p. p ≤ p
[sublist_snoc] Theorem
⊢ ∀h p q. p ≤ q ⇒ SNOC h p ≤ SNOC h q
[sublist_subset] Theorem
⊢ ∀ls sl. sl ≤ ls ⇒ set sl ⊆ set ls
[sublist_suffix] Theorem
⊢ ∀x p q. p ≤ q ⇔ p ⧺ x ≤ q ⧺ x
[sublist_tail] Theorem
⊢ ∀ls. ls ≠ [] ⇒ TL ls ≤ ls
[sublist_take] Theorem
⊢ ∀ls n. TAKE n ls ≤ ls
[sublist_trans] Theorem
⊢ ∀p q r. p ≤ q ∧ q ≤ r ⇒ p ≤ r
[sum_of_sums] Theorem
⊢ ∑ (λm. ∑ (f m) (count a)) (count b) =
∑ (λm. f (m DIV a) (m MOD a)) (count (a * b))
[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
HOL 4, Trindemossen-2