Structure pred_setTheory


Source File Identifier index Theory binding index

signature pred_setTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BIGINTER : thm
    val BIGUNION : thm
    val BIJ_DEF : thm
    val CARD_DEF : thm
    val CHOICE_DEF : thm
    val COMPL_DEF : thm
    val CROSS_DEF : thm
    val DELETE_DEF : thm
    val DFUNSET : thm
    val DIFF_DEF : thm
    val DISJOINT_DEF : thm
    val EMPTY_DEF : thm
    val FINITE_DEF : thm
    val FUNSET : thm
    val GSPECIFICATION : thm
    val HAS_SIZE : thm
    val IMAGE_DEF : thm
    val INJ_DEF : thm
    val INSERT_DEF : thm
    val INTER_DEF : thm
    val LINV_LO : thm
    val LINV_OPT_def : thm
    val MAX_SET_DEF : thm
    val MIN_SET_DEF : thm
    val POW_DEF : thm
    val PREIMAGE_def : thm
    val PROD_IMAGE_DEF : thm
    val PROD_SET_DEF : thm
    val PSUBSET_DEF : thm
    val REL_RESTRICT_DEF : thm
    val REST_DEF : thm
    val RINV_LO : thm
    val SING_DEF : thm
    val SUBSET_DEF : thm
    val SUM_IMAGE_DEF : thm
    val SUM_SET_DEF : thm
    val SURJ_DEF : thm
    val UNION_DEF : thm
    val UNIV_DEF : thm
    val chooser_def : thm
    val count_def : thm
    val countable_def : thm
    val disjUNION_def : thm
    val enumerate_def : thm
    val equiv_on_def : thm
    val is_measure_maximal_def : thm
    val num_to_pair_def : thm
    val pair_to_num_def : thm
    val pairwise_def : thm
    val partition_def : thm
    val schroeder_close_def : thm
  
  (*  Theorems  *)
    val ABSORPTION : thm
    val ABSORPTION_RWT : thm
    val ABS_DIFF_SUM_IMAGE : thm
    val BIGINTER_EMPTY : thm
    val BIGINTER_INSERT : thm
    val BIGINTER_INTER : thm
    val BIGINTER_SING : thm
    val BIGINTER_SUBSET : thm
    val BIGINTER_UNION : thm
    val BIGINTER_applied : thm
    val BIGUNION_CROSS : thm
    val BIGUNION_EMPTY : thm
    val BIGUNION_EQ_EMPTY : thm
    val BIGUNION_IMAGE_UNIV : thm
    val BIGUNION_INSERT : thm
    val BIGUNION_PAIR : thm
    val BIGUNION_SING : thm
    val BIGUNION_SUBSET : thm
    val BIGUNION_UNION : thm
    val BIGUNION_applied : thm
    val BIGUNION_partition : thm
    val BIJ_ALT : thm
    val BIJ_COMPOSE : thm
    val BIJ_DELETE : thm
    val BIJ_EMPTY : thm
    val BIJ_FINITE : thm
    val BIJ_FINITE_SUBSET : thm
    val BIJ_ID : thm
    val BIJ_IFF_INV : thm
    val BIJ_IMAGE : thm
    val BIJ_IMP_11 : thm
    val BIJ_INJ_SURJ : thm
    val BIJ_INSERT : thm
    val BIJ_INSERT_IMP : thm
    val BIJ_INV : thm
    val BIJ_LINV_BIJ : thm
    val BIJ_LINV_INV : thm
    val BIJ_NUM_COUNTABLE : thm
    val BIJ_SYM : thm
    val BIJ_SYM_IMP : thm
    val BIJ_TRANS : thm
    val BIJ_support : thm
    val CARD_BIGUNION_SAME_SIZED_SETS : thm
    val CARD_COUNT : thm
    val CARD_CROSS : thm
    val CARD_DELETE : thm
    val CARD_DIFF : thm
    val CARD_DIFF_EQN : thm
    val CARD_EMPTY : thm
    val CARD_EQ_0 : thm
    val CARD_IMAGE : thm
    val CARD_INJ_IMAGE : thm
    val CARD_INSERT : thm
    val CARD_INTER_LESS_EQ : thm
    val CARD_LE_MAX_SET : thm
    val CARD_POW : thm
    val CARD_PSUBSET : thm
    val CARD_REST : thm
    val CARD_SING : thm
    val CARD_SING_CROSS : thm
    val CARD_SUBSET : thm
    val CARD_UNION : thm
    val CARD_UNION_EQN : thm
    val CARD_UNION_LE : thm
    val CARD_disjUNION : thm
    val CHOICE_INSERT_REST : thm
    val CHOICE_INTRO : thm
    val CHOICE_NOT_IN_REST : thm
    val CHOICE_SING : thm
    val COMMUTING_ITSET_INSERT : thm
    val COMMUTING_ITSET_RECURSES : thm
    val COMPL_CLAUSES : thm
    val COMPL_COMPL : thm
    val COMPL_EMPTY : thm
    val COMPL_INTER : thm
    val COMPL_SPLITS : thm
    val COMPL_UNION : thm
    val COMPL_applied : thm
    val COMPONENT : thm
    val COUNTABLE_ALT : thm
    val COUNTABLE_ALT_BIJ : thm
    val COUNTABLE_COUNT : thm
    val COUNTABLE_ENUM : thm
    val COUNTABLE_IMAGE_NUM : thm
    val COUNTABLE_NUM : thm
    val COUNTABLE_SUBSET : thm
    val COUNT_11 : thm
    val COUNT_DELETE : thm
    val COUNT_MONO : thm
    val COUNT_NOT_EMPTY : thm
    val COUNT_SUC : thm
    val COUNT_ZERO : thm
    val COUNT_applied : thm
    val CROSS_BIGUNION : thm
    val CROSS_EMPTY : thm
    val CROSS_EMPTY_EQN : thm
    val CROSS_EQNS : thm
    val CROSS_INSERT_LEFT : thm
    val CROSS_INSERT_RIGHT : thm
    val CROSS_SINGS : thm
    val CROSS_SUBSET : thm
    val CROSS_UNIV : thm
    val CROSS_applied : thm
    val DECOMPOSITION : thm
    val DELETE_COMM : thm
    val DELETE_DELETE : thm
    val DELETE_EQ_SING : thm
    val DELETE_INSERT : thm
    val DELETE_INTER : thm
    val DELETE_NON_ELEMENT : thm
    val DELETE_NON_ELEMENT_RWT : thm
    val DELETE_SUBSET : thm
    val DELETE_SUBSET_INSERT : thm
    val DELETE_applied : thm
    val DFUNSET_applied : thm
    val DIFF_BIGINTER : thm
    val DIFF_BIGINTER1 : thm
    val DIFF_COMM : thm
    val DIFF_DIFF : thm
    val DIFF_DIFF_SUBSET : thm
    val DIFF_EMPTY : thm
    val DIFF_EQ_EMPTY : thm
    val DIFF_INSERT : thm
    val DIFF_INTER : thm
    val DIFF_INTER2 : thm
    val DIFF_INTER_COMPL : thm
    val DIFF_INTER_SUBSET : thm
    val DIFF_SAME_UNION : thm
    val DIFF_SUBSET : thm
    val DIFF_UNION : thm
    val DIFF_UNIV : thm
    val DIFF_applied : thm
    val DISJOINT_ALT : thm
    val DISJOINT_BIGINTER : thm
    val DISJOINT_BIGUNION : thm
    val DISJOINT_COUNT : thm
    val DISJOINT_DELETE_SYM : thm
    val DISJOINT_DIFF : thm
    val DISJOINT_DIFFS : thm
    val DISJOINT_EMPTY : thm
    val DISJOINT_EMPTY_REFL : thm
    val DISJOINT_EMPTY_REFL_RWT : thm
    val DISJOINT_IMAGE : thm
    val DISJOINT_INSERT : thm
    val DISJOINT_INSERT' : thm
    val DISJOINT_SING_EMPTY : thm
    val DISJOINT_SUBSET : thm
    val DISJOINT_SYM : thm
    val DISJOINT_UNION : thm
    val DISJOINT_UNION_BOTH : thm
    val ELT_IN_DELETE : thm
    val EMPTY_DELETE : thm
    val EMPTY_DIFF : thm
    val EMPTY_FUNSET : thm
    val EMPTY_IN_POW : thm
    val EMPTY_NOT_IN_partition : thm
    val EMPTY_NOT_UNIV : thm
    val EMPTY_SUBSET : thm
    val EMPTY_UNION : thm
    val EMPTY_applied : thm
    val ENUMERATE : thm
    val EQUAL_SING : thm
    val EQ_SUBSET_SUBSET : thm
    val EQ_UNIV : thm
    val EXISTS_IN_IMAGE : thm
    val EXISTS_IN_INSERT : thm
    val EXPLICIT_ENUMERATE_MONO : thm
    val EXPLICIT_ENUMERATE_NOT_EMPTY : thm
    val EXTENSION : thm
    val FINITELY_INJECTIVE_IMAGE_FINITE : thm
    val FINITE_BIGINTER : thm
    val FINITE_BIGUNION : thm
    val FINITE_BIGUNION_EQ : thm
    val FINITE_BIJ : thm
    val FINITE_BIJ_CARD : thm
    val FINITE_BIJ_CARD_EQ : thm
    val FINITE_BIJ_COUNT : thm
    val FINITE_BIJ_COUNT_EQ : thm
    val FINITE_COMPLETE_INDUCTION : thm
    val FINITE_COUNT : thm
    val FINITE_CROSS : thm
    val FINITE_CROSS_EQ : thm
    val FINITE_DELETE : thm
    val FINITE_DIFF : thm
    val FINITE_DIFF_down : thm
    val FINITE_EMPTY : thm
    val FINITE_HAS_SIZE : thm
    val FINITE_INDUCT : thm
    val FINITE_INJ : thm
    val FINITE_INSERT : thm
    val FINITE_INTER : thm
    val FINITE_ISO_NUM : thm
    val FINITE_POW : thm
    val FINITE_POW_EQN : thm
    val FINITE_PREIMAGE : thm
    val FINITE_PSUBSET_INFINITE : thm
    val FINITE_PSUBSET_UNIV : thm
    val FINITE_REST : thm
    val FINITE_REST_EQ : thm
    val FINITE_SING : thm
    val FINITE_SURJ : thm
    val FINITE_SURJ_BIJ : thm
    val FINITE_StrongOrder_WF : thm
    val FINITE_UNION : thm
    val FINITE_WEAK_ENUMERATE : thm
    val FINITE_WF_noloops : thm
    val FINITE_is_measure_maximal : thm
    val FINITE_partition : thm
    val FORALL_IN_BIGUNION : thm
    val FORALL_IN_IMAGE : thm
    val FORALL_IN_INSERT : thm
    val FORALL_IN_UNION : thm
    val FUNSET_DFUNSET : thm
    val FUNSET_EMPTY : thm
    val FUNSET_INTER : thm
    val FUNSET_THM : thm
    val FUNSET_applied : thm
    val GSPECIFICATION_applied : thm
    val GSPEC_AND : thm
    val GSPEC_EQ : thm
    val GSPEC_EQ2 : thm
    val GSPEC_ETA : thm
    val GSPEC_F : thm
    val GSPEC_F_COND : thm
    val GSPEC_ID : thm
    val GSPEC_IMAGE : thm
    val GSPEC_OR : thm
    val GSPEC_PAIR_ETA : thm
    val GSPEC_T : thm
    val HAS_SIZE_0 : thm
    val HAS_SIZE_CARD : thm
    val HAS_SIZE_SUC : thm
    val IMAGE_11 : thm
    val IMAGE_11_INFINITE : thm
    val IMAGE_BIGUNION : thm
    val IMAGE_COMPOSE : thm
    val IMAGE_CONG : thm
    val IMAGE_DELETE : thm
    val IMAGE_EMPTY : thm
    val IMAGE_EQ_EMPTY : thm
    val IMAGE_EQ_SING : thm
    val IMAGE_FINITE : thm
    val IMAGE_I : thm
    val IMAGE_ID : thm
    val IMAGE_II : thm
    val IMAGE_IMAGE : thm
    val IMAGE_IN : thm
    val IMAGE_INSERT : thm
    val IMAGE_INTER : thm
    val IMAGE_PREIMAGE : thm
    val IMAGE_SING : thm
    val IMAGE_SUBSET : thm
    val IMAGE_SUBSET_gen : thm
    val IMAGE_SURJ : thm
    val IMAGE_UNION : thm
    val IMAGE_applied : thm
    val INFINITE_DIFF_FINITE : thm
    val INFINITE_EXPLICIT_ENUMERATE : thm
    val INFINITE_INHAB : thm
    val INFINITE_INJ : thm
    val INFINITE_INJ_NOT_SURJ : thm
    val INFINITE_NUM_UNIV : thm
    val INFINITE_PAIR_UNIV : thm
    val INFINITE_SUBSET : thm
    val INFINITE_UNIV : thm
    val INJECTIVE_IMAGE_FINITE : thm
    val INJ_BIJ_SUBSET : thm
    val INJ_CARD : thm
    val INJ_CARD_IMAGE : thm
    val INJ_CARD_IMAGE_EQ : thm
    val INJ_COMPOSE : thm
    val INJ_DELETE : thm
    val INJ_EMPTY : thm
    val INJ_EXTEND : thm
    val INJ_ID : thm
    val INJ_IFF : thm
    val INJ_IMAGE : thm
    val INJ_IMAGE_BIJ : thm
    val INJ_IMAGE_SUBSET : thm
    val INJ_INL : thm
    val INJ_INR : thm
    val INJ_INSERT : thm
    val INJ_LINV_OPT : thm
    val INJ_LINV_OPT_IMAGE : thm
    val INJ_SUBSET : thm
    val INSERT_COMM : thm
    val INSERT_DELETE : thm
    val INSERT_DIFF : thm
    val INSERT_EQ_SING : thm
    val INSERT_INSERT : thm
    val INSERT_INTER : thm
    val INSERT_SING_UNION : thm
    val INSERT_SUBSET : thm
    val INSERT_UNION : thm
    val INSERT_UNION_EQ : thm
    val INSERT_UNIV : thm
    val INSERT_applied : thm
    val INTER_ASSOC : thm
    val INTER_BIGUNION : thm
    val INTER_COMM : thm
    val INTER_CROSS : thm
    val INTER_EMPTY : thm
    val INTER_FINITE : thm
    val INTER_IDEMPOT : thm
    val INTER_OVER_UNION : thm
    val INTER_SUBSET : thm
    val INTER_SUBSET_EQN : thm
    val INTER_UNION : thm
    val INTER_UNION_COMPL : thm
    val INTER_UNIV : thm
    val INTER_applied : thm
    val IN_ABS : thm
    val IN_APP : thm
    val IN_BIGINTER : thm
    val IN_BIGINTER_IMAGE : thm
    val IN_BIGUNION : thm
    val IN_BIGUNION_IMAGE : thm
    val IN_COMPL : thm
    val IN_COUNT : thm
    val IN_CROSS : thm
    val IN_DELETE : thm
    val IN_DELETE_EQ : thm
    val IN_DFUNSET : thm
    val IN_DIFF : thm
    val IN_DISJOINT : thm
    val IN_EQ_UNIV_IMP : thm
    val IN_FUNSET : thm
    val IN_GSPEC : thm
    val IN_GSPEC_IFF : thm
    val IN_IMAGE : thm
    val IN_INFINITE_NOT_FINITE : thm
    val IN_INSERT : thm
    val IN_INSERT_EXPAND : thm
    val IN_INTER : thm
    val IN_POW : thm
    val IN_PREIMAGE : thm
    val IN_REST : thm
    val IN_SING : thm
    val IN_UNION : thm
    val IN_UNIV : thm
    val IN_disjUNION : thm
    val ITSET_EMPTY : thm
    val ITSET_IND : thm
    val ITSET_INSERT : thm
    val ITSET_THM : thm
    val ITSET_def : thm
    val ITSET_ind : thm
    val K_SUBSET : thm
    val KoenigsLemma : thm
    val KoenigsLemma_WF : thm
    val LESS_CARD_DIFF : thm
    val LINV_DEF : thm
    val LINV_OPT_THM : thm
    val MAX_SET_ELIM : thm
    val MAX_SET_REWRITES : thm
    val MAX_SET_THM : thm
    val MAX_SET_UNION : thm
    val MEMBER_NOT_EMPTY : thm
    val MIN_SET_ELIM : thm
    val MIN_SET_LEM : thm
    val MIN_SET_LEQ_MAX_SET : thm
    val MIN_SET_THM : thm
    val MIN_SET_UNION : thm
    val NOT_EMPTY_INSERT : thm
    val NOT_EMPTY_SING : thm
    val NOT_EQUAL_SETS : thm
    val NOT_INSERT_EMPTY : thm
    val NOT_IN_EMPTY : thm
    val NOT_IN_FINITE : thm
    val NOT_PSUBSET_EMPTY : thm
    val NOT_SING_EMPTY : thm
    val NOT_UNIV_PSUBSET : thm
    val NUM_SET_WOP : thm
    val PAIR_IN_GSPEC_1 : thm
    val PAIR_IN_GSPEC_2 : thm
    val PAIR_IN_GSPEC_IFF : thm
    val PAIR_IN_GSPEC_same : thm
    val PHP : thm
    val POW_EMPTY : thm
    val POW_EQNS : thm
    val POW_INSERT : thm
    val POW_applied : thm
    val PREIMAGE_ALT : thm
    val PREIMAGE_BIGUNION : thm
    val PREIMAGE_COMP : thm
    val PREIMAGE_COMPL : thm
    val PREIMAGE_COMPL_INTER : thm
    val PREIMAGE_CROSS : thm
    val PREIMAGE_DIFF : thm
    val PREIMAGE_DISJOINT : thm
    val PREIMAGE_EMPTY : thm
    val PREIMAGE_I : thm
    val PREIMAGE_IMAGE : thm
    val PREIMAGE_INTER : thm
    val PREIMAGE_K : thm
    val PREIMAGE_SUBSET : thm
    val PREIMAGE_UNION : thm
    val PREIMAGE_UNIV : thm
    val PREIMAGE_applied : thm
    val PROD_IMAGE_THM : thm
    val PROD_SET_EMPTY : thm
    val PROD_SET_IMAGE_REDUCTION : thm
    val PROD_SET_THM : thm
    val PSUBSET_EQN : thm
    val PSUBSET_FINITE : thm
    val PSUBSET_INSERT_SUBSET : thm
    val PSUBSET_IRREFL : thm
    val PSUBSET_MEMBER : thm
    val PSUBSET_SING : thm
    val PSUBSET_SUBSET_TRANS : thm
    val PSUBSET_TRANS : thm
    val PSUBSET_UNIV : thm
    val RC_PSUBSET : thm
    val RC_SUBSET_THM : thm
    val REL_RESTRICT_EMPTY : thm
    val REL_RESTRICT_SUBSET : thm
    val REST_PSUBSET : thm
    val REST_SING : thm
    val REST_SUBSET : thm
    val REST_applied : thm
    val RINV_DEF : thm
    val RTC_PSUBSET : thm
    val RTC_SUBSET_THM : thm
    val SCHROEDER_BERNSTEIN : thm
    val SCHROEDER_BERNSTEIN_AUTO : thm
    val SCHROEDER_CLOSE : thm
    val SCHROEDER_CLOSED : thm
    val SCHROEDER_CLOSE_SET : thm
    val SCHROEDER_CLOSE_SUBSET : thm
    val SET_CASES : thm
    val SET_EQ_SUBSET : thm
    val SET_MINIMUM : thm
    val SING : thm
    val SING_DELETE : thm
    val SING_EMPTY : thm
    val SING_FINITE : thm
    val SING_IFF_CARD1 : thm
    val SING_IFF_EMPTY_REST : thm
    val SING_INSERT : thm
    val SING_UNION : thm
    val SING_applied : thm
    val SPECIFICATION : thm
    val SUBSET_ADD : thm
    val SUBSET_ANTISYM : thm
    val SUBSET_ANTISYM_EQ : thm
    val SUBSET_BIGINTER : thm
    val SUBSET_BIGUNION : thm
    val SUBSET_BIGUNION_I : thm
    val SUBSET_CROSS : thm
    val SUBSET_DELETE : thm
    val SUBSET_DELETE_BOTH : thm
    val SUBSET_DIFF : thm
    val SUBSET_DIFF_EMPTY : thm
    val SUBSET_DISJOINT : thm
    val SUBSET_EMPTY : thm
    val SUBSET_EQ_CARD : thm
    val SUBSET_FINITE : thm
    val SUBSET_FINITE_I : thm
    val SUBSET_IMAGE : thm
    val SUBSET_INSERT : thm
    val SUBSET_INSERT_DELETE : thm
    val SUBSET_INSERT_RIGHT : thm
    val SUBSET_INTER : thm
    val SUBSET_INTER1 : thm
    val SUBSET_INTER2 : thm
    val SUBSET_INTER_ABSORPTION : thm
    val SUBSET_K : thm
    val SUBSET_MAX_SET : thm
    val SUBSET_MIN_SET : thm
    val SUBSET_OF_INSERT : thm
    val SUBSET_POW : thm
    val SUBSET_PSUBSET_TRANS : thm
    val SUBSET_REFL : thm
    val SUBSET_THM : thm
    val SUBSET_TRANS : thm
    val SUBSET_UNION : thm
    val SUBSET_UNION_ABSORPTION : thm
    val SUBSET_UNIV : thm
    val SUBSET_applied : thm
    val SUBSET_count_MAX_SET : thm
    val SUBSET_reflexive : thm
    val SUBSET_transitive : thm
    val SUM_IMAGE_CONG : thm
    val SUM_IMAGE_DELETE : thm
    val SUM_IMAGE_INJ_o : thm
    val SUM_IMAGE_IN_LE : thm
    val SUM_IMAGE_MONO_LESS : thm
    val SUM_IMAGE_MONO_LESS_EQ : thm
    val SUM_IMAGE_PERMUTES : thm
    val SUM_IMAGE_SING : thm
    val SUM_IMAGE_SUBSET_LE : thm
    val SUM_IMAGE_THM : thm
    val SUM_IMAGE_UNION : thm
    val SUM_IMAGE_ZERO : thm
    val SUM_IMAGE_lower_bound : thm
    val SUM_IMAGE_upper_bound : thm
    val SUM_SAME_IMAGE : thm
    val SUM_SET_DELETE : thm
    val SUM_SET_EMPTY : thm
    val SUM_SET_IN_LE : thm
    val SUM_SET_SING : thm
    val SUM_SET_SUBSET_LE : thm
    val SUM_SET_THM : thm
    val SUM_SET_UNION : thm
    val SUM_SET_count : thm
    val SUM_SET_count_2 : thm
    val SUM_UNIV : thm
    val SURJ_CARD : thm
    val SURJ_COMPOSE : thm
    val SURJ_EMPTY : thm
    val SURJ_ID : thm
    val SURJ_IMAGE : thm
    val SURJ_IMP_INJ : thm
    val SURJ_INJ_INV : thm
    val TC_PSUBSET : thm
    val TC_SUBSET_THM : thm
    val UNION_ASSOC : thm
    val UNION_COMM : thm
    val UNION_DELETE : thm
    val UNION_DIFF : thm
    val UNION_DIFF_2 : thm
    val UNION_DIFF_EQ : thm
    val UNION_EMPTY : thm
    val UNION_IDEMPOT : thm
    val UNION_OVER_INTER : thm
    val UNION_SUBSET : thm
    val UNION_UNIV : thm
    val UNION_applied : thm
    val UNIQUE_MEMBER_SING : thm
    val UNIV_BOOL : thm
    val UNIV_FUNSET_UNIV : thm
    val UNIV_FUN_TO_BOOL : thm
    val UNIV_NOT_EMPTY : thm
    val UNIV_SUBSET : thm
    val UNIV_applied : thm
    val X_LE_MAX_SET : thm
    val bigunion_countable : thm
    val chooser_compute : thm
    val compl_insert : thm
    val count_EQN : thm
    val count_add : thm
    val count_add1 : thm
    val countable_EMPTY : thm
    val countable_INSERT : thm
    val countable_Uprod : thm
    val countable_Usum : thm
    val countable_image_nats : thm
    val countable_surj : thm
    val cross_countable : thm
    val cross_countable_IFF : thm
    val disjUNION_UNIV : thm
    val finite_countable : thm
    val image_countable : thm
    val in_max_set : thm
    val infinite_num_inj : thm
    val infinite_pow_uncountable : thm
    val infinite_rest : thm
    val inj_countable : thm
    val inj_image_countable_IFF : thm
    val inj_surj : thm
    val inter_countable : thm
    val is_measure_maximal_INSERT : thm
    val is_measure_maximal_SING : thm
    val num_countable : thm
    val pair_to_num_formula : thm
    val pair_to_num_inv : thm
    val pairwise_SUBSET : thm
    val pairwise_UNION : thm
    val partition_CARD : thm
    val partition_SUBSET : thm
    val partition_elements_disjoint : thm
    val partition_elements_interrelate : thm
    val pow_no_surj : thm
    val subset_countable : thm
    val transitive_PSUBSET : thm
    val union_countable : thm
    val union_countable_IFF : thm
  
  val pred_set_grammars : type_grammar.grammar * term_grammar.grammar
  
  val SET_SPEC_ss : simpLib.ssfrag
  
