Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-23 15:16 deb16814

View on Github →

refactor(*): import content from lean/library/data and library_dev

Estimated changes

added theorem eq_iff_sub_eq_zero
added theorem eq_inv_iff_eq_inv
added theorem eq_of_mul_inv_eq_one
added theorem eq_one_of_inv_eq_one
added theorem eq_sub_iff_add_eq
added theorem inv_eq_inv_iff_eq
added theorem inv_eq_one_iff_eq_one
added theorem left_inverse_inv
added theorem mul_eq_iff_eq_inv_mul
added theorem mul_eq_iff_eq_mul_inv
added theorem sub_eq_iff_eq_add
added def gpow
added theorem gpow_add
added theorem gpow_comm
added theorem inv_pow
added def monoid.pow
added theorem mul_pow
added theorem one_pow
added theorem pow_add
added theorem pow_comm
added theorem pow_ge_one_of_ge_one
added def pow_int
added theorem pow_inv_comm
added theorem pow_mul
added def pow_nat
added theorem pow_one
added theorem pow_pos
added theorem pow_sub
added theorem pow_succ'
added theorem pow_succ
added theorem pow_zero
added theorem lattice.bot_inf_eq
added theorem lattice.bot_le
added theorem lattice.bot_sup_eq
added theorem lattice.bot_unique
added theorem lattice.eq_bot_iff
added theorem lattice.eq_top_iff
added theorem lattice.inf_assoc
added theorem lattice.inf_bot_eq
added theorem lattice.inf_comm
added theorem lattice.inf_eq_top_iff
added theorem lattice.inf_idem
added theorem lattice.inf_le_inf
added theorem lattice.inf_le_left
added theorem lattice.inf_le_right
added theorem lattice.inf_of_le_left
added theorem lattice.inf_sup_self
added theorem lattice.inf_top_eq
added theorem lattice.le_inf
added theorem lattice.le_inf_iff
added theorem lattice.le_inf_sup
added theorem lattice.le_of_inf_eq
added theorem lattice.le_of_sup_eq
added theorem lattice.le_sup_left
added theorem lattice.le_sup_right
added theorem lattice.le_top
added theorem lattice.sup_assoc
added theorem lattice.sup_bot_eq
added theorem lattice.sup_comm
added theorem lattice.sup_eq_bot_iff
added theorem lattice.sup_idem
added theorem lattice.sup_inf_le
added theorem lattice.sup_inf_self
added theorem lattice.sup_le
added theorem lattice.sup_le_iff
added theorem lattice.sup_le_sup
added theorem lattice.sup_of_le_left
added theorem lattice.sup_top_eq
added theorem lattice.top_inf_eq
added theorem lattice.top_sup_eq
added theorem lattice.top_unique
added theorem lattice.bot_inf_eq
added theorem lattice.bot_le
added theorem lattice.bot_sup_eq
added theorem lattice.bot_unique
added theorem lattice.eq_bot_iff
added theorem lattice.eq_top_iff
added def lattice.imp
added theorem lattice.inf_assoc
added theorem lattice.inf_bot_eq
added theorem lattice.inf_comm
added theorem lattice.inf_eq_top_iff
added theorem lattice.inf_idem
added theorem lattice.inf_le_inf
added theorem lattice.inf_le_left'
added theorem lattice.inf_le_left
added theorem lattice.inf_le_right'
added theorem lattice.inf_le_right
added theorem lattice.inf_of_le_left
added theorem lattice.inf_sup_self
added theorem lattice.inf_top_eq
added theorem lattice.le_bot_iff
added theorem lattice.le_inf
added theorem lattice.le_inf_iff
added theorem lattice.le_inf_sup
added theorem lattice.le_of_inf_eq
added theorem lattice.le_of_sup_eq
added theorem lattice.le_sup_left'
added theorem lattice.le_sup_left
added theorem lattice.le_sup_right'
added theorem lattice.le_sup_right
added theorem lattice.le_top
added theorem lattice.sup_assoc
added theorem lattice.sup_bot_eq
added theorem lattice.sup_comm
added theorem lattice.sup_eq_bot_iff
added theorem lattice.sup_idem
added theorem lattice.sup_inf_le
added theorem lattice.sup_inf_self
added theorem lattice.sup_le
added theorem lattice.sup_le_iff
added theorem lattice.sup_le_sup
added theorem lattice.sup_of_le_left
added theorem lattice.sup_top_eq
added theorem lattice.top_inf_eq
added theorem lattice.top_le_iff
added theorem lattice.top_sup_eq
added theorem lattice.top_unique
added theorem le_antisymm'
added theorem lattice.inf_neg_eq_bot
added theorem lattice.inf_sup_left
added theorem lattice.inf_sup_right
added theorem lattice.le_sup_inf
added theorem lattice.neg_bot
added theorem lattice.neg_eq_neg_iff
added theorem lattice.neg_inf
added theorem lattice.neg_inf_eq_bot
added theorem lattice.neg_le_neg
added theorem lattice.neg_neg
added theorem lattice.neg_sup
added theorem lattice.neg_sup_eq_top
added theorem lattice.neg_top
added theorem lattice.neg_unique
added theorem lattice.sub_eq
added theorem lattice.sub_eq_left
added theorem lattice.sup_inf_left
added theorem lattice.sup_inf_right
added theorem lattice.sup_neg_eq_top
added theorem lattice.sup_sub_same
added theorem lattice.monotone_and
added theorem lattice.monotone_or
added theorem lattice.monotone_and
added theorem lattice.monotone_or
added theorem lattice.inf_Sup_eq
added theorem lattice.neg_Inf
added theorem lattice.neg_Sup
added theorem lattice.neg_infi
added theorem lattice.neg_supr
added theorem lattice.sup_Inf_eq
added def lattice.Inf
added theorem lattice.Inf_empty
added theorem lattice.Inf_eq_infi
added theorem lattice.Inf_image
added theorem lattice.Inf_insert
added theorem lattice.Inf_le
added theorem lattice.Inf_le_Inf
added theorem lattice.Inf_le_Sup
added theorem lattice.Inf_le_iff
added theorem lattice.Inf_le_of_le
added theorem lattice.Inf_singleton
added theorem lattice.Inf_union
added theorem lattice.Inf_univ
added def lattice.Sup
added theorem lattice.Sup_empty
added theorem lattice.Sup_eq_supr
added theorem lattice.Sup_image
added theorem lattice.Sup_insert
added theorem lattice.Sup_inter_le
added theorem lattice.Sup_le
added theorem lattice.Sup_le_Sup
added theorem lattice.Sup_singleton
added theorem lattice.Sup_union
added theorem lattice.Sup_univ
added def lattice.infi
added theorem lattice.infi_and
added theorem lattice.infi_comm
added theorem lattice.infi_const
added theorem lattice.infi_empty
added theorem lattice.infi_emptyset
added theorem lattice.infi_exists
added theorem lattice.infi_false
added theorem lattice.infi_inf_eq
added theorem lattice.infi_insert
added theorem lattice.infi_le
added theorem lattice.infi_le_infi2
added theorem lattice.infi_le_infi
added theorem lattice.infi_le_of_le
added theorem lattice.infi_or
added theorem lattice.infi_prod
added theorem lattice.infi_sigma
added theorem lattice.infi_singleton
added theorem lattice.infi_subtype
added theorem lattice.infi_sum
added theorem lattice.infi_true
added theorem lattice.infi_union
added theorem lattice.infi_unit
added theorem lattice.infi_univ
added theorem lattice.le_Inf
added theorem lattice.le_Inf_inter
added theorem lattice.le_Sup
added theorem lattice.le_Sup_iff
added theorem lattice.le_Sup_of_le
added theorem lattice.le_infi
added theorem lattice.le_infi_iff
added theorem lattice.le_supr
added theorem lattice.le_supr_of_le
added def lattice.supr
added theorem lattice.supr_and
added theorem lattice.supr_comm
added theorem lattice.supr_const
added theorem lattice.supr_empty
added theorem lattice.supr_emptyset
added theorem lattice.supr_exists
added theorem lattice.supr_false
added theorem lattice.supr_insert
added theorem lattice.supr_le
added theorem lattice.supr_le_iff
added theorem lattice.supr_le_supr2
added theorem lattice.supr_le_supr
added theorem lattice.supr_or
added theorem lattice.supr_prod
added theorem lattice.supr_sigma
added theorem lattice.supr_singleton
added theorem lattice.supr_subtype
added theorem lattice.supr_sum
added theorem lattice.supr_sup_eq
added theorem lattice.supr_true
added theorem lattice.supr_union
added theorem lattice.supr_unit
added theorem lattice.supr_univ
added theorem set.subset_union_left
added theorem set.subset_union_right
added theorem insert_def
added theorem insert_eq_of_mem
added theorem insert_of_has_insert
added theorem inter_def
added theorem inter_left_comm
added def lattice.Inf
added theorem lattice.Inf_empty
added theorem lattice.Inf_eq_infi
added theorem lattice.Inf_image
added theorem lattice.Inf_insert
added theorem lattice.Inf_le
added theorem lattice.Inf_le_Inf
added theorem lattice.Inf_le_Sup
added theorem lattice.Inf_le_iff
added theorem lattice.Inf_le_of_le
added theorem lattice.Inf_singleton
added theorem lattice.Inf_union
added theorem lattice.Inf_univ
added def lattice.Sup
added theorem lattice.Sup_empty
added theorem lattice.Sup_eq_supr
added theorem lattice.Sup_image
added theorem lattice.Sup_insert
added theorem lattice.Sup_inter_le
added theorem lattice.Sup_le
added theorem lattice.Sup_le_Sup
added theorem lattice.Sup_singleton
added theorem lattice.Sup_union
added theorem lattice.Sup_univ
added theorem lattice.foo'
added theorem lattice.foo
added def lattice.infi
added theorem lattice.infi_and
added theorem lattice.infi_comm
added theorem lattice.infi_const
added theorem lattice.infi_empty
added theorem lattice.infi_emptyset
added theorem lattice.infi_exists
added theorem lattice.infi_false
added theorem lattice.infi_inf_eq
added theorem lattice.infi_insert
added theorem lattice.infi_le'
added theorem lattice.infi_le
added theorem lattice.infi_le_infi2
added theorem lattice.infi_le_infi
added theorem lattice.infi_le_of_le
added theorem lattice.infi_or
added theorem lattice.infi_prod
added theorem lattice.infi_sigma
added theorem lattice.infi_singleton
added theorem lattice.infi_subtype
added theorem lattice.infi_sum
added theorem lattice.infi_true
added theorem lattice.infi_union
added theorem lattice.infi_unit
added theorem lattice.infi_univ
added theorem lattice.le_Inf
added theorem lattice.le_Inf_inter
added theorem lattice.le_Sup
added theorem lattice.le_Sup_iff
added theorem lattice.le_Sup_of_le
added theorem lattice.le_infi
added theorem lattice.le_infi_iff
added theorem lattice.le_supr'
added theorem lattice.le_supr
added theorem lattice.le_supr_of_le
added def lattice.supr
added theorem lattice.supr_and
added theorem lattice.supr_comm
added theorem lattice.supr_const
added theorem lattice.supr_empty
added theorem lattice.supr_emptyset
added theorem lattice.supr_exists
added theorem lattice.supr_false
added theorem lattice.supr_insert
added theorem lattice.supr_le
added theorem lattice.supr_le_iff
added theorem lattice.supr_le_supr2
added theorem lattice.supr_le_supr
added theorem lattice.supr_or
added theorem lattice.supr_prod
added theorem lattice.supr_sigma
added theorem lattice.supr_singleton
added theorem lattice.supr_subtype
added theorem lattice.supr_sum
added theorem lattice.supr_sup_eq
added theorem lattice.supr_true
added theorem lattice.supr_union
added theorem lattice.supr_unit
added theorem lattice.supr_univ
added theorem mem_insert_iff
added theorem mem_inter_eq
added theorem mem_set_of
added theorem mem_set_of_eq
added theorem mem_singleton
added theorem mem_singleton_iff
added theorem mem_union_eq
added theorem mem_univ_eq
added theorem nmem_set_of_eq
added theorem set_eq_def
added theorem set_of_false
added theorem singleton_def
added theorem subset_def
added theorem subset_insert
added theorem subset_univ
added theorem union_def
added theorem union_left_comm
added theorem Union_subset_Union2
added theorem Union_subset_Union
added theorem bind_assoc
added theorem compl_image_set_of
added theorem diff_empty
added theorem diff_neq_empty
added def directed
added theorem directed_of_chain
added def directed_on
added theorem directed_on_Union
added theorem eq_of_sup_eq_inf_eq
added theorem filter.Inter_mem_sets
added def filter.at_bot
added def filter.at_top
added theorem filter.bind_def
added theorem filter.bind_mono2
added theorem filter.bind_mono
added theorem filter.bind_sup
added theorem filter.binfi_sup_eq
added def filter.cofinite
added theorem filter.filter_eq
added theorem filter.fmap_principal
added theorem filter.image_mem_map
added theorem filter.inf_principal
added theorem filter.infi_sets_eq'
added theorem filter.infi_sets_eq
added theorem filter.infi_sup_eq
added theorem filter.inter_mem_sets
added def filter.join
added theorem filter.le_lift'
added theorem filter.le_map_vmap
added theorem filter.le_vmap_map
added theorem filter.lift'_cong
added theorem filter.lift'_id
added theorem filter.lift'_infi
added theorem filter.lift'_mono'
added theorem filter.lift'_mono
added theorem filter.lift'_principal
added theorem filter.lift_assoc
added theorem filter.lift_comm
added theorem filter.lift_infi'
added theorem filter.lift_infi
added theorem filter.lift_mono'
added theorem filter.lift_mono
added theorem filter.lift_principal
added theorem filter.lift_sets_eq
added def filter.map
added theorem filter.map_binfi_eq
added theorem filter.map_bot
added theorem filter.map_compose
added theorem filter.map_eq_bot_iff
added theorem filter.map_id
added theorem filter.map_infi_eq
added theorem filter.map_infi_le
added theorem filter.map_lift'_eq2
added theorem filter.map_lift'_eq
added theorem filter.map_lift_eq2
added theorem filter.map_lift_eq
added theorem filter.map_mono
added theorem filter.map_principal
added theorem filter.map_sup
added theorem filter.map_vmap_le
added theorem filter.mem_bind_sets
added theorem filter.mem_bot_sets
added theorem filter.mem_inf_sets
added theorem filter.mem_infi_sets
added theorem filter.mem_join_sets
added theorem filter.mem_lift'
added theorem filter.mem_lift'_iff
added theorem filter.mem_lift
added theorem filter.mem_lift_iff
added theorem filter.mem_map
added theorem filter.mem_prod_iff
added theorem filter.mem_pure
added theorem filter.mem_return_sets
added theorem filter.mem_sup_sets
added theorem filter.mem_vmap_of_mem
added theorem filter.monotone_lift'
added theorem filter.monotone_lift
added theorem filter.monotone_map
added theorem filter.monotone_vmap
added def filter.principal
added theorem filter.principal_bind
added theorem filter.principal_empty
added theorem filter.principal_mono
added theorem filter.principal_univ
added theorem filter.prod_comm
added theorem filter.prod_inf_prod
added theorem filter.prod_lift_lift
added theorem filter.prod_map_map_eq
added theorem filter.prod_mem_prod
added theorem filter.prod_mono
added theorem filter.prod_neq_bot
added theorem filter.prod_same_eq
added theorem filter.pure_def
added theorem filter.return_neq_bot
added theorem filter.seq_mono
added theorem filter.sup_join
added theorem filter.sup_principal
added theorem filter.supr_join
added theorem filter.supr_map
added theorem filter.supr_principal
added theorem filter.supr_sets_eq
added def filter.towards
added theorem filter.ultrafilter_map
added theorem filter.univ_mem_sets'
added theorem filter.univ_mem_sets
added theorem filter.vimage_mem_vmap
added def filter.vmap
added theorem filter.vmap_eq_lift'
added theorem filter.vmap_lift'_eq2
added theorem filter.vmap_lift'_eq
added theorem filter.vmap_lift_eq2
added theorem filter.vmap_lift_eq
added theorem filter.vmap_map
added theorem filter.vmap_mono
added theorem filter.vmap_neq_bot
added theorem filter.vmap_principal
added theorem filter.vmap_vmap_comp
added structure filter
added theorem lattice.Sup_le_iff
added theorem map_bind
added theorem not_not_mem_iff
added theorem prod.fst_swap
added theorem prod.mk.eta
added theorem prod.snd_swap
added def prod.swap
added theorem prod.swap_prod_mk
added theorem prod.swap_swap
added theorem prod.swap_swap_eq
added theorem pure_seq_eq_map
added theorem sUnion_eq_Union
added theorem sUnion_mono
added theorem seq_bind_eq
added theorem seq_eq_bind_map
added theorem set.bind_def
added theorem set.fmap_eq_image
added theorem set.image_swap_prod
added theorem set.mem_prod_eq
added theorem set.mem_seq_iff
added theorem set.monotone_inter
added theorem set.monotone_prod
added theorem set.monotone_set_of
added theorem set.prod_inter_prod
added theorem set.prod_mono
added theorem set.prod_neq_empty_iff
added theorem set.prod_vimage_eq
added theorem set.set_of_mem_eq
added theorem set.vimage_set_of_eq
added theorem singleton_neq_emptyset
added def upwards
added theorem ge_of_eq
added def lattice.gfp
added theorem lattice.gfp_comp
added theorem lattice.gfp_eq
added theorem lattice.gfp_gfp
added theorem lattice.gfp_induct
added theorem lattice.gfp_le
added theorem lattice.le_gfp
added theorem lattice.le_lfp
added def lattice.lfp
added theorem lattice.lfp_comp
added theorem lattice.lfp_eq
added theorem lattice.lfp_induct
added theorem lattice.lfp_le
added theorem lattice.lfp_lfp
added theorem lattice.monotone_gfp
added theorem lattice.monotone_lfp
added def zorn.chain
added inductive zorn.chain_closure
added theorem zorn.chain_insert
added theorem zorn.chain_succ
added def zorn.max_chain
added theorem zorn.max_chain_spec
added def zorn.succ_chain
added theorem zorn.succ_increasing
added theorem zorn.succ_spec
added def zorn.super_chain
added theorem zorn.super_of_not_max
added theorem zorn.zorn
added theorem zorn.zorn_weak_order
added theorem le_dual_eq_le
added theorem le_max_left_iff_true
added theorem le_max_right_iff_true
added theorem max.left_comm
added theorem max.right_comm
added theorem min_right_comm
added def monotone
added theorem monotone_app
added theorem monotone_comp
added theorem monotone_const
added theorem monotone_id
added theorem monotone_lam
added def weak_order_dual
added theorem mul_neg_one_eq_neg
added def bitvec.adc
added def bitvec.add_lsb
added def bitvec.and
added def bitvec.append
added def bitvec.fill_shr
added def bitvec.not
added theorem bitvec.of_nat_succ
added def bitvec.or
added def bitvec.sbb
added def bitvec.sborrow
added def bitvec.sge
added def bitvec.sgt
added def bitvec.shl
added def bitvec.sle
added def bitvec.slt
added def bitvec.sshr
added theorem bitvec.to_nat_append
added theorem bitvec.to_nat_of_nat
added def bitvec.uborrow
added def bitvec.uge
added def bitvec.ugt
added def bitvec.ule
added def bitvec.ult
added def bitvec.ushr
added def bitvec.xor
added def bitvec
added theorem bool.band_assoc
added theorem bool.band_comm
added theorem bool.band_elim_left
added theorem bool.band_elim_right
added theorem bool.band_eq_ff
added theorem bool.band_eq_tt
added theorem bool.band_ff
added theorem bool.band_intro
added theorem bool.band_left_comm
added theorem bool.band_self
added theorem bool.band_tt
added theorem bool.bnot_bnot
added theorem bool.bnot_false
added theorem bool.bnot_true
added theorem bool.bor_assoc
added theorem bool.bor_comm
added theorem bool.bor_eq_ff
added theorem bool.bor_eq_tt
added theorem bool.bor_ff
added theorem bool.bor_inl
added theorem bool.bor_inr
added theorem bool.bor_left_comm
added theorem bool.bor_tt
added def bool.bxor
added theorem bool.bxor_assoc
added theorem bool.bxor_comm
added theorem bool.bxor_ff
added theorem bool.bxor_left_comm
added theorem bool.bxor_self
added theorem bool.bxor_tt
added theorem bool.coe_tt
added theorem bool.cond_ff
added theorem bool.cond_tt
added theorem bool.dichotomy
added theorem bool.eq_ff_of_ne_tt
added theorem bool.eq_tt_of_ne_ff
added theorem bool.ff_band
added theorem bool.ff_bor
added theorem bool.ff_bxor
added theorem bool.ff_bxor_ff
added theorem bool.ff_bxor_tt
added theorem bool.or_of_bor_eq
added theorem bool.tt_band
added theorem bool.tt_bor
added theorem bool.tt_bxor
added theorem bool.tt_bxor_ff
added theorem bool.tt_bxor_tt
added theorem lt_succ_of_lt
added def raise_fin
added theorem bucket_array.foldl_eq
added def bucket_array
added theorem hash_map.contains_iff
added def hash_map.entries
added theorem hash_map.entries_empty
added def hash_map.erase
added def hash_map.find
added theorem hash_map.find_aux_iff
added theorem hash_map.find_empty
added theorem hash_map.find_erase
added theorem hash_map.find_erase_eq
added theorem hash_map.find_erase_ne
added theorem hash_map.find_iff
added theorem hash_map.find_insert
added def hash_map.fold
added def hash_map.insert
added theorem hash_map.insert_lemma
added def hash_map.keys
added theorem hash_map.keys_empty
added theorem hash_map.mem_erase
added theorem hash_map.mem_insert
added theorem hash_map.mk_as_list
added def hash_map.mk_idx
added def hash_map.of_list
added theorem hash_map.valid.eq'
added theorem hash_map.valid.eq
added theorem hash_map.valid.erase
added theorem hash_map.valid.insert
added theorem hash_map.valid.mk
added theorem hash_map.valid.modify
added theorem hash_map.valid.nodup
added theorem hash_map.valid.replace
added def hash_map.valid
added theorem hash_map.valid_aux.eq
added inductive hash_map.valid_aux
added structure hash_map
added def mk_hash_map
added theorem int.neg_add_neg
added theorem neg_nat_succ
added theorem neg_pred
added theorem neg_succ
added theorem neg_succ_of_nat_eq'
added theorem of_nat_sub
added def pred
added theorem pred_nat_succ
added theorem pred_neg_pred
added theorem pred_succ
added def rec_nat_on
added theorem rec_nat_on_neg
added def succ
added theorem succ_neg_nat_succ
added theorem succ_neg_succ
added theorem succ_pred
added def lazy_list.append
added def lazy_list.approx
added def lazy_list.filter
added def lazy_list.for
added def lazy_list.head
added def lazy_list.join
added def lazy_list.map
added def lazy_list.map₂
added def lazy_list.nth
added def lazy_list.tail
added def lazy_list.zip
added inductive lazy_list
added theorem list.append.assoc
added theorem list.append_concat
added theorem list.concat_append
added theorem list.concat_cons
added theorem list.concat_ne_nil
added theorem list.concat_nil
added theorem list.cons_inj
added theorem list.cons_ne_nil
added def list.count
added theorem list.count_append
added theorem list.count_concat
added theorem list.count_cons'
added theorem list.count_cons
added theorem list.count_cons_of_ne
added theorem list.count_cons_self
added theorem list.count_nil
added theorem list.count_pos_of_mem
added theorem list.count_singleton
added theorem list.head_cons
added theorem list.index_of_cons
added theorem list.index_of_nil
added theorem list.index_of_nth
added def list.inth
added theorem list.inth_succ
added theorem list.inth_zero
added def list.ith
added theorem list.ith_succ
added theorem list.ith_zero
added theorem list.last_congr
added theorem list.last_cons_cons
added theorem list.last_singleton
added theorem list.length_taken_le
added theorem list.mem_iff_count_pos
added theorem list.mem_of_count_pos
added theorem list.nth_eq_some
added theorem list.tail_cons
added theorem list.tail_nil
added theorem list.taken_all
added theorem list.taken_all_of_ge
added theorem list.taken_cons
added theorem list.taken_nil
added theorem list.taken_zero
added theorem list.all_cons
added theorem list.all_eq_tt_iff
added theorem list.all_nil
added theorem list.any_cons
added theorem list.any_eq_tt_iff
added theorem list.any_nil
added theorem list.any_of_mem
added def list.dinj
added def list.dinj₁
added def list.dmap
added theorem list.dmap_cons_of_neg
added theorem list.dmap_cons_of_pos
added theorem list.dmap_nil
added def list.flat
added theorem list.foldl_append
added theorem list.foldl_cons
added theorem list.foldl_eq_foldr
added theorem list.foldl_nil
added theorem list.foldl_reverse
added theorem list.foldr_append
added theorem list.foldr_cons
added theorem list.foldr_nil
added theorem list.foldr_reverse
added theorem list.forall_mem_cons
added theorem list.forall_mem_nil
added theorem list.length_mapAccumR
added theorem list.length_map_accumr
added theorem list.length_product
added theorem list.length_replicate
added def list.mapAccumR
added def list.map_accumr
added theorem list.map₂_nil1
added theorem list.map₂_nil2
added theorem list.mem_dmap
added theorem list.mem_product
added theorem list.nil_product
added def list.product
added theorem list.product_cons
added theorem list.product_nil
added def list.replicate
added theorem list.unzip_cons'
added theorem list.unzip_cons
added theorem list.unzip_nil
added theorem list.zip_cons_cons
added theorem list.zip_nil_left
added theorem list.zip_nil_right
added theorem list.zip_unzip
added theorem list.perm.eqv
added theorem list.perm.mem_of_perm
added theorem list.perm.perm_app
added theorem list.perm.perm_app_inv
added theorem list.perm.perm_erase
added theorem list.perm.perm_ext
added theorem list.perm.perm_filter
added theorem list.perm.perm_insert
added theorem list.perm.perm_inter
added theorem list.perm.perm_map
added theorem list.perm.perm_middle
added theorem list.perm.perm_of_qeq
added theorem list.perm.perm_product
added theorem list.perm.perm_rev
added theorem list.perm.perm_union
added inductive list.perm.qeq
added theorem list.perm.qeq_app
added theorem list.perm.qeq_of_mem
added theorem list.perm.qeq_split
added theorem list.perm.xswap
added inductive list.perm
added theorem list.disjoint.comm
added def list.disjoint
added theorem list.disjoint_left
added theorem list.disjoint_nil_left
added theorem list.disjoint_right
added theorem list.erase_append_left
added theorem list.erase_cons
added theorem list.erase_cons_head
added theorem list.erase_cons_tail
added def list.erase_dup
added theorem list.erase_dup_nil
added theorem list.erase_dup_sublist
added theorem list.erase_dup_subset
added theorem list.erase_nil
added theorem list.erase_of_not_mem
added theorem list.erase_sublist
added theorem list.erase_subset
added theorem list.forall_mem_union
added theorem list.insert.def
added theorem list.insert_nil
added theorem list.insert_of_mem
added theorem list.insert_of_not_mem
added theorem list.inter_cons_of_mem
added theorem list.inter_nil
added theorem list.length_upto
added theorem list.lt_of_mem_upto
added theorem list.mem_erase_dup
added theorem list.mem_erase_dup_iff
added theorem list.mem_insert_iff
added theorem list.mem_insert_of_mem
added theorem list.mem_insert_self
added theorem list.mem_inter_iff
added theorem list.mem_of_mem_erase
added theorem list.mem_union_iff
added theorem list.mem_union_left
added theorem list.mem_union_right
added theorem list.mem_upto_of_lt
added inductive list.nodup
added theorem list.nodup_app_comm
added theorem list.nodup_concat
added theorem list.nodup_cons
added theorem list.nodup_erase_dup
added theorem list.nodup_filter
added theorem list.nodup_head
added theorem list.nodup_insert
added theorem list.nodup_map
added theorem list.nodup_middle
added theorem list.nodup_nil
added theorem list.nodup_of_sublist
added theorem list.nodup_product
added theorem list.nodup_singleton
added theorem list.nodup_upto
added theorem list.subset_erase_dup
added theorem list.union_cons
added theorem list.union_nil
added def list.upto
added theorem list.upto_nil
added theorem list.upto_step
added theorem list.upto_succ
added theorem list.length_split_le
added theorem list.length_split_lt
added def list.merge
added def list.merge_sort
added theorem list.perm_merge
added theorem list.perm_merge_sort
added theorem list.perm_split
added def list.sorted
added theorem list.sorted_cons
added theorem list.sorted_merge
added theorem list.sorted_merge_sort
added theorem list.sorted_nil
added theorem list.sorted_singleton
added def list.split
added theorem list.split_cons_of_eq
added theorem nat.add_pos_left
added theorem nat.add_pos_right
added theorem nat.lt_succ_iff_le
added theorem nat.succ_le_succ_iff
added def iterate
added theorem nat.add_eq_addl
added theorem nat.add_one
added theorem nat.add_one_ne_zero
added def nat.addl
added theorem nat.addl_succ_left
added theorem nat.addl_succ_right
added theorem nat.addl_zero_left
added theorem nat.addl_zero_right
added theorem nat.discriminate
added theorem nat.one_add
added theorem nat.one_succ_zero
added theorem nat.sub_induction
added theorem nat.succ_inj
added theorem nat.two_step_induction
added theorem nat.zero_has_zero
added def ball'
added def ball
added theorem ball_of_ball_succ'
added theorem ball_of_ball_succ
added theorem ball_succ_of_ball
added theorem ball_zero'
added theorem ball_zero
added theorem not_ball_of_not
added def step_p
added theorem nat.comprime_one_left
added theorem nat.comprime_one_right
added theorem nat.coprime_mul
added theorem nat.coprime_mul_right
added theorem nat.coprime_of_dvd'
added theorem nat.coprime_of_dvd
added theorem nat.coprime_pow
added theorem nat.coprime_pow_left
added theorem nat.coprime_pow_right
added theorem nat.coprime_swap
added theorem nat.dvd_gcd
added theorem nat.dvd_lcm_left
added theorem nat.dvd_lcm_right
added theorem nat.exists_coprime
added theorem nat.gcd_assoc
added theorem nat.gcd_comm
added theorem nat.gcd_div
added theorem nat.gcd_dvd
added theorem nat.gcd_dvd_left
added theorem nat.gcd_dvd_right
added theorem nat.gcd_mul_lcm
added theorem nat.gcd_mul_left
added theorem nat.gcd_mul_right
added theorem nat.gcd_one_right
added theorem nat.lcm_assoc
added theorem nat.lcm_comm
added theorem nat.lcm_dvd
added theorem nat.lcm_one_left
added theorem nat.lcm_one_right
added theorem nat.lcm_self
added theorem nat.lcm_zero_left
added theorem nat.lcm_zero_right
added theorem nat.dist.def
added def nat.dist
added theorem nat.dist_add_add_left
added theorem nat.dist_add_add_right
added theorem nat.dist_comm
added theorem nat.dist_eq_intro
added theorem nat.dist_eq_sub_of_ge
added theorem nat.dist_eq_sub_of_le
added theorem nat.dist_eq_zero
added theorem nat.dist_mul_left
added theorem nat.dist_mul_right
added theorem nat.dist_pos_of_ne
added theorem nat.dist_self
added theorem nat.dist_succ_succ
added theorem nat.dist_zero_left
added theorem nat.dist_zero_right
added theorem nat.eq_of_dist_eq_zero
added def cast_num
added def cast_pos_num
added def int.of_snum
added def int.of_znum
added def nat.of_num
added def nat.of_pos_num
added def num.bit
added def num.cmp
added def num.of_nat
added def num.pred
added def num.size
added def num.succ'
added def num.succ
added def num.to_znum
added inductive num
added def nzsnum.bit0
added def nzsnum.bit1
added def nzsnum.drec'
added def nzsnum.head
added def nzsnum.not
added def nzsnum.sign
added def nzsnum.tail
added inductive nzsnum
added def pos_num.bit
added def pos_num.cmp
added def pos_num.is_one
added def pos_num.of_nat
added def pos_num.pred'
added def pos_num.pred
added def pos_num.psub
added def pos_num.size
added def pos_num.succ
added inductive pos_num
added def snum.bit0
added def snum.bit1
added def snum.bit
added theorem snum.bit_one
added theorem snum.bit_zero
added def snum.bits
added def snum.cadd
added def snum.czadd
added def snum.drec'
added def snum.head
added def snum.not
added def snum.pred
added def snum.rec'
added def snum.sign
added def snum.succ
added def snum.tail
added def snum.test_bit
added inductive snum
added def znum.pred
added def znum.succ
added def znum.zneg
added inductive znum
added def num.land
added def num.ldiff
added def num.lor
added def num.lxor
added def num.one_bits
added def num.shiftl
added def num.shiftr
added def num.test_bit
added def pos_num.land
added def pos_num.ldiff
added def pos_num.lor
added def pos_num.lxor
added def pos_num.one_bits
added def pos_num.shiftl
added def pos_num.shiftr
added def pos_num.test_bit
added theorem num.add_of_nat
added theorem num.add_succ
added theorem num.add_to_nat
added theorem num.add_zero
added theorem num.bit_to_nat
added theorem num.bitwise_to_nat
added theorem num.cmp_dec
added theorem num.cmp_swap
added theorem num.land_to_nat
added theorem num.ldiff_to_nat
added theorem num.le_iff_cmp
added theorem num.lor_to_nat
added theorem num.lt_iff_cmp
added theorem num.lxor_to_nat
added theorem num.mul_to_nat
added theorem num.of_nat_inj
added theorem num.of_to_nat
added theorem num.one_to_nat
added theorem num.pred_to_nat
added theorem num.shiftl_to_nat
added theorem num.shiftr_to_nat
added theorem num.succ'_to_nat
added theorem num.succ_to_nat
added theorem num.test_bit_to_nat
added theorem num.to_nat_inj
added theorem num.to_of_nat
added theorem num.zero_add
added theorem num.zero_to_nat
added theorem pos_num.add_one
added theorem pos_num.add_succ
added theorem pos_num.add_to_nat
added theorem pos_num.bit0_of_bit0
added theorem pos_num.bit1_of_bit1
added theorem pos_num.bit_to_nat
added theorem pos_num.cmp_dec
added theorem pos_num.cmp_dec_lemma
added theorem pos_num.cmp_swap
added theorem pos_num.le_iff_cmp
added theorem pos_num.lt_iff_cmp
added theorem pos_num.mul_to_nat
added theorem pos_num.of_to_nat
added theorem pos_num.one_add
added theorem pos_num.one_to_nat
added theorem pos_num.pred'_to_nat
added theorem pos_num.pred_to_nat
added theorem pos_num.succ_to_nat
added theorem pos_num.to_nat_inj
added theorem pos_num.to_nat_pos
added def pfun.as_subtype
added theorem pfun.bind_defined
added def pfun.dom
added theorem pfun.dom_iff_graph
added def pfun.eval_opt
added def pfun.fn
added def pfun.graph
added theorem pfun.pure_defined
added def pfun.ran
added def pfun.restrict
added def pfun
added def roption.assert
added theorem roption.assert_defined
added theorem roption.bind_assoc
added theorem roption.bind_defined
added theorem roption.dom_iff_mem
added theorem roption.eq_ret_of_mem
added theorem roption.mem_bind
added theorem roption.mem_ret
added theorem roption.mem_ret_iff
added theorem roption.mem_some
added theorem roption.mem_unique
added theorem roption.of_to_option
added def roption.restrict
added theorem roption.some_bind
added theorem roption.to_of_option
added structure roption
added def nat.succ_pnat
added def nat.to_pnat'
added def nat.to_pnat
added theorem pnat.nat_coe_val
added theorem pnat.to_pnat'_coe
added theorem pnat.to_pnat'_val
added def pnat
added theorem not_antimono
added def rat
added def computation.bind
added theorem computation.bind_assoc
added theorem computation.bind_congr
added theorem computation.bind_ret'
added theorem computation.bind_ret
added theorem computation.equiv.refl
added theorem computation.equiv.symm
added def computation.get
added theorem computation.get_bind
added theorem computation.get_equiv
added theorem computation.get_ret
added theorem computation.get_think
added theorem computation.get_thinkN
added def computation.head
added theorem computation.head_empty
added theorem computation.head_ret
added theorem computation.head_think
added def computation.join
added theorem computation.le_stable
added theorem computation.length_ret
added def computation.lmap
added def computation.map
added theorem computation.map_comp
added theorem computation.map_congr
added theorem computation.map_id
added theorem computation.map_ret'
added theorem computation.map_ret
added theorem computation.map_think'
added theorem computation.map_think
added theorem computation.mem_bind
added theorem computation.mem_map
added theorem computation.mem_unique
added theorem computation.orelse_ret
added theorem computation.ret_bind
added theorem computation.ret_mem
added theorem computation.ret_orelse
added theorem computation.return_def
added def computation.rmap
added def computation.tail
added theorem computation.tail_empty
added theorem computation.tail_ret
added theorem computation.tail_think
added theorem computation.thinkN_mem
added theorem computation.think_bind
added theorem computation.think_mem
added def computation
added def seq.append
added theorem seq.append_assoc
added theorem seq.append_nil
added def seq.bisim_o
added def seq.cases_on
added theorem seq.coinduction2
added theorem seq.coinduction
added def seq.cons
added theorem seq.cons_append
added def seq.corec.F
added def seq.corec
added def seq.corec_eq
added def seq.destruct
added theorem seq.destruct_cons
added theorem seq.destruct_eq_cons
added theorem seq.destruct_eq_nil
added theorem seq.destruct_nil
added def seq.drop
added theorem seq.dropn_add
added theorem seq.dropn_tail
added theorem seq.eq_of_bisim
added theorem seq.exists_of_mem_map
added def seq.head
added theorem seq.head_cons
added theorem seq.head_dropn
added theorem seq.head_eq_destruct
added theorem seq.head_nil
added def seq.join
added theorem seq.join_append
added theorem seq.join_cons
added theorem seq.join_cons_cons
added theorem seq.join_cons_nil
added theorem seq.join_nil
added theorem seq.le_stable
added def seq.map
added theorem seq.map_append
added theorem seq.map_comp
added theorem seq.map_cons
added theorem seq.map_id
added theorem seq.map_nil
added theorem seq.map_nth
added theorem seq.map_tail
added theorem seq.mem_cons
added theorem seq.mem_cons_iff
added theorem seq.mem_cons_of_mem
added theorem seq.mem_map
added theorem seq.mem_rec_on
added def seq.nil
added theorem seq.nil_append
added theorem seq.not_mem_nil
added def seq.nth
added theorem seq.nth_tail
added def seq.of_lazy_list
added def seq.of_list
added def seq.of_list_cons
added def seq.of_list_nil
added def seq.of_stream
added def seq.omap
added def seq.split_at
added def seq.tail
added theorem seq.tail_cons
added theorem seq.tail_nil
added def seq.take
added def seq.to_list'
added def seq.to_list
added def seq.to_stream
added def seq.unzip
added def seq.zip
added def seq.zip_with
added def seq1.bind
added theorem seq1.bind_assoc
added theorem seq1.bind_ret
added def seq1.join
added theorem seq1.join_cons
added theorem seq1.join_join
added theorem seq1.join_map_ret
added theorem seq1.join_nil
added def seq1.map
added theorem seq1.map_id
added theorem seq1.map_join'
added theorem seq1.map_join
added def seq1.ret
added theorem seq1.ret_bind
added def seq1.to_seq
added def seq1
added def seq
added def wseq.all
added def wseq.any
added def wseq.append
added theorem wseq.append_assoc
added theorem wseq.append_nil
added def wseq.bind
added theorem wseq.bind_assoc
added theorem wseq.bind_congr
added theorem wseq.bind_ret
added theorem wseq.bisim_o.imp
added def wseq.bisim_o
added def wseq.cases_on
added def wseq.collect
added def wseq.compute
added def wseq.cons
added theorem wseq.cons_append
added theorem wseq.cons_congr
added def wseq.destruct
added theorem wseq.destruct_append
added theorem wseq.destruct_congr
added theorem wseq.destruct_cons
added theorem wseq.destruct_dropn
added theorem wseq.destruct_flatten
added theorem wseq.destruct_join
added theorem wseq.destruct_map
added theorem wseq.destruct_nil
added theorem wseq.destruct_of_seq
added theorem wseq.destruct_tail
added theorem wseq.destruct_think
added def wseq.drop.aux
added def wseq.drop
added theorem wseq.dropn_add
added theorem wseq.dropn_congr
added theorem wseq.dropn_cons
added theorem wseq.dropn_nil
added theorem wseq.dropn_of_seq
added theorem wseq.dropn_tail
added theorem wseq.dropn_think
added theorem wseq.eq_or_mem_iff_mem
added theorem wseq.equiv.equivalence
added theorem wseq.equiv.ext
added theorem wseq.equiv.refl
added theorem wseq.equiv.symm
added theorem wseq.equiv.trans
added def wseq.equiv
added theorem wseq.exists_nth_of_mem
added theorem wseq.exists_of_mem_map
added def wseq.filter
added def wseq.filter_map
added def wseq.find
added def wseq.find_index
added def wseq.flatten
added theorem wseq.flatten_congr
added theorem wseq.flatten_equiv
added theorem wseq.flatten_ret
added theorem wseq.flatten_think
added def wseq.get
added def wseq.head
added theorem wseq.head_congr
added theorem wseq.head_cons
added theorem wseq.head_nil
added theorem wseq.head_of_seq
added theorem wseq.head_think
added def wseq.index_of
added def wseq.indexes_of
added def wseq.inits
added def wseq.is_empty
added def wseq.is_finite
added def wseq.join
added theorem wseq.join_append
added theorem wseq.join_congr
added def wseq.join_cons
added theorem wseq.join_join
added theorem wseq.join_map_ret
added def wseq.join_nil
added theorem wseq.join_ret
added def wseq.join_think
added def wseq.length
added theorem wseq.length_eq_map
added def wseq.lift_rel
added theorem wseq.lift_rel_append
added theorem wseq.lift_rel_bind
added theorem wseq.lift_rel_destruct
added theorem wseq.lift_rel_flatten
added theorem wseq.lift_rel_join.lem
added theorem wseq.lift_rel_join
added theorem wseq.lift_rel_map
added theorem wseq.lift_rel_o.imp
added def wseq.lift_rel_o
added def wseq.map
added theorem wseq.map_append
added theorem wseq.map_comp
added theorem wseq.map_congr
added theorem wseq.map_cons
added theorem wseq.map_id
added theorem wseq.map_join
added theorem wseq.map_nil
added theorem wseq.map_ret
added theorem wseq.map_think
added theorem wseq.mem_congr
added theorem wseq.mem_cons
added theorem wseq.mem_cons_iff
added theorem wseq.mem_cons_of_mem
added theorem wseq.mem_map
added theorem wseq.mem_of_mem_dropn
added theorem wseq.mem_of_mem_tail
added theorem wseq.mem_rec_on
added theorem wseq.mem_think
added def wseq.nil
added theorem wseq.nil_append
added theorem wseq.not_mem_nil
added def wseq.nth
added theorem wseq.nth_add
added theorem wseq.nth_congr
added theorem wseq.nth_mem
added theorem wseq.nth_of_seq
added theorem wseq.nth_tail
added theorem wseq.nth_terminates_le
added def wseq.of_list
added def wseq.of_list_nil
added def wseq.of_seq
added def wseq.of_stream
added def wseq.productive
added theorem wseq.productive_congr
added def wseq.remove_nth
added def wseq.ret
added theorem wseq.ret_bind
added def wseq.scanl
added theorem wseq.seq_destruct_cons
added theorem wseq.seq_destruct_nil
added def wseq.split_at
added def wseq.tail.aux
added def wseq.tail
added theorem wseq.tail_congr
added theorem wseq.tail_cons
added theorem wseq.tail_nil
added theorem wseq.tail_of_seq
added theorem wseq.tail_think
added def wseq.take
added def wseq.think
added theorem wseq.think_append
added theorem wseq.think_congr
added theorem wseq.think_equiv
added def wseq.to_list
added def wseq.to_list_nil
added theorem wseq.to_list_of_list
added def wseq.to_seq
added theorem wseq.to_seq_of_seq
added def wseq.union
added def wseq.update_nth
added def wseq.zip
added def wseq.zip_with
added def wseq
added theorem set.empty_inter
added theorem set.empty_subset
added theorem set.empty_union
added theorem set.ext
added theorem set.inter_assoc
added theorem set.inter_comm
added theorem set.inter_empty
added theorem set.inter_self
added theorem set.mem_empty_eq
added theorem set.ne_empty_of_mem
added theorem set.not_mem_empty
added theorem set.subset.antisymm
added theorem set.subset.refl
added theorem set.subset.trans
added theorem set.union_assoc
added theorem set.union_comm
added theorem set.union_empty
added theorem set.union_self
added inductive set.finite
added theorem set.finite_image
added theorem set.finite_insert
added theorem set.finite_sUnion
added theorem set.finite_singleton
added theorem set.finite_subset
added theorem set.finite_union
added def set.Inter
added def set.Union
added theorem set.Union_subset
added theorem set.Union_subset_iff
added theorem set.bInter_empty
added theorem set.bInter_insert
added theorem set.bInter_pair
added theorem set.bInter_singleton
added theorem set.bInter_union
added theorem set.bInter_univ
added theorem set.bUnion_empty
added theorem set.bUnion_insert
added theorem set.bUnion_pair
added theorem set.bUnion_singleton
added theorem set.bUnion_subset
added theorem set.bUnion_union
added theorem set.bUnion_univ
added theorem set.compl_Inter
added theorem set.compl_Union
added theorem set.compl_comp_compl
added theorem set.compl_compl
added theorem set.compl_compl_image
added theorem set.compl_empty
added theorem set.compl_eq_univ_diff
added theorem set.compl_inter
added theorem set.compl_inter_self
added theorem set.compl_sInter
added theorem set.compl_sUnion
added theorem set.compl_union
added theorem set.compl_union_self
added theorem set.compl_univ
added theorem set.diff_eq
added theorem set.diff_subset
added def set.disjoint
added theorem set.disjoint_bot_left
added theorem set.disjoint_bot_right
added theorem set.disjoint_symm
added theorem set.empty_ne_univ
added def set.eq_on
added theorem set.eq_sep_of_subset
added theorem set.eq_univ_of_forall
added theorem set.fix_set_compl
added theorem set.image_comp
added theorem set.image_empty
added theorem set.image_id
added theorem set.image_insert_eq
added theorem set.image_subset
added theorem set.image_union
added theorem set.insert_comm
added theorem set.insert_def
added theorem set.insert_eq
added theorem set.insert_eq_of_mem
added theorem set.insert_ne_empty
added theorem set.inter_compl_self
added theorem set.inter_def
added theorem set.inter_distrib_left
added theorem set.inter_left_comm
added theorem set.inter_right_comm
added theorem set.inter_subset_inter
added theorem set.inter_subset_left
added theorem set.inter_subset_right
added theorem set.inter_univ
added theorem set.mem_Inter
added theorem set.mem_Inter_eq
added theorem set.mem_Union_eq
added theorem set.mem_bInter
added theorem set.mem_bUnion
added theorem set.mem_compl
added theorem set.mem_compl_eq
added theorem set.mem_compl_iff
added theorem set.mem_diff
added theorem set.mem_diff_eq
added theorem set.mem_diff_iff
added theorem set.mem_image
added theorem set.mem_image_compl
added theorem set.mem_image_eq
added theorem set.mem_image_of_mem
added theorem set.mem_insert
added theorem set.mem_insert_iff
added theorem set.mem_insert_of_mem
added theorem set.mem_inter
added theorem set.mem_inter_eq
added theorem set.mem_inter_iff
added theorem set.mem_of_mem_diff
added theorem set.mem_powerset
added theorem set.mem_powerset_iff
added theorem set.mem_sInter
added theorem set.mem_sInter_eq
added theorem set.mem_sUnion
added theorem set.mem_sUnion_eq
added theorem set.mem_sep
added theorem set.mem_sep_eq
added theorem set.mem_sep_iff
added theorem set.mem_set_of
added theorem set.mem_set_of_eq
added theorem set.mem_singleton