(*
   [numpair] Parent theory of "pred_set"
   
   [BIGINTER]  Definition
      
      ⊢ ∀P. BIGINTER P = {x | ∀s. s ∈ P ⇒ x ∈ s}
   
   [BIGUNION]  Definition
      
      ⊢ ∀P. BIGUNION P = {x | ∃s. s ∈ P ∧ x ∈ s}
   
   [BIJ_DEF]  Definition
      
      ⊢ ∀f s t. BIJ f s t ⇔ INJ f s t ∧ SURJ f s t
   
   [CARD_DEF]  Definition
      
      ⊢ CARD ∅ = 0 ∧
        ∀s. FINITE s ⇒
            ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)
   
   [CHOICE_DEF]  Definition
      
      ⊢ ∀s. s ≠ ∅ ⇒ CHOICE s ∈ s
   
   [COMPL_DEF]  Definition
      
      ⊢ ∀P. COMPL P = 𝕌(:α) DIFF P
   
   [CROSS_DEF]  Definition
      
      ⊢ ∀P Q. P × Q = {p | FST p ∈ P ∧ SND p ∈ Q}
   
   [DELETE_DEF]  Definition
      
      ⊢ ∀s x. s DELETE x = s DIFF {x}
   
   [DFUNSET]  Definition
      
      ⊢ ∀P Q. DFUNSET P Q = (λf. ∀x. x ∈ P ⇒ f x ∈ Q x)
   
   [DIFF_DEF]  Definition
      
      ⊢ ∀s t. s DIFF t = {x | x ∈ s ∧ x ∉ t}
   
   [DISJOINT_DEF]  Definition
      
      ⊢ ∀s t. DISJOINT s t ⇔ s ∩ t = ∅
   
   [EMPTY_DEF]  Definition
      
      ⊢ ∅ = (λx. F)
   
   [FINITE_DEF]  Definition
      
      ⊢ ∀s. FINITE s ⇔ ∀P. P ∅ ∧ (∀s. P s ⇒ ∀e. P (e INSERT s)) ⇒ P s
   
   [FUNSET]  Definition
      
      ⊢ ∀P Q. FUNSET P Q = (λf. ∀x. x ∈ P ⇒ f x ∈ Q)
   
   [GSPECIFICATION]  Definition
      
      ⊢ ∀f v. v ∈ GSPEC f ⇔ ∃x. (v,T) = f x
   
   [HAS_SIZE]  Definition
      
      ⊢ ∀s n. s HAS_SIZE n ⇔ FINITE s ∧ CARD s = n
   
   [IMAGE_DEF]  Definition
      
      ⊢ ∀f s. IMAGE f s = {f x | x ∈ s}
   
   [INJ_DEF]  Definition
      
      ⊢ ∀f s t.
          INJ f s t ⇔
          (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ f x = f y ⇒ x = y
   
   [INSERT_DEF]  Definition
      
      ⊢ ∀x s. x INSERT s = {y | y = x ∨ y ∈ s}
   
   [INTER_DEF]  Definition
      
      ⊢ ∀s t. s ∩ t = {x | x ∈ s ∧ x ∈ t}
   
   [LINV_LO]  Definition
      
      ⊢ ∀f s y. LINV f s y = THE (LINV_OPT f s y)
   
   [LINV_OPT_def]  Definition
      
      ⊢ ∀f s y.
          LINV_OPT f s y =
          if y ∈ IMAGE f s then SOME (@x. x ∈ s ∧ f x = y) else NONE
   
   [MAX_SET_DEF]  Definition
      
      ⊢ ∀s. FINITE s ⇒
            (s ≠ ∅ ⇒ MAX_SET s ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ MAX_SET s) ∧
            (s = ∅ ⇒ MAX_SET s = 0)
   
   [MIN_SET_DEF]  Definition
      
      ⊢ MIN_SET = $LEAST
   
   [POW_DEF]  Definition
      
      ⊢ ∀set. POW set = {s | s ⊆ set}
   
   [PREIMAGE_def]  Definition
      
      ⊢ ∀f s. PREIMAGE f s = {x | f x ∈ s}
   
   [PROD_IMAGE_DEF]  Definition
      
      ⊢ ∀f s. Π f s = ITSET (λe acc. f e * acc) s 1
   
   [PROD_SET_DEF]  Definition
      
      ⊢ PROD_SET = Π I
   
   [PSUBSET_DEF]  Definition
      
      ⊢ ∀s t. s ⊂ t ⇔ s ⊆ t ∧ s ≠ t
   
   [REL_RESTRICT_DEF]  Definition
      
      ⊢ ∀R s x y. REL_RESTRICT R s x y ⇔ x ∈ s ∧ y ∈ s ∧ R x y
   
   [REST_DEF]  Definition
      
      ⊢ ∀s. REST s = s DELETE CHOICE s
   
   [RINV_LO]  Definition
      
      ⊢ ∀f s y. RINV f s y = THE (LINV_OPT f s y)
   
   [SING_DEF]  Definition
      
      ⊢ ∀s. SING s ⇔ ∃x. s = {x}
   
   [SUBSET_DEF]  Definition
      
      ⊢ ∀s t. s ⊆ t ⇔ ∀x. x ∈ s ⇒ x ∈ t
   
   [SUM_IMAGE_DEF]  Definition
      
      ⊢ ∀f s. ∑ f s = ITSET (λe acc. f e + acc) s 0
   
   [SUM_SET_DEF]  Definition
      
      ⊢ SUM_SET = ∑ I
   
   [SURJ_DEF]  Definition
      
      ⊢ ∀f s t.
          SURJ f s t ⇔
          (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x. x ∈ t ⇒ ∃y. y ∈ s ∧ f y = x
   
   [UNION_DEF]  Definition
      
      ⊢ ∀s t. s ∪ t = {x | x ∈ s ∨ x ∈ t}
   
   [UNIV_DEF]  Definition
      
      ⊢ 𝕌(:α) = (λx. T)
   
   [chooser_def]  Definition
      
      ⊢ (∀s. chooser s 0 = CHOICE s) ∧
        ∀s n. chooser s (SUC n) = chooser (REST s) n
   
   [count_def]  Definition
      
      ⊢ ∀n. count n = {m | m < n}
   
   [countable_def]  Definition
      
      ⊢ ∀s. countable s ⇔ ∃f. INJ f s 𝕌(:num)
   
   [disjUNION_def]  Definition
      
      ⊢ ∀A B. A ⊔ B = {INL a | a ∈ A} ∪ {INR b | b ∈ B}
   
   [enumerate_def]  Definition
      
      ⊢ ∀s. enumerate s = @f. BIJ f 𝕌(:num) s
   
   [equiv_on_def]  Definition
      
      ⊢ ∀R s.
          R equiv_on s ⇔
          (∀x. x ∈ s ⇒ R x x) ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ (R x y ⇔ R y x)) ∧
          ∀x y z. x ∈ s ∧ y ∈ s ∧ z ∈ s ∧ R x y ∧ R y z ⇒ R x z
   
   [is_measure_maximal_def]  Definition
      
      ⊢ ∀m s x. is_measure_maximal m s x ⇔ x ∈ s ∧ ∀y. y ∈ s ⇒ m y ≤ m x
   
   [num_to_pair_def]  Definition
      
      ⊢ ∀n. num_to_pair n = (nfst n,nsnd n)
   
   [pair_to_num_def]  Definition
      
      ⊢ ∀m n. pair_to_num (m,n) = m ⊗ n
   
   [pairwise_def]  Definition
      
      ⊢ ∀P s. pairwise P s ⇔ ∀e1 e2. e1 ∈ s ∧ e2 ∈ s ⇒ P e1 e2
   
   [partition_def]  Definition
      
      ⊢ ∀R s. partition R s = {t | ∃x. x ∈ s ∧ t = {y | y ∈ s ∧ R x y}}
   
   [schroeder_close_def]  Definition
      
      ⊢ ∀f s x. schroeder_close f s x ⇔ ∃n. x ∈ FUNPOW (IMAGE f) n s
   
   [ABSORPTION]  Theorem
      
      ⊢ ∀x s. x ∈ s ⇔ x INSERT s = s
   
   [ABSORPTION_RWT]  Theorem
      
      ⊢ ∀x s. x ∈ s ⇒ x INSERT s = s
   
   [ABS_DIFF_SUM_IMAGE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ABS_DIFF (∑ f s) (∑ g s) ≤ ∑ (λx. ABS_DIFF (f x) (g x)) s
   
   [BIGINTER_EMPTY]  Theorem
      
      ⊢ BIGINTER ∅ = 𝕌(:α)
   
   [BIGINTER_INSERT]  Theorem
      
      ⊢ ∀P B. BIGINTER (P INSERT B) = P ∩ BIGINTER B
   
   [BIGINTER_INTER]  Theorem
      
      ⊢ ∀P Q. BIGINTER {P; Q} = P ∩ Q
   
   [BIGINTER_SING]  Theorem
      
      ⊢ ∀P. BIGINTER {P} = P
   
   [BIGINTER_SUBSET]  Theorem
      
      ⊢ ∀sp s t. t ∈ s ∧ t ⊆ sp ⇒ BIGINTER s ⊆ sp
   
   [BIGINTER_UNION]  Theorem
      
      ⊢ ∀s1 s2. BIGINTER (s1 ∪ s2) = BIGINTER s1 ∩ BIGINTER s2
   
   [BIGINTER_applied]  Theorem
      
      ⊢ BIGINTER B x ⇔ ∀P. P ∈ B ⇒ x ∈ P
   
   [BIGUNION_CROSS]  Theorem
      
      ⊢ ∀f s t. BIGUNION (IMAGE f s) × t = BIGUNION (IMAGE (λn. f n × t) s)
   
   [BIGUNION_EMPTY]  Theorem
      
      ⊢ BIGUNION ∅ = ∅
   
   [BIGUNION_EQ_EMPTY]  Theorem
      
      ⊢ ∀P. (BIGUNION P = ∅ ⇔ P = ∅ ∨ P = {∅}) ∧
            (∅ = BIGUNION P ⇔ P = ∅ ∨ P = {∅})
   
   [BIGUNION_IMAGE_UNIV]  Theorem
      
      ⊢ ∀f N.
          (∀n. N ≤ n ⇒ f n = ∅) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE f (count N))
   
   [BIGUNION_INSERT]  Theorem
      
      ⊢ ∀s P. BIGUNION (s INSERT P) = s ∪ BIGUNION P
   
   [BIGUNION_PAIR]  Theorem
      
      ⊢ ∀s t. BIGUNION {s; t} = s ∪ t
   
   [BIGUNION_SING]  Theorem
      
      ⊢ ∀x. BIGUNION {x} = x
   
   [BIGUNION_SUBSET]  Theorem
      
      ⊢ ∀X P. BIGUNION P ⊆ X ⇔ ∀Y. Y ∈ P ⇒ Y ⊆ X
   
   [BIGUNION_UNION]  Theorem
      
      ⊢ ∀s1 s2. BIGUNION (s1 ∪ s2) = BIGUNION s1 ∪ BIGUNION s2
   
   [BIGUNION_applied]  Theorem
      
      ⊢ ∀x sos. BIGUNION sos x ⇔ ∃s. x ∈ s ∧ s ∈ sos
   
   [BIGUNION_partition]  Theorem
      
      ⊢ R equiv_on s ⇒ BIGUNION (partition R s) = s
   
   [BIJ_ALT]  Theorem
      
      ⊢ ∀f s t.
          BIJ f s t ⇔ f ∈ FUNSET s t ∧ ∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ y = f x
   
   [BIJ_COMPOSE]  Theorem
      
      ⊢ ∀f g s t u. BIJ f s t ∧ BIJ g t u ⇒ BIJ (g ∘ f) s u
   
   [BIJ_DELETE]  Theorem
      
      ⊢ ∀s t f. BIJ f s t ⇒ ∀e. e ∈ s ⇒ BIJ f (s DELETE e) (t DELETE f e)
   
   [BIJ_EMPTY]  Theorem
      
      ⊢ ∀f. (∀s. BIJ f ∅ s ⇔ s = ∅) ∧ ∀s. BIJ f s ∅ ⇔ s = ∅
   
   [BIJ_FINITE]  Theorem
      
      ⊢ ∀f s t. BIJ f s t ∧ FINITE s ⇒ FINITE t
   
   [BIJ_FINITE_SUBSET]  Theorem
      
      ⊢ ∀f s t.
          BIJ f 𝕌(:num) s ∧ FINITE t ∧ t ⊆ s ⇒ ∃N. ∀n. N ≤ n ⇒ f n ∉ t
   
   [BIJ_ID]  Theorem
      
      ⊢ ∀s. (λx. x) PERMUTES s
   
   [BIJ_IFF_INV]  Theorem
      
      ⊢ ∀f s t.
          BIJ f s t ⇔
          (∀x. x ∈ s ⇒ f x ∈ t) ∧
          ∃g. (∀x. x ∈ t ⇒ g x ∈ s) ∧ (∀x. x ∈ s ⇒ g (f x) = x) ∧
              ∀x. x ∈ t ⇒ f (g x) = x
   
   [BIJ_IMAGE]  Theorem
      
      ⊢ ∀f s t. BIJ f s t ⇒ t = IMAGE f s
   
   [BIJ_IMP_11]  Theorem
      
      ⊢ BIJ f 𝕌(:α) 𝕌(:β) ⇒ ∀x y. f x = f y ⇔ x = y
   
   [BIJ_INJ_SURJ]  Theorem
      
      ⊢ ∀s t. (∃f. INJ f s t) ∧ (∃g. SURJ g s t) ⇒ ∃h. BIJ h s t
   
   [BIJ_INSERT]  Theorem
      
      ⊢ ∀f e s t.
          BIJ f (e INSERT s) t ⇔
          e ∉ s ∧ f e ∈ t ∧ BIJ f s (t DELETE f e) ∨ e ∈ s ∧ BIJ f s t
   
   [BIJ_INSERT_IMP]  Theorem
      
      ⊢ ∀f e s t.
          e ∉ s ∧ BIJ f (e INSERT s) t ⇒
          ∃u. f e INSERT u = t ∧ f e ∉ u ∧ BIJ f s u
   
   [BIJ_INV]  Theorem
      
      ⊢ ∀f s t.
          BIJ f s t ⇒
          ∃g. BIJ g t s ∧ (∀x. x ∈ s ⇒ (g ∘ f) x = x) ∧
              ∀x. x ∈ t ⇒ (f ∘ g) x = x
   
   [BIJ_LINV_BIJ]  Theorem
      
      ⊢ ∀f s t. BIJ f s t ⇒ BIJ (LINV f s) t s
   
   [BIJ_LINV_INV]  Theorem
      
      ⊢ ∀f s t. BIJ f s t ⇒ ∀x. x ∈ t ⇒ f (LINV f s x) = x
   
   [BIJ_NUM_COUNTABLE]  Theorem
      
      ⊢ ∀s. (∃f. BIJ f 𝕌(:num) s) ⇒ countable s
   
   [BIJ_SYM]  Theorem
      
      ⊢ ∀s t. (∃f. BIJ f s t) ⇔ ∃g. BIJ g t s
   
   [BIJ_SYM_IMP]  Theorem
      
      ⊢ ∀s t. (∃f. BIJ f s t) ⇒ ∃g. BIJ g t s
   
   [BIJ_TRANS]  Theorem
      
      ⊢ ∀s t u. (∃f. BIJ f s t) ∧ (∃g. BIJ g t u) ⇒ ∃h. BIJ h s u
   
   [BIJ_support]  Theorem
      
      ⊢ ∀f s' s.
          f PERMUTES s' ∧ s' ⊆ s ∧ (∀x. x ∉ s' ⇒ f x = x) ⇒ f PERMUTES s
   
   [CARD_BIGUNION_SAME_SIZED_SETS]  Theorem
      
      ⊢ ∀n s.
          FINITE s ∧ (∀e. e ∈ s ⇒ FINITE e ∧ CARD e = n) ∧
          (∀e1 e2. e1 ∈ s ∧ e2 ∈ s ∧ e1 ≠ e2 ⇒ DISJOINT e1 e2) ⇒
          CARD (BIGUNION s) = CARD s * n
   
   [CARD_COUNT]  Theorem
      
      ⊢ ∀n. CARD (count n) = n
   
   [CARD_CROSS]  Theorem
      
      ⊢ ∀P Q. FINITE P ∧ FINITE Q ⇒ CARD (P × Q) = CARD P * CARD Q
   
   [CARD_DELETE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∀x. CARD (s DELETE x) = if x ∈ s then CARD s − 1 else CARD s
   
   [CARD_DIFF]  Theorem
      
      ⊢ ∀t. FINITE t ⇒
            ∀s. FINITE s ⇒ CARD (s DIFF t) = CARD s − CARD (s ∩ t)
   
   [CARD_DIFF_EQN]  Theorem
      
      ⊢ ∀t s. FINITE s ⇒ CARD (s DIFF t) = CARD s − CARD (s ∩ t)
   
   [CARD_EMPTY]  Theorem
      
      ⊢ CARD ∅ = 0
   
   [CARD_EQ_0]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ (CARD s = 0 ⇔ s = ∅)
   
   [CARD_IMAGE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ CARD (IMAGE f s) ≤ CARD s
   
   [CARD_INJ_IMAGE]  Theorem
      
      ⊢ ∀f s.
          (∀x y. f x = f y ⇔ x = y) ∧ FINITE s ⇒ CARD (IMAGE f s) = CARD s
   
   [CARD_INSERT]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∀x. CARD (x INSERT s) = if x ∈ s then CARD s else SUC (CARD s)
   
   [CARD_INTER_LESS_EQ]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. CARD (s ∩ t) ≤ CARD s
   
   [CARD_LE_MAX_SET]  Theorem
      
      ⊢ FINITE s ⇒ CARD s ≤ MAX_SET s + 1
   
   [CARD_POW]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ CARD (POW s) = 2 ** CARD s
   
   [CARD_PSUBSET]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. t ⊂ s ⇒ CARD t < CARD s
   
   [CARD_REST]  Theorem
      
      ⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ CARD (REST s) = CARD s − 1
   
   [CARD_SING]  Theorem
      
      ⊢ ∀x. CARD {x} = 1
   
   [CARD_SING_CROSS]  Theorem
      
      ⊢ ∀x P. FINITE P ⇒ CARD ({x} × P) = CARD P
   
   [CARD_SUBSET]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. t ⊆ s ⇒ CARD t ≤ CARD s
   
   [CARD_UNION]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∀t. FINITE t ⇒ CARD (s ∪ t) + CARD (s ∩ t) = CARD s + CARD t
   
   [CARD_UNION_EQN]  Theorem
      
      ⊢ ∀s t.
          FINITE s ∧ FINITE t ⇒
          CARD (s ∪ t) = CARD s + CARD t − CARD (s ∩ t)
   
   [CARD_UNION_LE]  Theorem
      
      ⊢ FINITE s ∧ FINITE t ⇒ CARD (s ∪ t) ≤ CARD s + CARD t
   
   [CARD_disjUNION]  Theorem
      
      ⊢ FINITE s ∧ FINITE t ⇒ CARD (s ⊔ t) = CARD s + CARD t
   
   [CHOICE_INSERT_REST]  Theorem
      
      ⊢ ∀s. s ≠ ∅ ⇒ CHOICE s INSERT REST s = s
   
   [CHOICE_INTRO]  Theorem
      
      ⊢ (∃x. x ∈ s) ∧ (∀x. x ∈ s ⇒ P x) ⇒ P (CHOICE s)
   
   [CHOICE_NOT_IN_REST]  Theorem
      
      ⊢ ∀s. CHOICE s ∉ REST s
   
   [CHOICE_SING]  Theorem
      
      ⊢ ∀x. CHOICE {x} = x
   
   [COMMUTING_ITSET_INSERT]  Theorem
      
      ⊢ ∀f s.
          (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
          ∀x b. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b)
   
   [COMMUTING_ITSET_RECURSES]  Theorem
      
      ⊢ ∀f e s b.
          (∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
          ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b)
   
   [COMPL_CLAUSES]  Theorem
      
      ⊢ ∀s. COMPL s ∩ s = ∅ ∧ COMPL s ∪ s = 𝕌(:α)
   
   [COMPL_COMPL]  Theorem
      
      ⊢ ∀s. COMPL (COMPL s) = s
   
   [COMPL_EMPTY]  Theorem
      
      ⊢ COMPL ∅ = 𝕌(:α)
   
   [COMPL_INTER]  Theorem
      
      ⊢ x ∩ COMPL x = ∅ ∧ COMPL x ∩ x = ∅
   
   [COMPL_SPLITS]  Theorem
      
      ⊢ ∀p q. p ∩ q ∪ COMPL p ∩ q = q
   
   [COMPL_UNION]  Theorem
      
      ⊢ COMPL (s ∪ t) = COMPL s ∩ COMPL t
   
   [COMPL_applied]  Theorem
      
      ⊢ ∀x s. COMPL s x ⇔ x ∉ s
   
   [COMPONENT]  Theorem
      
      ⊢ ∀x s. x ∈ x INSERT s
   
   [COUNTABLE_ALT]  Theorem
      
      ⊢ ∀s. countable s ⇔ ∃f. ∀x. x ∈ s ⇒ ∃n. f n = x
   
   [COUNTABLE_ALT_BIJ]  Theorem
      
      ⊢ ∀s. countable s ⇔ FINITE s ∨ BIJ (enumerate s) 𝕌(:num) s
   
   [COUNTABLE_COUNT]  Theorem
      
      ⊢ ∀n. countable (count n)
   
   [COUNTABLE_ENUM]  Theorem
      
      ⊢ ∀c. countable c ⇔ c = ∅ ∨ ∃f. c = IMAGE f 𝕌(:num)
   
   [COUNTABLE_IMAGE_NUM]  Theorem
      
      ⊢ ∀f s. countable (IMAGE f s)
   
   [COUNTABLE_NUM]  Theorem
      
      ⊢ ∀s. countable s
   
   [COUNTABLE_SUBSET]  Theorem
      
      ⊢ ∀s t. s ⊆ t ∧ countable t ⇒ countable s
   
   [COUNT_11]  Theorem
      
      ⊢ ∀n1 n2. count n1 = count n2 ⇔ n1 = n2
   
   [COUNT_DELETE]  Theorem
      
      ⊢ ∀n. count n DELETE n = count n
   
   [COUNT_MONO]  Theorem
      
      ⊢ ∀m n. m ≤ n ⇒ count m ⊆ count n
   
   [COUNT_NOT_EMPTY]  Theorem
      
      ⊢ ∀n. 0 < n ⇔ count n ≠ ∅
   
   [COUNT_SUC]  Theorem
      
      ⊢ ∀n. count (SUC n) = n INSERT count n
   
   [COUNT_ZERO]  Theorem
      
      ⊢ count 0 = ∅
   
   [COUNT_applied]  Theorem
      
      ⊢ ∀m n. count n m ⇔ m < n
   
   [CROSS_BIGUNION]  Theorem
      
      ⊢ ∀f s t. s × BIGUNION (IMAGE f t) = BIGUNION (IMAGE (λn. s × f n) t)
   
   [CROSS_EMPTY]  Theorem
      
      ⊢ ∀P. P × ∅ = ∅ ∧ ∅ × P = ∅
   
   [CROSS_EMPTY_EQN]  Theorem
      
      ⊢ s × t = ∅ ⇔ s = ∅ ∨ t = ∅
   
   [CROSS_EQNS]  Theorem
      
      ⊢ ∀s1 s2.
          ∅ × s2 = ∅ ∧ (a INSERT s1) × s2 = IMAGE (λy. (a,y)) s2 ∪ s1 × s2
   
   [CROSS_INSERT_LEFT]  Theorem
      
      ⊢ ∀P Q x. (x INSERT P) × Q = {x} × Q ∪ P × Q
   
   [CROSS_INSERT_RIGHT]  Theorem
      
      ⊢ ∀P Q x. P × (x INSERT Q) = P × {x} ∪ P × Q
   
   [CROSS_SINGS]  Theorem
      
      ⊢ ∀x y. {x} × {y} = {(x,y)}
   
   [CROSS_SUBSET]  Theorem
      
      ⊢ ∀P Q P0 Q0. P0 × Q0 ⊆ P × Q ⇔ P0 = ∅ ∨ Q0 = ∅ ∨ P0 ⊆ P ∧ Q0 ⊆ Q
   
   [CROSS_UNIV]  Theorem
      
      ⊢ 𝕌(:α # β) = 𝕌(:α) × 𝕌(:β)
   
   [CROSS_applied]  Theorem
      
      ⊢ ∀P Q x. (P × Q) x ⇔ FST x ∈ P ∧ SND x ∈ Q
   
   [DECOMPOSITION]  Theorem
      
      ⊢ ∀s x. x ∈ s ⇔ ∃t. s = x INSERT t ∧ x ∉ t
   
   [DELETE_COMM]  Theorem
      
      ⊢ ∀x y s. s DELETE x DELETE y = s DELETE y DELETE x
   
   [DELETE_DELETE]  Theorem
      
      ⊢ ∀x s. s DELETE x DELETE x = s DELETE x
   
   [DELETE_EQ_SING]  Theorem
      
      ⊢ ∀s x. x ∈ s ⇒ (s DELETE x = ∅ ⇔ s = {x})
   
   [DELETE_INSERT]  Theorem
      
      ⊢ ∀x y s.
          (x INSERT s) DELETE y =
          if x = y then s DELETE y else x INSERT s DELETE y
   
   [DELETE_INTER]  Theorem
      
      ⊢ ∀s t x. (s DELETE x) ∩ t = s ∩ t DELETE x
   
   [DELETE_NON_ELEMENT]  Theorem
      
      ⊢ ∀x s. x ∉ s ⇔ s DELETE x = s
   
   [DELETE_NON_ELEMENT_RWT]  Theorem
      
      ⊢ ∀s x. x ∉ s ⇒ s DELETE x = s
   
   [DELETE_SUBSET]  Theorem
      
      ⊢ ∀x s. s DELETE x ⊆ s
   
   [DELETE_SUBSET_INSERT]  Theorem
      
      ⊢ ∀s e s2. s DELETE e ⊆ s2 ⇔ s ⊆ e INSERT s2
   
   [DELETE_applied]  Theorem
      
      ⊢ ∀s x y. (s DELETE y) x ⇔ x ∈ s ∧ x ≠ y
   
   [DFUNSET_applied]  Theorem
      
      ⊢ ∀f P Q. DFUNSET P Q f ⇔ ∀x. x ∈ P ⇒ f x ∈ Q x
   
   [DIFF_BIGINTER]  Theorem
      
      ⊢ ∀sp s.
          (∀t. t ∈ s ⇒ t ⊆ sp) ∧ s ≠ ∅ ⇒
          BIGINTER s = sp DIFF BIGUNION (IMAGE (λu. sp DIFF u) s)
   
   [DIFF_BIGINTER1]  Theorem
      
      ⊢ ∀sp s. sp DIFF BIGINTER s = BIGUNION (IMAGE (λu. sp DIFF u) s)
   
   [DIFF_COMM]  Theorem
      
      ⊢ ∀x y z. x DIFF y DIFF z = x DIFF z DIFF y
   
   [DIFF_DIFF]  Theorem
      
      ⊢ ∀s t. s DIFF t DIFF t = s DIFF t
   
   [DIFF_DIFF_SUBSET]  Theorem
      
      ⊢ ∀s t. t ⊆ s ⇒ s DIFF (s DIFF t) = t
   
   [DIFF_EMPTY]  Theorem
      
      ⊢ ∀s. s DIFF ∅ = s
   
   [DIFF_EQ_EMPTY]  Theorem
      
      ⊢ ∀s. s DIFF s = ∅
   
   [DIFF_INSERT]  Theorem
      
      ⊢ ∀s t x. s DIFF (x INSERT t) = s DELETE x DIFF t
   
   [DIFF_INTER]  Theorem
      
      ⊢ ∀s t g. (s DIFF t) ∩ g = s ∩ g DIFF t
   
   [DIFF_INTER2]  Theorem
      
      ⊢ ∀s t. s DIFF t ∩ s = s DIFF t
   
   [DIFF_INTER_COMPL]  Theorem
      
      ⊢ ∀s t. s DIFF t = s ∩ COMPL t
   
   [DIFF_INTER_SUBSET]  Theorem
      
      ⊢ ∀r s t. r ⊆ s ⇒ r DIFF s ∩ t = r DIFF t
   
   [DIFF_SAME_UNION]  Theorem
      
      ⊢ ∀x y. x ∪ y DIFF x = y DIFF x ∧ x ∪ y DIFF y = x DIFF y
   
   [DIFF_SUBSET]  Theorem
      
      ⊢ ∀s t. s DIFF t ⊆ s
   
   [DIFF_UNION]  Theorem
      
      ⊢ ∀x y z. x DIFF (y ∪ z) = x DIFF y DIFF z
   
   [DIFF_UNIV]  Theorem
      
      ⊢ ∀s. s DIFF 𝕌(:α) = ∅
   
   [DIFF_applied]  Theorem
      
      ⊢ ∀s t x. (s DIFF t) x ⇔ x ∈ s ∧ x ∉ t
   
   [DISJOINT_ALT]  Theorem
      
      ⊢ ∀s t. DISJOINT s t ⇔ ∀x. x ∈ s ⇒ x ∉ t
   
   [DISJOINT_BIGINTER]  Theorem
      
      ⊢ ∀X Y P.
          Y ∈ P ∧ DISJOINT Y X ⇒
          DISJOINT X (BIGINTER P) ∧ DISJOINT (BIGINTER P) X
   
   [DISJOINT_BIGUNION]  Theorem
      
      ⊢ (∀s t. DISJOINT (BIGUNION s) t ⇔ ∀s'. s' ∈ s ⇒ DISJOINT s' t) ∧
        ∀s t. DISJOINT t (BIGUNION s) ⇔ ∀s'. s' ∈ s ⇒ DISJOINT t s'
   
   [DISJOINT_COUNT]  Theorem
      
      ⊢ ∀f. (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
            ∀n. DISJOINT (f n) (BIGUNION (IMAGE f (count n)))
   
   [DISJOINT_DELETE_SYM]  Theorem
      
      ⊢ ∀s t x. DISJOINT (s DELETE x) t ⇔ DISJOINT (t DELETE x) s
   
   [DISJOINT_DIFF]  Theorem
      
      ⊢ ∀s t. DISJOINT t (s DIFF t) ∧ DISJOINT (s DIFF t) t
   
   [DISJOINT_DIFFS]  Theorem
      
      ⊢ ∀f g m n.
          (∀n. f n ⊆ f (SUC n)) ∧ (∀n. g n = f (SUC n) DIFF f n) ∧ m ≠ n ⇒
          DISJOINT (g m) (g n)
   
   [DISJOINT_EMPTY]  Theorem
      
      ⊢ ∀s. DISJOINT ∅ s ∧ DISJOINT s ∅
   
   [DISJOINT_EMPTY_REFL]  Theorem
      
      ⊢ ∀s. s = ∅ ⇔ DISJOINT s s
   
   [DISJOINT_EMPTY_REFL_RWT]  Theorem
      
      ⊢ ∀s. DISJOINT s s ⇔ s = ∅
   
   [DISJOINT_IMAGE]  Theorem
      
      ⊢ (∀x y. f x = f y ⇔ x = y) ⇒
        (DISJOINT (IMAGE f s1) (IMAGE f s2) ⇔ DISJOINT s1 s2)
   
   [DISJOINT_INSERT]  Theorem
      
      ⊢ ∀x s t. DISJOINT (x INSERT s) t ⇔ DISJOINT s t ∧ x ∉ t
   
   [DISJOINT_INSERT']  Theorem
      
      ⊢ ∀x s t. DISJOINT t (x INSERT s) ⇔ DISJOINT t s ∧ x ∉ t
   
   [DISJOINT_SING_EMPTY]  Theorem
      
      ⊢ ∀x. DISJOINT {x} ∅
   
   [DISJOINT_SUBSET]  Theorem
      
      ⊢ ∀s t u. DISJOINT s t ∧ u ⊆ t ⇒ DISJOINT s u
   
   [DISJOINT_SYM]  Theorem
      
      ⊢ ∀s t. DISJOINT s t ⇔ DISJOINT t s
   
   [DISJOINT_UNION]  Theorem
      
      ⊢ ∀s t u. DISJOINT (s ∪ t) u ⇔ DISJOINT s u ∧ DISJOINT t u
   
   [DISJOINT_UNION_BOTH]  Theorem
      
      ⊢ ∀s t u.
          (DISJOINT (s ∪ t) u ⇔ DISJOINT s u ∧ DISJOINT t u) ∧
          (DISJOINT u (s ∪ t) ⇔ DISJOINT s u ∧ DISJOINT t u)
   
   [ELT_IN_DELETE]  Theorem
      
      ⊢ ∀x s. x ∉ s DELETE x
   
   [EMPTY_DELETE]  Theorem
      
      ⊢ ∀x. ∅ DELETE x = ∅
   
   [EMPTY_DIFF]  Theorem
      
      ⊢ ∀s. ∅ DIFF s = ∅
   
   [EMPTY_FUNSET]  Theorem
      
      ⊢ ∀s. FUNSET ∅ s = 𝕌(:α -> β)
   
   [EMPTY_IN_POW]  Theorem
      
      ⊢ ∀s. ∅ ∈ POW s
   
   [EMPTY_NOT_IN_partition]  Theorem
      
      ⊢ R equiv_on s ⇒ ∅ ∉ partition R s
   
   [EMPTY_NOT_UNIV]  Theorem
      
      ⊢ ∅ ≠ 𝕌(:α)
   
   [EMPTY_SUBSET]  Theorem
      
      ⊢ ∀s. ∅ ⊆ s
   
   [EMPTY_UNION]  Theorem
      
      ⊢ ∀s t. s ∪ t = ∅ ⇔ s = ∅ ∧ t = ∅
   
   [EMPTY_applied]  Theorem
      
      ⊢ ∅ x ⇔ F
   
   [ENUMERATE]  Theorem
      
      ⊢ ∀s. (∃f. BIJ f 𝕌(:num) s) ⇔ BIJ (enumerate s) 𝕌(:num) s
   
   [EQUAL_SING]  Theorem
      
      ⊢ ∀x y. {x} = {y} ⇔ x = y
   
   [EQ_SUBSET_SUBSET]  Theorem
      
      ⊢ ∀s t. s = t ⇒ s ⊆ t ∧ t ⊆ s
   
   [EQ_UNIV]  Theorem
      
      ⊢ (∀x. x ∈ s) ⇔ s = 𝕌(:α)
   
   [EXISTS_IN_IMAGE]  Theorem
      
      ⊢ ∀P f s. (∃y. y ∈ IMAGE f s ∧ P y) ⇔ ∃x. x ∈ s ∧ P (f x)
   
   [EXISTS_IN_INSERT]  Theorem
      
      ⊢ ∀P a s. (∃x. x ∈ a INSERT s ∧ P x) ⇔ P a ∨ ∃x. x ∈ s ∧ P x
   
   [EXPLICIT_ENUMERATE_MONO]  Theorem
      
      ⊢ ∀n s. FUNPOW REST n s ⊆ s
   
   [EXPLICIT_ENUMERATE_NOT_EMPTY]  Theorem
      
      ⊢ ∀n s. INFINITE s ⇒ FUNPOW REST n s ≠ ∅
   
   [EXTENSION]  Theorem
      
      ⊢ ∀s t. s = t ⇔ ∀x. x ∈ s ⇔ x ∈ t
   
   [FINITELY_INJECTIVE_IMAGE_FINITE]  Theorem
      
      ⊢ ∀f. (∀x. FINITE {y | x = f y}) ⇒ ∀s. FINITE (IMAGE f s) ⇔ FINITE s
   
   [FINITE_BIGINTER]  Theorem
      
      ⊢ (∃s. s ∈ P ∧ FINITE s) ⇒ FINITE (BIGINTER P)
   
   [FINITE_BIGUNION]  Theorem
      
      ⊢ ∀P. FINITE P ∧ (∀s. s ∈ P ⇒ FINITE s) ⇒ FINITE (BIGUNION P)
   
   [FINITE_BIGUNION_EQ]  Theorem
      
      ⊢ ∀P. FINITE (BIGUNION P) ⇔ FINITE P ∧ ∀s. s ∈ P ⇒ FINITE s
   
   [FINITE_BIJ]  Theorem
      
      ⊢ ∀f s t. FINITE s ∧ BIJ f s t ⇒ FINITE t ∧ CARD s = CARD t
   
   [FINITE_BIJ_CARD]  Theorem
      
      ⊢ ∀f s t. FINITE s ∧ BIJ f s t ⇒ CARD s = CARD t
   
   [FINITE_BIJ_CARD_EQ]  Theorem
      
      ⊢ ∀S. FINITE S ⇒ ∀t f. BIJ f S t ∧ FINITE t ⇒ CARD S = CARD t
   
   [FINITE_BIJ_COUNT]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∃f b. BIJ f (count b) s
   
   [FINITE_BIJ_COUNT_EQ]  Theorem
      
      ⊢ ∀s. FINITE s ⇔ ∃c n. BIJ c (count n) s
   
   [FINITE_COMPLETE_INDUCTION]  Theorem
      
      ⊢ ∀P. (∀x. (∀y. y ⊂ x ⇒ P y) ⇒ FINITE x ⇒ P x) ⇒ ∀x. FINITE x ⇒ P x
   
   [FINITE_COUNT]  Theorem
      
      ⊢ ∀n. FINITE (count n)
   
   [FINITE_CROSS]  Theorem
      
      ⊢ ∀P Q. FINITE P ∧ FINITE Q ⇒ FINITE (P × Q)
   
   [FINITE_CROSS_EQ]  Theorem
      
      ⊢ ∀P Q. FINITE (P × Q) ⇔ P = ∅ ∨ Q = ∅ ∨ FINITE P ∧ FINITE Q
   
   [FINITE_DELETE]  Theorem
      
      ⊢ ∀x s. FINITE (s DELETE x) ⇔ FINITE s
   
   [FINITE_DIFF]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. FINITE (s DIFF t)
   
   [FINITE_DIFF_down]  Theorem
      
      ⊢ ∀P Q. FINITE (P DIFF Q) ∧ FINITE Q ⇒ FINITE P
   
   [FINITE_EMPTY]  Theorem
      
      ⊢ FINITE ∅
   
   [FINITE_HAS_SIZE]  Theorem
      
      ⊢ ∀s. FINITE s ⇔ s HAS_SIZE CARD s
   
   [FINITE_INDUCT]  Theorem
      
      ⊢ ∀P. P ∅ ∧ (∀s. FINITE s ∧ P s ⇒ ∀e. e ∉ s ⇒ P (e INSERT s)) ⇒
            ∀s. FINITE s ⇒ P s
   
   [FINITE_INJ]  Theorem
      
      ⊢ ∀f s t. INJ f s t ∧ FINITE t ⇒ FINITE s
   
   [FINITE_INSERT]  Theorem
      
      ⊢ ∀x s. FINITE (x INSERT s) ⇔ FINITE s
   
   [FINITE_INTER]  Theorem
      
      ⊢ ∀s1 s2. FINITE s1 ∨ FINITE s2 ⇒ FINITE (s1 ∩ s2)
   
   [FINITE_ISO_NUM]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∃f. (∀n m. n < CARD s ∧ m < CARD s ⇒ f n = f m ⇒ n = m) ∧
                s = {f n | n < CARD s}
   
   [FINITE_POW]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ FINITE (POW s)
   
   [FINITE_POW_EQN]  Theorem
      
      ⊢ FINITE (POW s) ⇔ FINITE s
   
   [FINITE_PREIMAGE]  Theorem
      
      ⊢ (∀x y. f x = f y ⇔ x = y) ∧ FINITE s ⇒ FINITE (PREIMAGE f s)
   
   [FINITE_PSUBSET_INFINITE]  Theorem
      
      ⊢ ∀s. INFINITE s ⇔ ∀t. FINITE t ⇒ t ⊆ s ⇒ t ⊂ s
   
   [FINITE_PSUBSET_UNIV]  Theorem
      
      ⊢ INFINITE 𝕌(:α) ⇔ ∀s. FINITE s ⇒ s ⊂ 𝕌(:α)
   
   [FINITE_REST]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ FINITE (REST s)
   
   [FINITE_REST_EQ]  Theorem
      
      ⊢ ∀s. FINITE (REST s) ⇔ FINITE s
   
   [FINITE_SING]  Theorem
      
      ⊢ ∀x. FINITE {x}
   
   [FINITE_SURJ]  Theorem
      
      ⊢ FINITE s ∧ SURJ f s t ⇒ FINITE t
   
   [FINITE_SURJ_BIJ]  Theorem
      
      ⊢ FINITE s ∧ SURJ f s t ∧ CARD t = CARD s ⇒ BIJ f s t
   
   [FINITE_StrongOrder_WF]  Theorem
      
      ⊢ ∀R s.
          FINITE s ∧ StrongOrder (REL_RESTRICT R s) ⇒ WF (REL_RESTRICT R s)
   
   [FINITE_UNION]  Theorem
      
      ⊢ ∀s t. FINITE (s ∪ t) ⇔ FINITE s ∧ FINITE t
   
   [FINITE_WEAK_ENUMERATE]  Theorem
      
      ⊢ ∀s. FINITE s ⇔ ∃f b. ∀e. e ∈ s ⇔ ∃n. n < b ∧ e = f n
   
   [FINITE_WF_noloops]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            (WF (REL_RESTRICT R s) ⇔ irreflexive (REL_RESTRICT R s)⁺)
   
   [FINITE_is_measure_maximal]  Theorem
      
      ⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃x. is_measure_maximal m s x
   
   [FINITE_partition]  Theorem
      
      ⊢ ∀R s.
          FINITE s ⇒
          FINITE (partition R s) ∧ ∀t. t ∈ partition R s ⇒ FINITE t
   
   [FORALL_IN_BIGUNION]  Theorem
      
      ⊢ ∀P s. (∀x. x ∈ BIGUNION s ⇒ P x) ⇔ ∀t x. t ∈ s ∧ x ∈ t ⇒ P x
   
   [FORALL_IN_IMAGE]  Theorem
      
      ⊢ ∀P f s. (∀y. y ∈ IMAGE f s ⇒ P y) ⇔ ∀x. x ∈ s ⇒ P (f x)
   
   [FORALL_IN_INSERT]  Theorem
      
      ⊢ ∀P a s. (∀x. x ∈ a INSERT s ⇒ P x) ⇔ P a ∧ ∀x. x ∈ s ⇒ P x
   
   [FORALL_IN_UNION]  Theorem
      
      ⊢ ∀P s t. (∀x. x ∈ s ∪ t ⇒ P x) ⇔ (∀x. x ∈ s ⇒ P x) ∧ ∀x. x ∈ t ⇒ P x
   
   [FUNSET_DFUNSET]  Theorem
      
      ⊢ ∀x y. FUNSET x y = DFUNSET x (K y)
   
   [FUNSET_EMPTY]  Theorem
      
      ⊢ ∀s f. f ∈ FUNSET s ∅ ⇔ s = ∅
   
   [FUNSET_INTER]  Theorem
      
      ⊢ ∀a b c. FUNSET a (b ∩ c) = FUNSET a b ∩ FUNSET a c
   
   [FUNSET_THM]  Theorem
      
      ⊢ ∀s t f x. f ∈ FUNSET s t ∧ x ∈ s ⇒ f x ∈ t
   
   [FUNSET_applied]  Theorem
      
      ⊢ ∀f P Q. FUNSET P Q f ⇔ ∀x. x ∈ P ⇒ f x ∈ Q
   
   [GSPECIFICATION_applied]  Theorem
      
      ⊢ ∀f v. GSPEC f v ⇔ ∃x. (v,T) = f x
   
   [GSPEC_AND]  Theorem
      
      ⊢ ∀P Q. {x | P x ∧ Q x} = {x | P x} ∩ {x | Q x}
   
   [GSPEC_EQ]  Theorem
      
      ⊢ {x | x = y} = {y}
   
   [GSPEC_EQ2]  Theorem
      
      ⊢ {x | y = x} = {y}
   
   [GSPEC_ETA]  Theorem
      
      ⊢ {x | P x} = P
   
   [GSPEC_F]  Theorem
      
      ⊢ {x | F} = ∅
   
   [GSPEC_F_COND]  Theorem
      
      ⊢ ∀f. (∀x. ¬SND (f x)) ⇒ GSPEC f = ∅
   
   [GSPEC_ID]  Theorem
      
      ⊢ {x | x ∈ y} = y
   
   [GSPEC_IMAGE]  Theorem
      
      ⊢ GSPEC f = IMAGE (FST ∘ f) (SND ∘ f)
   
   [GSPEC_OR]  Theorem
      
      ⊢ ∀P Q. {x | P x ∨ Q x} = {x | P x} ∪ {x | Q x}
   
   [GSPEC_PAIR_ETA]  Theorem
      
      ⊢ {(x,y) | P x y} = UNCURRY P
   
   [GSPEC_T]  Theorem
      
      ⊢ {x | T} = 𝕌(:α)
   
   [HAS_SIZE_0]  Theorem
      
      ⊢ ∀s. s HAS_SIZE 0 ⇔ s = ∅
   
   [HAS_SIZE_CARD]  Theorem
      
      ⊢ ∀s n. s HAS_SIZE n ⇒ CARD s = n
   
   [HAS_SIZE_SUC]  Theorem
      
      ⊢ ∀s n. s HAS_SIZE SUC n ⇔ s ≠ ∅ ∧ ∀a. a ∈ s ⇒ s DELETE a HAS_SIZE n
   
   [IMAGE_11]  Theorem
      
      ⊢ (∀x y. f x = f y ⇔ x = y) ⇒ (IMAGE f s1 = IMAGE f s2 ⇔ s1 = s2)
   
   [IMAGE_11_INFINITE]  Theorem
      
      ⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇒
            ∀s. INFINITE s ⇒ INFINITE (IMAGE f s)
   
   [IMAGE_BIGUNION]  Theorem
      
      ⊢ ∀f M. IMAGE f (BIGUNION M) = BIGUNION (IMAGE (IMAGE f) M)
   
   [IMAGE_COMPOSE]  Theorem
      
      ⊢ ∀f g s. IMAGE (f ∘ g) s = IMAGE f (IMAGE g s)
   
   [IMAGE_CONG]  Theorem
      
      ⊢ ∀f s f' s'.
          s = s' ∧ (∀x. x ∈ s' ⇒ f x = f' x) ⇒ IMAGE f s = IMAGE f' s'
   
   [IMAGE_DELETE]  Theorem
      
      ⊢ ∀f x s. x ∉ s ⇒ IMAGE f (s DELETE x) = IMAGE f s
   
   [IMAGE_EMPTY]  Theorem
      
      ⊢ ∀f. IMAGE f ∅ = ∅
   
   [IMAGE_EQ_EMPTY]  Theorem
      
      ⊢ ∀s f. (IMAGE f s = ∅ ⇔ s = ∅) ∧ (∅ = IMAGE f s ⇔ s = ∅)
   
   [IMAGE_EQ_SING]  Theorem
      
      ⊢ IMAGE f s = {z} ⇔ s ≠ ∅ ∧ ∀x. x ∈ s ⇒ f x = z
   
   [IMAGE_FINITE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀f. FINITE (IMAGE f s)
   
   [IMAGE_I]  Theorem
      
      ⊢ IMAGE I s = s
   
   [IMAGE_ID]  Theorem
      
      ⊢ ∀s. IMAGE (λx. x) s = s
   
   [IMAGE_II]  Theorem
      
      ⊢ IMAGE I = I
   
   [IMAGE_IMAGE]  Theorem
      
      ⊢ ∀f g s. IMAGE f (IMAGE g s) = IMAGE (f ∘ g) s
   
   [IMAGE_IN]  Theorem
      
      ⊢ ∀x s. x ∈ s ⇒ ∀f. f x ∈ IMAGE f s
   
   [IMAGE_INSERT]  Theorem
      
      ⊢ ∀f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s
   
   [IMAGE_INTER]  Theorem
      
      ⊢ ∀f s t. IMAGE f (s ∩ t) ⊆ IMAGE f s ∩ IMAGE f t
   
   [IMAGE_PREIMAGE]  Theorem
      
      ⊢ ∀f s. IMAGE f (PREIMAGE f s) ⊆ s
   
   [IMAGE_SING]  Theorem
      
      ⊢ ∀f x. IMAGE f {x} = {f x}
   
   [IMAGE_SUBSET]  Theorem
      
      ⊢ ∀s t. s ⊆ t ⇒ ∀f. IMAGE f s ⊆ IMAGE f t
   
   [IMAGE_SUBSET_gen]  Theorem
      
      ⊢ ∀f s u t. s ⊆ u ∧ IMAGE f u ⊆ t ⇒ IMAGE f s ⊆ t
   
   [IMAGE_SURJ]  Theorem
      
      ⊢ ∀f s t. SURJ f s t ⇔ IMAGE f s = t
   
   [IMAGE_UNION]  Theorem
      
      ⊢ ∀f s t. IMAGE f (s ∪ t) = IMAGE f s ∪ IMAGE f t
   
   [IMAGE_applied]  Theorem
      
      ⊢ ∀y s f. IMAGE f s y ⇔ ∃x. y = f x ∧ x ∈ s
   
   [INFINITE_DIFF_FINITE]  Theorem
      
      ⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ s DIFF t ≠ ∅
   
   [INFINITE_EXPLICIT_ENUMERATE]  Theorem
      
      ⊢ ∀s. INFINITE s ⇒ INJ (λn. CHOICE (FUNPOW REST n s)) 𝕌(:num) s
   
   [INFINITE_INHAB]  Theorem
      
      ⊢ ∀P. INFINITE P ⇒ ∃x. x ∈ P
   
   [INFINITE_INJ]  Theorem
      
      ⊢ ∀f s t. INJ f s t ∧ INFINITE s ⇒ INFINITE t
   
   [INFINITE_INJ_NOT_SURJ]  Theorem
      
      ⊢ ∀s. INFINITE s ⇔ ∃f. INJ f s s ∧ ¬SURJ f s s
   
   [INFINITE_NUM_UNIV]  Theorem
      
      ⊢ INFINITE 𝕌(:num)
   
   [INFINITE_PAIR_UNIV]  Theorem
      
      ⊢ FINITE 𝕌(:α # β) ⇔ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β)
   
   [INFINITE_SUBSET]  Theorem
      
      ⊢ ∀s. INFINITE s ⇒ ∀t. s ⊆ t ⇒ INFINITE t
   
   [INFINITE_UNIV]  Theorem
      
      ⊢ INFINITE 𝕌(:α) ⇔ ∃f. (∀x y. f x = f y ⇒ x = y) ∧ ∃y. ∀x. f x ≠ y
   
   [INJECTIVE_IMAGE_FINITE]  Theorem
      
      ⊢ ∀f. (∀x y. f x = f y ⇔ x = y) ⇒ ∀s. FINITE (IMAGE f s) ⇔ FINITE s
   
   [INJ_BIJ_SUBSET]  Theorem
      
      ⊢ s0 ⊆ s ∧ INJ f s t ⇒ BIJ f s0 (IMAGE f s0)
   
   [INJ_CARD]  Theorem
      
      ⊢ ∀f s t. INJ f s t ∧ FINITE t ⇒ CARD s ≤ CARD t
   
   [INJ_CARD_IMAGE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ INJ f s t ⇒ CARD (IMAGE f s) = CARD s
   
   [INJ_CARD_IMAGE_EQ]  Theorem
      
      ⊢ INJ f s t ⇒ FINITE s ⇒ CARD (IMAGE f s) = CARD s
   
   [INJ_COMPOSE]  Theorem
      
      ⊢ ∀f g s t u. INJ f s t ∧ INJ g t u ⇒ INJ (g ∘ f) s u
   
   [INJ_DELETE]  Theorem
      
      ⊢ ∀f s t. INJ f s t ⇒ ∀e. e ∈ s ⇒ INJ f (s DELETE e) (t DELETE f e)
   
   [INJ_EMPTY]  Theorem
      
      ⊢ ∀f. (∀s. INJ f ∅ s) ∧ ∀s. INJ f s ∅ ⇔ s = ∅
   
   [INJ_EXTEND]  Theorem
      
      ⊢ ∀b s t x y.
          INJ b s t ∧ x ∉ s ∧ y ∉ t ⇒
          INJ b⦇x ↦ y⦈ (x INSERT s) (y INSERT t)
   
   [INJ_ID]  Theorem
      
      ⊢ ∀s. INJ (λx. x) s s
   
   [INJ_IFF]  Theorem
      
      ⊢ INJ f s t ⇔
        (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x y. x ∈ s ∧ y ∈ s ⇒ (f x = f y ⇔ x = y)
   
   [INJ_IMAGE]  Theorem
      
      ⊢ ∀f s t. INJ f s t ⇒ INJ f s (IMAGE f s)
   
   [INJ_IMAGE_BIJ]  Theorem
      
      ⊢ ∀s f. (∃t. INJ f s t) ⇒ BIJ f s (IMAGE f s)
   
   [INJ_IMAGE_SUBSET]  Theorem
      
      ⊢ ∀f s t. INJ f s t ⇒ IMAGE f s ⊆ t
   
   [INJ_INL]  Theorem
      
      ⊢ (∀x. x ∈ s ⇒ INL x ∈ t) ⇒ INJ INL s t
   
   [INJ_INR]  Theorem
      
      ⊢ (∀x. x ∈ s ⇒ INR x ∈ t) ⇒ INJ INR s t
   
   [INJ_INSERT]  Theorem
      
      ⊢ ∀f x s t.
          INJ f (x INSERT s) t ⇔
          INJ f s t ∧ f x ∈ t ∧ ∀y. y ∈ s ∧ f x = f y ⇒ x = y
   
   [INJ_LINV_OPT]  Theorem
      
      ⊢ INJ f s t ⇒ ∀x y. LINV_OPT f s y = SOME x ⇔ y = f x ∧ x ∈ s ∧ y ∈ t
   
   [INJ_LINV_OPT_IMAGE]  Theorem
      
      ⊢ INJ (LINV_OPT f s) (IMAGE f s) (IMAGE SOME s)
   
   [INJ_SUBSET]  Theorem
      
      ⊢ ∀f s t s0 t0. INJ f s t ∧ s0 ⊆ s ∧ t ⊆ t0 ⇒ INJ f s0 t0
   
   [INSERT_COMM]  Theorem
      
      ⊢ ∀x y s. x INSERT y INSERT s = y INSERT x INSERT s
   
   [INSERT_DELETE]  Theorem
      
      ⊢ ∀x s. x ∈ s ⇒ x INSERT s DELETE x = s
   
   [INSERT_DIFF]  Theorem
      
      ⊢ ∀s t x.
          (x INSERT s) DIFF t =
          if x ∈ t then s DIFF t else x INSERT s DIFF t
   
   [INSERT_EQ_SING]  Theorem
      
      ⊢ ∀s x y. x INSERT s = {y} ⇔ x = y ∧ s ⊆ {y}
   
   [INSERT_INSERT]  Theorem
      
      ⊢ ∀x s. x INSERT x INSERT s = x INSERT s
   
   [INSERT_INTER]  Theorem
      
      ⊢ ∀x s t. (x INSERT s) ∩ t = if x ∈ t then x INSERT s ∩ t else s ∩ t
   
   [INSERT_SING_UNION]  Theorem
      
      ⊢ ∀s x. x INSERT s = {x} ∪ s
   
   [INSERT_SUBSET]  Theorem
      
      ⊢ ∀x s t. x INSERT s ⊆ t ⇔ x ∈ t ∧ s ⊆ t
   
   [INSERT_UNION]  Theorem
      
      ⊢ ∀x s t. (x INSERT s) ∪ t = if x ∈ t then s ∪ t else x INSERT s ∪ t
   
   [INSERT_UNION_EQ]  Theorem
      
      ⊢ ∀x s t. (x INSERT s) ∪ t = x INSERT s ∪ t
   
   [INSERT_UNIV]  Theorem
      
      ⊢ ∀x. x INSERT 𝕌(:α) = 𝕌(:α)
   
   [INSERT_applied]  Theorem
      
      ⊢ ∀x y s. (y INSERT s) x ⇔ x = y ∨ x ∈ s
   
   [INTER_ASSOC]  Theorem
      
      ⊢ ∀s t u. s ∩ (t ∩ u) = s ∩ t ∩ u
   
   [INTER_BIGUNION]  Theorem
      
      ⊢ (∀s t. BIGUNION s ∩ t = BIGUNION {x ∩ t | x ∈ s}) ∧
        ∀s t. t ∩ BIGUNION s = BIGUNION {t ∩ x | x ∈ s}
   
   [INTER_COMM]  Theorem
      
      ⊢ ∀s t. s ∩ t = t ∩ s
   
   [INTER_CROSS]  Theorem
      
      ⊢ ∀A B C D. A × B ∩ (C × D) = A ∩ C × (B ∩ D)
   
   [INTER_EMPTY]  Theorem
      
      ⊢ (∀s. ∅ ∩ s = ∅) ∧ ∀s. s ∩ ∅ = ∅
   
   [INTER_FINITE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. FINITE (s ∩ t)
   
   [INTER_IDEMPOT]  Theorem
      
      ⊢ ∀s. s ∩ s = s
   
   [INTER_OVER_UNION]  Theorem
      
      ⊢ ∀s t u. s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
   
   [INTER_SUBSET]  Theorem
      
      ⊢ (∀s t. s ∩ t ⊆ s) ∧ ∀s t. t ∩ s ⊆ s
   
   [INTER_SUBSET_EQN]  Theorem
      
      ⊢ (A ∩ B = A ⇔ A ⊆ B) ∧ (A ∩ B = B ⇔ B ⊆ A)
   
   [INTER_UNION]  Theorem
      
      ⊢ (A ∪ B) ∩ A = A ∧ (B ∪ A) ∩ A = A ∧ A ∩ (A ∪ B) = A ∧
        A ∩ (B ∪ A) = A
   
   [INTER_UNION_COMPL]  Theorem
      
      ⊢ ∀s t. s ∩ t = COMPL (COMPL s ∪ COMPL t)
   
   [INTER_UNIV]  Theorem
      
      ⊢ (∀s. 𝕌(:α) ∩ s = s) ∧ ∀s. s ∩ 𝕌(:α) = s
   
   [INTER_applied]  Theorem
      
      ⊢ ∀s t x. (s ∩ t) x ⇔ x ∈ s ∧ x ∈ t
   
   [IN_ABS]  Theorem
      
      ⊢ ∀x P. x ∈ (λx. P x) ⇔ P x
   
   [IN_APP]  Theorem
      
      ⊢ ∀x P. x ∈ P ⇔ P x
   
   [IN_BIGINTER]  Theorem
      
      ⊢ x ∈ BIGINTER B ⇔ ∀P. P ∈ B ⇒ x ∈ P
   
   [IN_BIGINTER_IMAGE]  Theorem
      
      ⊢ ∀x f s. x ∈ BIGINTER (IMAGE f s) ⇔ ∀y. y ∈ s ⇒ x ∈ f y
   
   [IN_BIGUNION]  Theorem
      
      ⊢ ∀x sos. x ∈ BIGUNION sos ⇔ ∃s. x ∈ s ∧ s ∈ sos
   
   [IN_BIGUNION_IMAGE]  Theorem
      
      ⊢ ∀f s y. y ∈ BIGUNION (IMAGE f s) ⇔ ∃x. x ∈ s ∧ y ∈ f x
   
   [IN_COMPL]  Theorem
      
      ⊢ ∀x s. x ∈ COMPL s ⇔ x ∉ s
   
   [IN_COUNT]  Theorem
      
      ⊢ ∀m n. m ∈ count n ⇔ m < n
   
   [IN_CROSS]  Theorem
      
      ⊢ ∀P Q x. x ∈ P × Q ⇔ FST x ∈ P ∧ SND x ∈ Q
   
   [IN_DELETE]  Theorem
      
      ⊢ ∀s x y. x ∈ s DELETE y ⇔ x ∈ s ∧ x ≠ y
   
   [IN_DELETE_EQ]  Theorem
      
      ⊢ ∀s x x'. (x ∈ s ⇔ x' ∈ s) ⇔ (x ∈ s DELETE x' ⇔ x' ∈ s DELETE x)
   
   [IN_DFUNSET]  Theorem
      
      ⊢ ∀f P Q. f ∈ DFUNSET P Q ⇔ ∀x. x ∈ P ⇒ f x ∈ Q x
   
   [IN_DIFF]  Theorem
      
      ⊢ ∀s t x. x ∈ s DIFF t ⇔ x ∈ s ∧ x ∉ t
   
   [IN_DISJOINT]  Theorem
      
      ⊢ ∀s t. DISJOINT s t ⇔ ¬∃x. x ∈ s ∧ x ∈ t
   
   [IN_EQ_UNIV_IMP]  Theorem
      
      ⊢ ∀s. s = 𝕌(:α) ⇒ ∀v. v ∈ s
   
   [IN_FUNSET]  Theorem
      
      ⊢ ∀f P Q. f ∈ FUNSET P Q ⇔ ∀x. x ∈ P ⇒ f x ∈ Q
   
   [IN_GSPEC]  Theorem
      
      ⊢ ∀y x P. P y ∧ x = f y ⇒ x ∈ {f x | P x}
   
   [IN_GSPEC_IFF]  Theorem
      
      ⊢ y ∈ {x | P x} ⇔ P y
   
   [IN_IMAGE]  Theorem
      
      ⊢ ∀y s f. y ∈ IMAGE f s ⇔ ∃x. y = f x ∧ x ∈ s
   
   [IN_INFINITE_NOT_FINITE]  Theorem
      
      ⊢ ∀s t. INFINITE s ∧ FINITE t ⇒ ∃x. x ∈ s ∧ x ∉ t
   
   [IN_INSERT]  Theorem
      
      ⊢ ∀x y s. x ∈ y INSERT s ⇔ x = y ∨ x ∈ s
   
   [IN_INSERT_EXPAND]  Theorem
      
      ⊢ ∀x y P. x ∈ y INSERT P ⇔ x = y ∨ x ≠ y ∧ x ∈ P
   
   [IN_INTER]  Theorem
      
      ⊢ ∀s t x. x ∈ s ∩ t ⇔ x ∈ s ∧ x ∈ t
   
   [IN_POW]  Theorem
      
      ⊢ ∀set e. e ∈ POW set ⇔ e ⊆ set
   
   [IN_PREIMAGE]  Theorem
      
      ⊢ ∀f s x. x ∈ PREIMAGE f s ⇔ f x ∈ s
   
   [IN_REST]  Theorem
      
      ⊢ ∀x s. x ∈ REST s ⇔ x ∈ s ∧ x ≠ CHOICE s
   
   [IN_SING]  Theorem
      
      ⊢ ∀x y. x ∈ {y} ⇔ x = y
   
   [IN_UNION]  Theorem
      
      ⊢ ∀s t x. x ∈ s ∪ t ⇔ x ∈ s ∨ x ∈ t
   
   [IN_UNIV]  Theorem
      
      ⊢ ∀x. x ∈ 𝕌(:α)
   
   [IN_disjUNION]  Theorem
      
      ⊢ (INL a ∈ A ⊔ B ⇔ a ∈ A) ∧ (INR b ∈ A ⊔ B ⇔ b ∈ B)
   
   [ITSET_EMPTY]  Theorem
      
      ⊢ ∀f b. ITSET f ∅ b = b
   
   [ITSET_IND]  Theorem
      
      ⊢ ∀P. (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
            ∀v v1. P v v1
   
   [ITSET_INSERT]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∀f x b.
              ITSET f (x INSERT s) b =
              ITSET f (REST (x INSERT s)) (f (CHOICE (x INSERT s)) b)
   
   [ITSET_THM]  Theorem
      
      ⊢ ∀s f b.
          FINITE s ⇒
          ITSET f s b =
          if s = ∅ then b else ITSET f (REST s) (f (CHOICE s) b)
   
   [ITSET_def]  Theorem
      
      ⊢ ∀s f b.
          ITSET f s b =
          if FINITE s then
            if s = ∅ then b else ITSET f (REST s) (f (CHOICE s) b)
          else ARB
   
   [ITSET_ind]  Theorem
      
      ⊢ ∀P. (∀s b. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s) (f (CHOICE s) b)) ⇒ P s b) ⇒
            ∀v v1. P v v1
   
   [K_SUBSET]  Theorem
      
      ⊢ ∀x y. K x ⊆ y ⇔ ¬x ∨ 𝕌(:α) ⊆ y
   
   [KoenigsLemma]  Theorem
      
      ⊢ ∀R. (∀x. FINITE {y | R x y}) ⇒
            ∀x. INFINITE {y | R꙳ x y} ⇒
                ∃f. f 0 = x ∧ ∀n. R (f n) (f (SUC n))
   
   [KoenigsLemma_WF]  Theorem
      
      ⊢ ∀R. (∀x. FINITE {y | R x y}) ∧ WF Rᵀ ⇒ ∀x. FINITE {y | R꙳ x y}
   
   [LESS_CARD_DIFF]  Theorem
      
      ⊢ ∀t. FINITE t ⇒ ∀s. FINITE s ⇒ CARD t < CARD s ⇒ 0 < CARD (s DIFF t)
   
   [LINV_DEF]  Theorem
      
      ⊢ ∀f s t. INJ f s t ⇒ ∀x. x ∈ s ⇒ LINV f s (f x) = x
   
   [LINV_OPT_THM]  Theorem
      
      ⊢ LINV_OPT f s y = SOME x ⇒ x ∈ s ∧ f x = y
   
   [MAX_SET_ELIM]  Theorem
      
      ⊢ ∀P Q.
          FINITE P ∧ (P = ∅ ⇒ Q 0) ∧
          (∀x. (∀y. y ∈ P ⇒ y ≤ x) ∧ x ∈ P ⇒ Q x) ⇒
          Q (MAX_SET P)
   
   [MAX_SET_REWRITES]  Theorem
      
      ⊢ MAX_SET ∅ = 0 ∧ MAX_SET {e} = e
   
   [MAX_SET_THM]  Theorem
      
      ⊢ MAX_SET ∅ = 0 ∧
        ∀e s. FINITE s ⇒ MAX_SET (e INSERT s) = MAX e (MAX_SET s)
   
   [MAX_SET_UNION]  Theorem
      
      ⊢ ∀A B.
          FINITE A ∧ FINITE B ⇒
          MAX_SET (A ∪ B) = MAX (MAX_SET A) (MAX_SET B)
   
   [MEMBER_NOT_EMPTY]  Theorem
      
      ⊢ ∀s. (∃x. x ∈ s) ⇔ s ≠ ∅
   
   [MIN_SET_ELIM]  Theorem
      
      ⊢ ∀P Q.
          P ≠ ∅ ∧ (∀x. (∀y. y ∈ P ⇒ x ≤ y) ∧ x ∈ P ⇒ Q x) ⇒ Q (MIN_SET P)
   
   [MIN_SET_LEM]  Theorem
      
      ⊢ ∀s. s ≠ ∅ ⇒ MIN_SET s ∈ s ∧ ∀x. x ∈ s ⇒ MIN_SET s ≤ x
   
   [MIN_SET_LEQ_MAX_SET]  Theorem
      
      ⊢ ∀s. s ≠ ∅ ∧ FINITE s ⇒ MIN_SET s ≤ MAX_SET s
   
   [MIN_SET_THM]  Theorem
      
      ⊢ (∀e. MIN_SET {e} = e) ∧
        ∀s e1 e2.
          MIN_SET (e1 INSERT e2 INSERT s) = MIN e1 (MIN_SET (e2 INSERT s))
   
   [MIN_SET_UNION]  Theorem
      
      ⊢ ∀A B.
          FINITE A ∧ FINITE B ∧ A ≠ ∅ ∧ B ≠ ∅ ⇒
          MIN_SET (A ∪ B) = MIN (MIN_SET A) (MIN_SET B)
   
   [NOT_EMPTY_INSERT]  Theorem
      
      ⊢ ∀x s. ∅ ≠ x INSERT s
   
   [NOT_EMPTY_SING]  Theorem
      
      ⊢ ∀x. ∅ ≠ {x}
   
   [NOT_EQUAL_SETS]  Theorem
      
      ⊢ ∀s t. s ≠ t ⇔ ∃x. x ∈ t ⇔ x ∉ s
   
   [NOT_INSERT_EMPTY]  Theorem
      
      ⊢ ∀x s. x INSERT s ≠ ∅
   
   [NOT_IN_EMPTY]  Theorem
      
      ⊢ ∀x. x ∉ ∅
   
   [NOT_IN_FINITE]  Theorem
      
      ⊢ INFINITE 𝕌(:α) ⇔ ∀s. FINITE s ⇒ ∃x. x ∉ s
   
   [NOT_PSUBSET_EMPTY]  Theorem
      
      ⊢ ∀s. ¬(s ⊂ ∅)
   
   [NOT_SING_EMPTY]  Theorem
      
      ⊢ ∀x. {x} ≠ ∅
   
   [NOT_UNIV_PSUBSET]  Theorem
      
      ⊢ ∀s. ¬(𝕌(:α) ⊂ s)
   
   [NUM_SET_WOP]  Theorem
      
      ⊢ ∀s. (∃n. n ∈ s) ⇔ ∃n. n ∈ s ∧ ∀m. m ∈ s ⇒ n ≤ m
   
   [PAIR_IN_GSPEC_1]  Theorem
      
      ⊢ (a,b) ∈ {(y,x) | P y} ⇔ P a ∧ b = x
   
   [PAIR_IN_GSPEC_2]  Theorem
      
      ⊢ (a,b) ∈ {(x,y) | P y} ⇔ P b ∧ a = x
   
   [PAIR_IN_GSPEC_IFF]  Theorem
      
      ⊢ (x,y) ∈ {(x,y) | P x y} ⇔ P x y
   
   [PAIR_IN_GSPEC_same]  Theorem
      
      ⊢ (a,b) ∈ {(x,x) | P x} ⇔ P a ∧ a = b
   
   [PHP]  Theorem
      
      ⊢ ∀f s t. FINITE t ∧ CARD t < CARD s ⇒ ¬INJ f s t
   
   [POW_EMPTY]  Theorem
      
      ⊢ ∀s. POW s ≠ ∅
   
   [POW_EQNS]  Theorem
      
      ⊢ POW ∅ = {∅} ∧
        ∀e s.
          POW (e INSERT s) = (let ps = POW s in IMAGE ($INSERT e) ps ∪ ps)
   
   [POW_INSERT]  Theorem
      
      ⊢ ∀e s. POW (e INSERT s) = IMAGE ($INSERT e) (POW s) ∪ POW s
   
   [POW_applied]  Theorem
      
      ⊢ ∀set e. POW set e ⇔ e ⊆ set
   
   [PREIMAGE_ALT]  Theorem
      
      ⊢ ∀f s. PREIMAGE f s = s ∘ f
   
   [PREIMAGE_BIGUNION]  Theorem
      
      ⊢ ∀f s. PREIMAGE f (BIGUNION s) = BIGUNION (IMAGE (PREIMAGE f) s)
   
   [PREIMAGE_COMP]  Theorem
      
      ⊢ ∀f g s. PREIMAGE f (PREIMAGE g s) = PREIMAGE (g ∘ f) s
   
   [PREIMAGE_COMPL]  Theorem
      
      ⊢ ∀f s. PREIMAGE f (COMPL s) = COMPL (PREIMAGE f s)
   
   [PREIMAGE_COMPL_INTER]  Theorem
      
      ⊢ ∀f t sp. PREIMAGE f (COMPL t) ∩ sp = sp DIFF PREIMAGE f t
   
   [PREIMAGE_CROSS]  Theorem
      
      ⊢ ∀f a b.
          PREIMAGE f (a × b) = PREIMAGE (FST ∘ f) a ∩ PREIMAGE (SND ∘ f) b
   
   [PREIMAGE_DIFF]  Theorem
      
      ⊢ ∀f s t. PREIMAGE f (s DIFF t) = PREIMAGE f s DIFF PREIMAGE f t
   
   [PREIMAGE_DISJOINT]  Theorem
      
      ⊢ ∀f s t. DISJOINT s t ⇒ DISJOINT (PREIMAGE f s) (PREIMAGE f t)
   
   [PREIMAGE_EMPTY]  Theorem
      
      ⊢ ∀f. PREIMAGE f ∅ = ∅
   
   [PREIMAGE_I]  Theorem
      
      ⊢ PREIMAGE I = I
   
   [PREIMAGE_IMAGE]  Theorem
      
      ⊢ ∀f s. s ⊆ PREIMAGE f (IMAGE f s)
   
   [PREIMAGE_INTER]  Theorem
      
      ⊢ ∀f s t. PREIMAGE f (s ∩ t) = PREIMAGE f s ∩ PREIMAGE f t
   
   [PREIMAGE_K]  Theorem
      
      ⊢ ∀x s. PREIMAGE (K x) s = if x ∈ s then 𝕌(:β) else ∅
   
   [PREIMAGE_SUBSET]  Theorem
      
      ⊢ ∀f s t. s ⊆ t ⇒ PREIMAGE f s ⊆ PREIMAGE f t
   
   [PREIMAGE_UNION]  Theorem
      
      ⊢ ∀f s t. PREIMAGE f (s ∪ t) = PREIMAGE f s ∪ PREIMAGE f t
   
   [PREIMAGE_UNIV]  Theorem
      
      ⊢ ∀f. PREIMAGE f 𝕌(:β) = 𝕌(:α)
   
   [PREIMAGE_applied]  Theorem
      
      ⊢ ∀f s x. PREIMAGE f s x ⇔ f x ∈ s
   
   [PROD_IMAGE_THM]  Theorem
      
      ⊢ ∀f. Π f ∅ = 1 ∧
            ∀e s. FINITE s ⇒ Π f (e INSERT s) = f e * Π f (s DELETE e)
   
   [PROD_SET_EMPTY]  Theorem
      
      ⊢ PROD_SET ∅ = 1
   
   [PROD_SET_IMAGE_REDUCTION]  Theorem
      
      ⊢ ∀f s x.
          FINITE (IMAGE f s) ∧ f x ∉ IMAGE f s ⇒
          PROD_SET (IMAGE f (x INSERT s)) = f x * PROD_SET (IMAGE f s)
   
   [PROD_SET_THM]  Theorem
      
      ⊢ PROD_SET ∅ = 1 ∧
        ∀x s. FINITE s ⇒ PROD_SET (x INSERT s) = x * PROD_SET (s DELETE x)
   
   [PSUBSET_EQN]  Theorem
      
      ⊢ ∀s1 s2. s1 ⊂ s2 ⇔ s1 ⊆ s2 ∧ ¬(s2 ⊆ s1)
   
   [PSUBSET_FINITE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. t ⊂ s ⇒ FINITE t
   
   [PSUBSET_INSERT_SUBSET]  Theorem
      
      ⊢ ∀s t. s ⊂ t ⇔ ∃x. x ∉ s ∧ x INSERT s ⊆ t
   
   [PSUBSET_IRREFL]  Theorem
      
      ⊢ ∀s. ¬(s ⊂ s)
   
   [PSUBSET_MEMBER]  Theorem
      
      ⊢ ∀s t. s ⊂ t ⇔ s ⊆ t ∧ ∃y. y ∈ t ∧ y ∉ s
   
   [PSUBSET_SING]  Theorem
      
      ⊢ ∀s x. x ⊂ {s} ⇔ x = ∅
   
   [PSUBSET_SUBSET_TRANS]  Theorem
      
      ⊢ ∀s t u. s ⊂ t ∧ t ⊆ u ⇒ s ⊂ u
   
   [PSUBSET_TRANS]  Theorem
      
      ⊢ ∀s t u. s ⊂ t ∧ t ⊂ u ⇒ s ⊂ u
   
   [PSUBSET_UNIV]  Theorem
      
      ⊢ ∀s. s ⊂ 𝕌(:α) ⇔ ∃x. x ∉ s
   
   [RC_PSUBSET]  Theorem
      
      ⊢ RC $PSUBSET = $SUBSET
   
   [RC_SUBSET_THM]  Theorem
      
      ⊢ RC $SUBSET = $SUBSET
   
   [REL_RESTRICT_EMPTY]  Theorem
      
      ⊢ REL_RESTRICT R ∅ = ∅ᵣ
   
   [REL_RESTRICT_SUBSET]  Theorem
      
      ⊢ s1 ⊆ s2 ⇒ REL_RESTRICT R s1 ⊆ᵣ REL_RESTRICT R s2
   
   [REST_PSUBSET]  Theorem
      
      ⊢ ∀s. s ≠ ∅ ⇒ REST s ⊂ s
   
   [REST_SING]  Theorem
      
      ⊢ ∀x. REST {x} = ∅
   
   [REST_SUBSET]  Theorem
      
      ⊢ ∀s. REST s ⊆ s
   
   [REST_applied]  Theorem
      
      ⊢ ∀x s. REST s x ⇔ x ∈ s ∧ x ≠ CHOICE s
   
   [RINV_DEF]  Theorem
      
      ⊢ ∀f s t. SURJ f s t ⇒ ∀x. x ∈ t ⇒ f (RINV f s x) = x
   
   [RTC_PSUBSET]  Theorem
      
      ⊢ $PSUBSET꙳ = $SUBSET
   
   [RTC_SUBSET_THM]  Theorem
      
      ⊢ $SUBSET꙳ = $SUBSET
   
   [SCHROEDER_BERNSTEIN]  Theorem
      
      ⊢ ∀s t. (∃f. INJ f s t) ∧ (∃g. INJ g t s) ⇒ ∃h. BIJ h s t
   
   [SCHROEDER_BERNSTEIN_AUTO]  Theorem
      
      ⊢ ∀s t. t ⊆ s ∧ (∃f. INJ f s t) ⇒ ∃g. BIJ g s t
   
   [SCHROEDER_CLOSE]  Theorem
      
      ⊢ ∀f s. x ∈ schroeder_close f s ⇔ ∃n. x ∈ FUNPOW (IMAGE f) n s
   
   [SCHROEDER_CLOSED]  Theorem
      
      ⊢ ∀f s. IMAGE f (schroeder_close f s) ⊆ schroeder_close f s
   
   [SCHROEDER_CLOSE_SET]  Theorem
      
      ⊢ ∀f s t. f ∈ FUNSET s s ∧ t ⊆ s ⇒ schroeder_close f t ⊆ s
   
   [SCHROEDER_CLOSE_SUBSET]  Theorem
      
      ⊢ ∀f s. s ⊆ schroeder_close f s
   
   [SET_CASES]  Theorem
      
      ⊢ ∀s. s = ∅ ∨ ∃x t. s = x INSERT t ∧ x ∉ t
   
   [SET_EQ_SUBSET]  Theorem
      
      ⊢ ∀s t. s = t ⇔ s ⊆ t ∧ t ⊆ s
   
   [SET_MINIMUM]  Theorem
      
      ⊢ ∀s M. (∃x. x ∈ s) ⇔ ∃x. x ∈ s ∧ ∀y. y ∈ s ⇒ M x ≤ M y
   
   [SING]  Theorem
      
      ⊢ ∀x. SING {x}
   
   [SING_DELETE]  Theorem
      
      ⊢ ∀x. {x} DELETE x = ∅
   
   [SING_EMPTY]  Theorem
      
      ⊢ SING ∅ ⇔ F
   
   [SING_FINITE]  Theorem
      
      ⊢ ∀s. SING s ⇒ FINITE s
   
   [SING_IFF_CARD1]  Theorem
      
      ⊢ ∀s. SING s ⇔ CARD s = 1 ∧ FINITE s
   
   [SING_IFF_EMPTY_REST]  Theorem
      
      ⊢ ∀s. SING s ⇔ s ≠ ∅ ∧ REST s = ∅
   
   [SING_INSERT]  Theorem
      
      ⊢ SING (x INSERT s) ⇔ s = ∅ ∨ s = {x}
   
   [SING_UNION]  Theorem
      
      ⊢ SING (s ∪ t) ⇔
        SING s ∧ t = ∅ ∨ SING t ∧ s = ∅ ∨ SING s ∧ SING t ∧ s = t
   
   [SING_applied]  Theorem
      
      ⊢ ∀x y. {y} x ⇔ x = y
   
   [SPECIFICATION]  Theorem
      
      ⊢ ∀P x. x ∈ P ⇔ P x
   
   [SUBSET_ADD]  Theorem
      
      ⊢ ∀f n d. (∀n. f n ⊆ f (SUC n)) ⇒ f n ⊆ f (n + d)
   
   [SUBSET_ANTISYM]  Theorem
      
      ⊢ ∀s t. s ⊆ t ∧ t ⊆ s ⇒ s = t
   
   [SUBSET_ANTISYM_EQ]  Theorem
      
      ⊢ ∀s t. s ⊆ t ∧ t ⊆ s ⇔ s = t
   
   [SUBSET_BIGINTER]  Theorem
      
      ⊢ ∀X P. X ⊆ BIGINTER P ⇔ ∀Y. Y ∈ P ⇒ X ⊆ Y
   
   [SUBSET_BIGUNION]  Theorem
      
      ⊢ ∀f g. f ⊆ g ⇒ BIGUNION f ⊆ BIGUNION g
   
   [SUBSET_BIGUNION_I]  Theorem
      
      ⊢ ∀x P. x ∈ P ⇒ x ⊆ BIGUNION P
   
   [SUBSET_CROSS]  Theorem
      
      ⊢ ∀a b c d. a ⊆ b ∧ c ⊆ d ⇒ a × c ⊆ b × d
   
   [SUBSET_DELETE]  Theorem
      
      ⊢ ∀x s t. s ⊆ t DELETE x ⇔ x ∉ s ∧ s ⊆ t
   
   [SUBSET_DELETE_BOTH]  Theorem
      
      ⊢ ∀s1 s2 x. s1 ⊆ s2 ⇒ s1 DELETE x ⊆ s2 DELETE x
   
   [SUBSET_DIFF]  Theorem
      
      ⊢ ∀s1 s2 s3. s1 ⊆ s2 DIFF s3 ⇔ s1 ⊆ s2 ∧ DISJOINT s1 s3
   
   [SUBSET_DIFF_EMPTY]  Theorem
      
      ⊢ ∀s t. s DIFF t = ∅ ⇔ s ⊆ t
   
   [SUBSET_DISJOINT]  Theorem
      
      ⊢ ∀s t u v. DISJOINT s t ∧ u ⊆ s ∧ v ⊆ t ⇒ DISJOINT u v
   
   [SUBSET_EMPTY]  Theorem
      
      ⊢ ∀s. s ⊆ ∅ ⇔ s = ∅
   
   [SUBSET_EQ_CARD]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. FINITE t ∧ CARD s = CARD t ∧ s ⊆ t ⇒ s = t
   
   [SUBSET_FINITE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. t ⊆ s ⇒ FINITE t
   
   [SUBSET_FINITE_I]  Theorem
      
      ⊢ ∀s t. FINITE s ∧ t ⊆ s ⇒ FINITE t
   
   [SUBSET_IMAGE]  Theorem
      
      ⊢ ∀f s t. s ⊆ IMAGE f t ⇔ ∃u. u ⊆ t ∧ s = IMAGE f u
   
   [SUBSET_INSERT]  Theorem
      
      ⊢ ∀x s. x ∉ s ⇒ ∀t. s ⊆ x INSERT t ⇔ s ⊆ t
   
   [SUBSET_INSERT_DELETE]  Theorem
      
      ⊢ ∀x s t. s ⊆ x INSERT t ⇔ s DELETE x ⊆ t
   
   [SUBSET_INSERT_RIGHT]  Theorem
      
      ⊢ ∀e s1 s2. s1 ⊆ s2 ⇒ s1 ⊆ e INSERT s2
   
   [SUBSET_INTER]  Theorem
      
      ⊢ ∀s t u. s ⊆ t ∩ u ⇔ s ⊆ t ∧ s ⊆ u
   
   [SUBSET_INTER1]  Theorem
      
      ⊢ ∀s t. s ⊆ t ⇒ s ∩ t = s
   
   [SUBSET_INTER2]  Theorem
      
      ⊢ ∀s t. s ⊆ t ⇒ t ∩ s = s
   
   [SUBSET_INTER_ABSORPTION]  Theorem
      
      ⊢ ∀s t. s ⊆ t ⇔ s ∩ t = s
   
   [SUBSET_K]  Theorem
      
      ⊢ ∀x y. x ⊆ K y ⇔ x ⊆ ∅ ∨ y
   
   [SUBSET_MAX_SET]  Theorem
      
      ⊢ ∀I J. FINITE I ∧ FINITE J ∧ I ⊆ J ⇒ MAX_SET I ≤ MAX_SET J
   
   [SUBSET_MIN_SET]  Theorem
      
      ⊢ ∀I J n. I ≠ ∅ ∧ J ≠ ∅ ∧ I ⊆ J ⇒ MIN_SET J ≤ MIN_SET I
   
   [SUBSET_OF_INSERT]  Theorem
      
      ⊢ ∀x s. s ⊆ x INSERT s
   
   [SUBSET_POW]  Theorem
      
      ⊢ ∀s1 s2. s1 ⊆ s2 ⇒ POW s1 ⊆ POW s2
   
   [SUBSET_PSUBSET_TRANS]  Theorem
      
      ⊢ ∀s t u. s ⊆ t ∧ t ⊂ u ⇒ s ⊂ u
   
   [SUBSET_REFL]  Theorem
      
      ⊢ ∀s. s ⊆ s
   
   [SUBSET_THM]  Theorem
      
      ⊢ ∀P Q. P ⊆ Q ⇒ ∀x. x ∈ P ⇒ x ∈ Q
   
   [SUBSET_TRANS]  Theorem
      
      ⊢ ∀s t u. s ⊆ t ∧ t ⊆ u ⇒ s ⊆ u
   
   [SUBSET_UNION]  Theorem
      
      ⊢ (∀s t. s ⊆ s ∪ t) ∧ ∀s t. s ⊆ t ∪ s
   
   [SUBSET_UNION_ABSORPTION]  Theorem
      
      ⊢ ∀s t. s ⊆ t ⇔ s ∪ t = t
   
   [SUBSET_UNIV]  Theorem
      
      ⊢ ∀s. s ⊆ 𝕌(:α)
   
   [SUBSET_applied]  Theorem
      
      ⊢ ∀s t. s ⊆ t ⇔ ∀x. s x ⇒ t x
   
   [SUBSET_count_MAX_SET]  Theorem
      
      ⊢ FINITE s ⇒ s ⊆ count (MAX_SET s + 1)
   
   [SUBSET_reflexive]  Theorem
      
      ⊢ reflexive $SUBSET
   
   [SUBSET_transitive]  Theorem
      
      ⊢ transitive $SUBSET
   
   [SUM_IMAGE_CONG]  Theorem
      
      ⊢ s1 = s2 ∧ (∀x. x ∈ s2 ⇒ f1 x = f2 x) ⇒ ∑ f1 s1 = ∑ f2 s2
   
   [SUM_IMAGE_DELETE]  Theorem
      
      ⊢ ∀f s.
          FINITE s ⇒
          ∀e. ∑ f (s DELETE e) = if e ∈ s then ∑ f s − f e else ∑ f s
   
   [SUM_IMAGE_INJ_o]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∀g. INJ g s 𝕌(:α) ⇒ ∀f. ∑ f (IMAGE g s) = ∑ (f ∘ g) s
   
   [SUM_IMAGE_IN_LE]  Theorem
      
      ⊢ ∀f s e. FINITE s ∧ e ∈ s ⇒ f e ≤ ∑ f s
   
   [SUM_IMAGE_MONO_LESS]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            (∃x. x ∈ s ∧ f x < g x) ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
            ∑ f s < ∑ g s
   
   [SUM_IMAGE_MONO_LESS_EQ]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ ∑ f s ≤ ∑ g s
   
   [SUM_IMAGE_PERMUTES]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀g. g PERMUTES s ⇒ ∀f. ∑ (f ∘ g) s = ∑ f s
   
   [SUM_IMAGE_SING]  Theorem
      
      ⊢ ∀f e. ∑ f {e} = f e
   
   [SUM_IMAGE_SUBSET_LE]  Theorem
      
      ⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ ∑ f t ≤ ∑ f s
   
   [SUM_IMAGE_THM]  Theorem
      
      ⊢ ∀f. ∑ f ∅ = 0 ∧
            ∀e s. FINITE s ⇒ ∑ f (e INSERT s) = f e + ∑ f (s DELETE e)
   
   [SUM_IMAGE_UNION]  Theorem
      
      ⊢ ∀f s t.
          FINITE s ∧ FINITE t ⇒ ∑ f (s ∪ t) = ∑ f s + ∑ f t − ∑ f (s ∩ t)
   
   [SUM_IMAGE_ZERO]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ (∑ f s = 0 ⇔ ∀x. x ∈ s ⇒ f x = 0)
   
   [SUM_IMAGE_lower_bound]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ n ≤ f x) ⇒ CARD s * n ≤ ∑ f s
   
   [SUM_IMAGE_upper_bound]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀n. (∀x. x ∈ s ⇒ f x ≤ n) ⇒ ∑ f s ≤ CARD s * n
   
   [SUM_SAME_IMAGE]  Theorem
      
      ⊢ ∀P. FINITE P ⇒
            ∀f p. p ∈ P ∧ (∀q. q ∈ P ⇒ f p = f q) ⇒ ∑ f P = CARD P * f p
   
   [SUM_SET_DELETE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∀e. SUM_SET (s DELETE e) =
                if e ∈ s then SUM_SET s − e else SUM_SET s
   
   [SUM_SET_EMPTY]  Theorem
      
      ⊢ SUM_SET ∅ = 0
   
   [SUM_SET_IN_LE]  Theorem
      
      ⊢ ∀x s. FINITE s ∧ x ∈ s ⇒ x ≤ SUM_SET s
   
   [SUM_SET_SING]  Theorem
      
      ⊢ ∀n. SUM_SET {n} = n
   
   [SUM_SET_SUBSET_LE]  Theorem
      
      ⊢ ∀s t. FINITE t ∧ s ⊆ t ⇒ SUM_SET s ≤ SUM_SET t
   
   [SUM_SET_THM]  Theorem
      
      ⊢ SUM_SET ∅ = 0 ∧
        ∀x s. FINITE s ⇒ SUM_SET (x INSERT s) = x + SUM_SET (s DELETE x)
   
   [SUM_SET_UNION]  Theorem
      
      ⊢ ∀s t.
          FINITE s ∧ FINITE t ⇒
          SUM_SET (s ∪ t) = SUM_SET s + SUM_SET t − SUM_SET (s ∩ t)
   
   [SUM_SET_count]  Theorem
      
      ⊢ SUM_SET (count n) = n * (n − 1) DIV 2
   
   [SUM_SET_count_2]  Theorem
      
      ⊢ ∀n. 2 * SUM_SET (count n) = n * (n − 1)
   
   [SUM_UNIV]  Theorem
      
      ⊢ 𝕌(:α + β) = IMAGE INL 𝕌(:α) ∪ IMAGE INR 𝕌(:β)
   
   [SURJ_CARD]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀t. SURJ f s t ⇒ FINITE t ∧ CARD t ≤ CARD s
   
   [SURJ_COMPOSE]  Theorem
      
      ⊢ ∀f g s t u. SURJ f s t ∧ SURJ g t u ⇒ SURJ (g ∘ f) s u
   
   [SURJ_EMPTY]  Theorem
      
      ⊢ ∀f. (∀s. SURJ f ∅ s ⇔ s = ∅) ∧ ∀s. SURJ f s ∅ ⇔ s = ∅
   
   [SURJ_ID]  Theorem
      
      ⊢ ∀s. SURJ (λx. x) s s
   
   [SURJ_IMAGE]  Theorem
      
      ⊢ SURJ f s (IMAGE f s)
   
   [SURJ_IMP_INJ]  Theorem
      
      ⊢ ∀s t. (∃f. SURJ f s t) ⇒ ∃g. INJ g t s
   
   [SURJ_INJ_INV]  Theorem
      
      ⊢ SURJ f s t ⇒ ∃g. INJ g t s ∧ ∀y. y ∈ t ⇒ f (g y) = y
   
   [TC_PSUBSET]  Theorem
      
      ⊢ $PSUBSET⁺ = $PSUBSET
   
   [TC_SUBSET_THM]  Theorem
      
      ⊢ $SUBSET⁺ = $SUBSET
   
   [UNION_ASSOC]  Theorem
      
      ⊢ ∀s t u. s ∪ (t ∪ u) = s ∪ t ∪ u
   
   [UNION_COMM]  Theorem
      
      ⊢ ∀s t. s ∪ t = t ∪ s
   
   [UNION_DELETE]  Theorem
      
      ⊢ ∀A B x. A ∪ B DELETE x = A DELETE x ∪ (B DELETE x)
   
   [UNION_DIFF]  Theorem
      
      ⊢ s ⊆ t ⇒ s ∪ (t DIFF s) = t ∧ t DIFF s ∪ s = t
   
   [UNION_DIFF_2]  Theorem
      
      ⊢ ∀s t. s ∪ (s DIFF t) = s
   
   [UNION_DIFF_EQ]  Theorem
      
      ⊢ (∀s t. s ∪ (t DIFF s) = s ∪ t) ∧ ∀s t. t DIFF s ∪ s = t ∪ s
   
   [UNION_EMPTY]  Theorem
      
      ⊢ (∀s. ∅ ∪ s = s) ∧ ∀s. s ∪ ∅ = s
   
   [UNION_IDEMPOT]  Theorem
      
      ⊢ ∀s. s ∪ s = s
   
   [UNION_OVER_INTER]  Theorem
      
      ⊢ ∀s t u. s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u
   
   [UNION_SUBSET]  Theorem
      
      ⊢ ∀s t u. s ∪ t ⊆ u ⇔ s ⊆ u ∧ t ⊆ u
   
   [UNION_UNIV]  Theorem
      
      ⊢ (∀s. 𝕌(:α) ∪ s = 𝕌(:α)) ∧ ∀s. s ∪ 𝕌(:α) = 𝕌(:α)
   
   [UNION_applied]  Theorem
      
      ⊢ ∀s t x. (s ∪ t) x ⇔ x ∈ s ∨ x ∈ t
   
   [UNIQUE_MEMBER_SING]  Theorem
      
      ⊢ ∀x s. x ∈ s ∧ (∀y. y ∈ s ⇒ x = y) ⇔ s = {x}
   
   [UNIV_BOOL]  Theorem
      
      ⊢ 𝕌(:bool) = {T; F}
   
   [UNIV_FUNSET_UNIV]  Theorem
      
      ⊢ FUNSET 𝕌(:α) 𝕌(:β) = 𝕌(:α -> β)
   
   [UNIV_FUN_TO_BOOL]  Theorem
      
      ⊢ 𝕌(:α -> bool) = POW 𝕌(:α)
   
   [UNIV_NOT_EMPTY]  Theorem
      
      ⊢ 𝕌(:α) ≠ ∅
   
   [UNIV_SUBSET]  Theorem
      
      ⊢ ∀s. 𝕌(:α) ⊆ s ⇔ s = 𝕌(:α)
   
   [UNIV_applied]  Theorem
      
      ⊢ ∀x. 𝕌(:α) x
   
   [X_LE_MAX_SET]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x ≤ MAX_SET s
   
   [bigunion_countable]  Theorem
      
      ⊢ ∀s. countable s ∧ (∀x. x ∈ s ⇒ countable x) ⇒
            countable (BIGUNION s)
   
   [chooser_compute]  Theorem
      
      ⊢ (∀s. chooser s 0 = CHOICE s) ∧
        (∀s n.
           chooser s (NUMERAL (BIT1 n)) =
           chooser (REST s) (NUMERAL (BIT1 n) − 1)) ∧
        ∀s n.
          chooser s (NUMERAL (BIT2 n)) =
          chooser (REST s) (NUMERAL (BIT1 n))
   
   [compl_insert]  Theorem
      
      ⊢ ∀s x. COMPL (x INSERT s) = COMPL s DELETE x
   
   [count_EQN]  Theorem
      
      ⊢ ∀n. count n =
            if n = 0 then ∅ else (let p = PRE n in p INSERT count p)
   
   [count_add]  Theorem
      
      ⊢ ∀n m. count (n + m) = count n ∪ IMAGE ($+ n) (count m)
   
   [count_add1]  Theorem
      
      ⊢ ∀n. count (n + 1) = n INSERT count n
   
   [countable_EMPTY]  Theorem
      
      ⊢ countable ∅
   
   [countable_INSERT]  Theorem
      
      ⊢ countable (x INSERT s) ⇔ countable s
   
   [countable_Uprod]  Theorem
      
      ⊢ countable 𝕌(:α # β) ⇔ countable 𝕌(:α) ∧ countable 𝕌(:β)
   
   [countable_Usum]  Theorem
      
      ⊢ countable 𝕌(:α + β) ⇔ countable 𝕌(:α) ∧ countable 𝕌(:β)
   
   [countable_image_nats]  Theorem
      
      ⊢ countable (IMAGE f 𝕌(:num))
   
   [countable_surj]  Theorem
      
      ⊢ ∀s. countable s ⇔ s = ∅ ∨ ∃f. SURJ f 𝕌(:num) s
   
   [cross_countable]  Theorem
      
      ⊢ ∀s t. countable s ∧ countable t ⇒ countable (s × t)
   
   [cross_countable_IFF]  Theorem
      
      ⊢ countable (s × t) ⇔ s = ∅ ∨ t = ∅ ∨ countable s ∧ countable t
   
   [disjUNION_UNIV]  Theorem
      
      ⊢ 𝕌(:α + β) = 𝕌(:α) ⊔ 𝕌(:β)
   
   [finite_countable]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ countable s
   
   [image_countable]  Theorem
      
      ⊢ ∀f s. countable s ⇒ countable (IMAGE f s)
   
   [in_max_set]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x ≤ MAX_SET s
   
   [infinite_num_inj]  Theorem
      
      ⊢ ∀s. INFINITE s ⇔ ∃f. INJ f 𝕌(:num) s
   
   [infinite_pow_uncountable]  Theorem
      
      ⊢ ∀s. INFINITE s ⇒ ¬countable (POW s)
   
   [infinite_rest]  Theorem
      
      ⊢ ∀s. INFINITE s ⇒ INFINITE (REST s)
   
   [inj_countable]  Theorem
      
      ⊢ ∀f s t. countable t ∧ INJ f s t ⇒ countable s
   
   [inj_image_countable_IFF]  Theorem
      
      ⊢ INJ f s (IMAGE f s) ⇒ (countable (IMAGE f s) ⇔ countable s)
   
   [inj_surj]  Theorem
      
      ⊢ ∀f s t. INJ f s t ⇒ s = ∅ ∨ ∃f'. SURJ f' t s
   
   [inter_countable]  Theorem
      
      ⊢ ∀s t. countable s ∨ countable t ⇒ countable (s ∩ t)
   
   [is_measure_maximal_INSERT]  Theorem
      
      ⊢ ∀x s m e y.
          x ∈ s ∧ m e < m x ⇒
          (is_measure_maximal m (e INSERT s) y ⇔ is_measure_maximal m s y)
   
   [is_measure_maximal_SING]  Theorem
      
      ⊢ is_measure_maximal m {x} y ⇔ y = x
   
   [num_countable]  Theorem
      
      ⊢ countable 𝕌(:num)
   
   [pair_to_num_formula]  Theorem
      
      ⊢ ∀x y. pair_to_num (x,y) = (x + y + 1) * (x + y) DIV 2 + y
   
   [pair_to_num_inv]  Theorem
      
      ⊢ (∀x. pair_to_num (num_to_pair x) = x) ∧
        ∀x y. num_to_pair (pair_to_num (x,y)) = (x,y)
   
   [pairwise_SUBSET]  Theorem
      
      ⊢ ∀R s t. pairwise R t ∧ s ⊆ t ⇒ pairwise R s
   
   [pairwise_UNION]  Theorem
      
      ⊢ pairwise R (s1 ∪ s2) ⇔
        pairwise R s1 ∧ pairwise R s2 ∧
        ∀x y. x ∈ s1 ∧ y ∈ s2 ⇒ R x y ∧ R y x
   
   [partition_CARD]  Theorem
      
      ⊢ ∀R s. R equiv_on s ∧ FINITE s ⇒ CARD s = ∑ CARD (partition R s)
   
   [partition_SUBSET]  Theorem
      
      ⊢ ∀R s t. t ∈ partition R s ⇒ t ⊆ s
   
   [partition_elements_disjoint]  Theorem
      
      ⊢ R equiv_on s ⇒
        ∀t1 t2.
          t1 ∈ partition R s ∧ t2 ∈ partition R s ∧ t1 ≠ t2 ⇒
          DISJOINT t1 t2
   
   [partition_elements_interrelate]  Theorem
      
      ⊢ R equiv_on s ⇒ ∀t. t ∈ partition R s ⇒ ∀x y. x ∈ t ∧ y ∈ t ⇒ R x y
   
   [pow_no_surj]  Theorem
      
      ⊢ ∀s. ¬∃f. SURJ f s (POW s)
   
   [subset_countable]  Theorem
      
      ⊢ ∀s t. countable s ∧ t ⊆ s ⇒ countable t
   
   [transitive_PSUBSET]  Theorem
      
      ⊢ transitive $PSUBSET
   
   [union_countable]  Theorem
      
      ⊢ ∀s t. countable s ∧ countable t ⇒ countable (s ∪ t)
   
   [union_countable_IFF]  Theorem
      
      ⊢ countable (s ∪ t) ⇔ countable s ∧ countable t
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14