Structure iterateTheory
signature iterateTheory =
sig
type thm = Thm.thm
(* Definitions *)
val FINREC_def : thm
val from_def : thm
val indicator : thm
val iterate : thm
val monoidal : thm
val neutral : thm
val nproduct : thm
val nsum : thm
val numseg : thm
val polynomial_function : thm
val product : thm
val sum_def : thm
val support : thm
(* Theorems *)
val ABS_LE_0 : thm
val ABS_LE_HALF_POW2 : thm
val ADD_SUB2 : thm
val ADD_SUBR : thm
val ADD_SUBR2 : thm
val BIGINTER_BIGUNION : thm
val BIGINTER_GSPEC : thm
val BIGUNION_BIGINTER : thm
val BIGUNION_GSPEC : thm
val BOUNDS_LINEAR : thm
val BOUNDS_LINEAR_0 : thm
val CARD_BIGUNION : thm
val CARD_EQ_NSUM : thm
val CARD_EQ_SUM : thm
val CARD_NUMSEG : thm
val CARD_NUMSEG_1 : thm
val CARD_NUMSEG_LEMMA : thm
val CARD_UNION_EQ : thm
val CHOOSE_SUBSET : thm
val CHOOSE_SUBSET_STRONG : thm
val COUNTABLE_FROM : thm
val COUNT_NUMSEG : thm
val DIFF_BIGINTER2 : thm
val DISJOINT_COUNT_FROM : thm
val DISJOINT_FROM_COUNT : thm
val DISJOINT_NUMSEG : thm
val DROP_INDICATOR : thm
val DROP_INDICATOR_ABS_LE_1 : thm
val DROP_INDICATOR_LE_1 : thm
val DROP_INDICATOR_POS_LE : thm
val EMPTY_BIGUNION : thm
val EXISTS_FINITE_SUBSET_IMAGE : thm
val FINITE_INDEX_NUMBERS : thm
val FINITE_INDEX_NUMSEG : thm
val FINITE_NUMSEG : thm
val FINITE_POWERSET : thm
val FINITE_REAL_INTERVAL : thm
val FINITE_RECURSION : thm
val FINITE_RESTRICT : thm
val FINITE_SUBSET_IMAGE : thm
val FINITE_SUPPORT : thm
val FINITE_SUPPORT_DELTA : thm
val FINREC_1_LEMMA : thm
val FINREC_EXISTS_LEMMA : thm
val FINREC_FUN : thm
val FINREC_FUN_LEMMA : thm
val FINREC_SUC_LEMMA : thm
val FINREC_UNIQUE_LEMMA : thm
val FINREC_compute : thm
val FORALL_FINITE_SUBSET_IMAGE : thm
val FROM_0 : thm
val FROM_INTER_NUMSEG : thm
val FROM_INTER_NUMSEG_GEN : thm
val FROM_INTER_NUMSEG_MAX : thm
val FROM_NOT_EMPTY : thm
val FUN_IN_IMAGE : thm
val HAS_SIZE_NUMSEG : thm
val HAS_SIZE_NUMSEG_1 : thm
val INDICATOR_COMPLEMENT : thm
val INDICATOR_EMPTY : thm
val INF : thm
val INFINITE_FROM : thm
val INF_CLOSE : thm
val INF_DEF_ALT : thm
val INF_EQ : thm
val INF_FINITE : thm
val INF_FINITE_LEMMA : thm
val INF_GREATER : thm
val INF_INSERT_FINITE : thm
val INF_LE : thm
val INF_SING : thm
val INF_UNIQUE_FINITE : thm
val IN_FROM : thm
val IN_NUMSEG : thm
val IN_NUMSEG_0 : thm
val IN_SUPPORT : thm
val ITERATE_AND : thm
val ITERATE_BIJECTION : thm
val ITERATE_CASES : thm
val ITERATE_CLAUSES : thm
val ITERATE_CLAUSES_GEN : thm
val ITERATE_CLAUSES_NUMSEG : thm
val ITERATE_CLOSED : thm
val ITERATE_DELETE : thm
val ITERATE_DELTA : thm
val ITERATE_DIFF : thm
val ITERATE_DIFF_GEN : thm
val ITERATE_EQ : thm
val ITERATE_EQ_GENERAL : thm
val ITERATE_EQ_GENERAL_INVERSES : thm
val ITERATE_EQ_NEUTRAL : thm
val ITERATE_EXPAND_CASES : thm
val ITERATE_IMAGE : thm
val ITERATE_IMAGE_NONZERO : thm
val ITERATE_INCL_EXCL : thm
val ITERATE_INJECTION : thm
val ITERATE_ITERATE_PRODUCT : thm
val ITERATE_NONZERO_IMAGE_LEMMA : thm
val ITERATE_OP : thm
val ITERATE_OP_GEN : thm
val ITERATE_PAIR : thm
val ITERATE_PERMUTE : thm
val ITERATE_PERMUTES : thm
val ITERATE_RELATED : thm
val ITERATE_SING : thm
val ITERATE_SOME : thm
val ITERATE_SUPERSET : thm
val ITERATE_SUPPORT : thm
val ITERATE_UNION : thm
val ITERATE_UNION_GEN : thm
val ITERATE_UNION_NONZERO : thm
val ITSET_alt : thm
val LAMBDA_PAIR : thm
val LE_ADD : thm
val LE_ADDR : thm
val LE_EXISTS : thm
val LE_INF : thm
val LOWER_BOUND_FINITE_SET_REAL : thm
val LT_EXISTS : thm
val MOD_NSUM_MOD : thm
val MOD_NSUM_MOD_NUMSEG : thm
val MONOIDAL_AC : thm
val MONOIDAL_ADD : thm
val MONOIDAL_AND : thm
val MONOIDAL_LIFTED : thm
val MONOIDAL_MUL : thm
val MONOIDAL_REAL_ADD : thm
val MONOIDAL_REAL_MUL : thm
val NEUTRAL_ADD : thm
val NEUTRAL_AND : thm
val NEUTRAL_LIFTED : thm
val NEUTRAL_MUL : thm
val NEUTRAL_REAL_ADD : thm
val NEUTRAL_REAL_MUL : thm
val NOT_EQ : thm
val NPRODUCT_ADD_SPLIT : thm
val NPRODUCT_CLAUSES : thm
val NPRODUCT_CLAUSES_LEFT : thm
val NPRODUCT_CLAUSES_NUMSEG : thm
val NPRODUCT_CLAUSES_RIGHT : thm
val NPRODUCT_CLOSED : thm
val NPRODUCT_CONG : thm
val NPRODUCT_CONST : thm
val NPRODUCT_CONST_NUMSEG : thm
val NPRODUCT_CONST_NUMSEG_1 : thm
val NPRODUCT_DELETE : thm
val NPRODUCT_DELTA : thm
val NPRODUCT_EQ : thm
val NPRODUCT_EQ_0 : thm
val NPRODUCT_EQ_0_NUMSEG : thm
val NPRODUCT_EQ_1 : thm
val NPRODUCT_EQ_1_NUMSEG : thm
val NPRODUCT_EQ_NUMSEG : thm
val NPRODUCT_FACT : thm
val NPRODUCT_IMAGE : thm
val NPRODUCT_LE : thm
val NPRODUCT_LE_NUMSEG : thm
val NPRODUCT_MUL : thm
val NPRODUCT_MUL_GEN : thm
val NPRODUCT_MUL_NUMSEG : thm
val NPRODUCT_OFFSET : thm
val NPRODUCT_ONE : thm
val NPRODUCT_PAIR : thm
val NPRODUCT_POS_LT : thm
val NPRODUCT_POS_LT_NUMSEG : thm
val NPRODUCT_SING : thm
val NPRODUCT_SING_NUMSEG : thm
val NPRODUCT_SUPERSET : thm
val NPRODUCT_SUPPORT : thm
val NPRODUCT_UNION : thm
val NSUM_0 : thm
val NSUM_ADD : thm
val NSUM_ADD_GEN : thm
val NSUM_ADD_NUMSEG : thm
val NSUM_ADD_SPLIT : thm
val NSUM_BIGUNION_NONZERO : thm
val NSUM_BIJECTION : thm
val NSUM_BOUND : thm
val NSUM_BOUND_GEN : thm
val NSUM_BOUND_LT : thm
val NSUM_BOUND_LT_ALL : thm
val NSUM_BOUND_LT_GEN : thm
val NSUM_CASES : thm
val NSUM_CLAUSES : thm
val NSUM_CLAUSES_LEFT : thm
val NSUM_CLAUSES_NUMSEG : thm
val NSUM_CLAUSES_RIGHT : thm
val NSUM_CLOSED : thm
val NSUM_CONG : thm
val NSUM_CONST : thm
val NSUM_CONST_NUMSEG : thm
val NSUM_DEGENERATE : thm
val NSUM_DELETE : thm
val NSUM_DELTA : thm
val NSUM_DIFF : thm
val NSUM_EQ : thm
val NSUM_EQ_0 : thm
val NSUM_EQ_0_IFF : thm
val NSUM_EQ_0_IFF_NUMSEG : thm
val NSUM_EQ_0_NUMSEG : thm
val NSUM_EQ_GENERAL : thm
val NSUM_EQ_GENERAL_INVERSES : thm
val NSUM_EQ_NUMSEG : thm
val NSUM_EQ_SUPERSET : thm
val NSUM_GROUP : thm
val NSUM_IMAGE : thm
val NSUM_IMAGE_GEN : thm
val NSUM_IMAGE_NONZERO : thm
val NSUM_INCL_EXCL : thm
val NSUM_INJECTION : thm
val NSUM_LE : thm
val NSUM_LE_GEN : thm
val NSUM_LE_NUMSEG : thm
val NSUM_LMUL : thm
val NSUM_LT : thm
val NSUM_LT_ALL : thm
val NSUM_MULTICOUNT : thm
val NSUM_MULTICOUNT_GEN : thm
val NSUM_NSUM_PRODUCT : thm
val NSUM_NSUM_RESTRICT : thm
val NSUM_OFFSET : thm
val NSUM_OFFSET_0 : thm
val NSUM_PAIR : thm
val NSUM_PERMUTE : thm
val NSUM_PERMUTE_COUNT : thm
val NSUM_PERMUTE_NUMSEG : thm
val NSUM_POS_BOUND : thm
val NSUM_POS_LT : thm
val NSUM_POS_LT_ALL : thm
val NSUM_RESTRICT : thm
val NSUM_RESTRICT_SET : thm
val NSUM_RMUL : thm
val NSUM_SING : thm
val NSUM_SING_NUMSEG : thm
val NSUM_SUBSET : thm
val NSUM_SUBSET_SIMPLE : thm
val NSUM_SUPERSET : thm
val NSUM_SUPPORT : thm
val NSUM_SWAP : thm
val NSUM_SWAP_NUMSEG : thm
val NSUM_TRIV_NUMSEG : thm
val NSUM_UNION : thm
val NSUM_UNION_EQ : thm
val NSUM_UNION_LZERO : thm
val NSUM_UNION_NONZERO : thm
val NSUM_UNION_RZERO : thm
val NUMSEG_ADD_SPLIT : thm
val NUMSEG_CLAUSES : thm
val NUMSEG_COMBINE_L : thm
val NUMSEG_COMBINE_R : thm
val NUMSEG_EMPTY : thm
val NUMSEG_LE : thm
val NUMSEG_LREC : thm
val NUMSEG_LT : thm
val NUMSEG_OFFSET_IMAGE : thm
val NUMSEG_REC : thm
val NUMSEG_RREC : thm
val NUMSEG_SING : thm
val PERMUTES_IN_NUMSEG : thm
val POLYNOMIAL_FUNCTION_ADD : thm
val POLYNOMIAL_FUNCTION_CONST : thm
val POLYNOMIAL_FUNCTION_FINITE_ROOTS : thm
val POLYNOMIAL_FUNCTION_ID : thm
val POLYNOMIAL_FUNCTION_INDUCT : thm
val POLYNOMIAL_FUNCTION_LMUL : thm
val POLYNOMIAL_FUNCTION_MUL : thm
val POLYNOMIAL_FUNCTION_NEG : thm
val POLYNOMIAL_FUNCTION_POW : thm
val POLYNOMIAL_FUNCTION_RMUL : thm
val POLYNOMIAL_FUNCTION_SUB : thm
val POLYNOMIAL_FUNCTION_SUM : thm
val POLYNOMIAL_FUNCTION_o : thm
val POWERSET_CLAUSES : thm
val POW_NEG_ODD : thm
val POW_POS_EVEN : thm
val PRODUCT_ABS : thm
val PRODUCT_ADD_SPLIT : thm
val PRODUCT_CLAUSES : thm
val PRODUCT_CLAUSES_LEFT : thm
val PRODUCT_CLAUSES_NUMSEG : thm
val PRODUCT_CLAUSES_RIGHT : thm
val PRODUCT_CLOSED : thm
val PRODUCT_CONG : thm
val PRODUCT_CONST : thm
val PRODUCT_CONST_NUMSEG : thm
val PRODUCT_CONST_NUMSEG_1 : thm
val PRODUCT_DELETE : thm
val PRODUCT_DELTA : thm
val PRODUCT_DIV : thm
val PRODUCT_DIV_NUMSEG : thm
val PRODUCT_EQ : thm
val PRODUCT_EQ_0 : thm
val PRODUCT_EQ_0_COUNT : thm
val PRODUCT_EQ_0_NUMSEG : thm
val PRODUCT_EQ_1 : thm
val PRODUCT_EQ_1_COUNT : thm
val PRODUCT_EQ_1_NUMSEG : thm
val PRODUCT_EQ_COUNT : thm
val PRODUCT_EQ_NUMSEG : thm
val PRODUCT_IMAGE : thm
val PRODUCT_INV : thm
val PRODUCT_LE : thm
val PRODUCT_LE_1 : thm
val PRODUCT_LE_NUMSEG : thm
val PRODUCT_MUL : thm
val PRODUCT_MUL_COUNT : thm
val PRODUCT_MUL_GEN : thm
val PRODUCT_MUL_NUMSEG : thm
val PRODUCT_NEG : thm
val PRODUCT_NEG_NUMSEG : thm
val PRODUCT_NEG_NUMSEG_1 : thm
val PRODUCT_OFFSET : thm
val PRODUCT_ONE : thm
val PRODUCT_PAIR : thm
val PRODUCT_PERMUTE : thm
val PRODUCT_PERMUTE_COUNT : thm
val PRODUCT_PERMUTE_NUMSEG : thm
val PRODUCT_POS_LE : thm
val PRODUCT_POS_LE_NUMSEG : thm
val PRODUCT_POS_LT : thm
val PRODUCT_POS_LT_NUMSEG : thm
val PRODUCT_SING : thm
val PRODUCT_SING_NUMSEG : thm
val PRODUCT_SUPERSET : thm
val PRODUCT_SUPPORT : thm
val PRODUCT_UNION : thm
val REAL_ABS_INF_LE : thm
val REAL_ABS_SUP_LE : thm
val REAL_ARCH_INV' : thm
val REAL_ARCH_INV_SUC : thm
val REAL_BOUNDS_LT : thm
val REAL_COMPLETE : thm
val REAL_EQ_SQUARE_ABS : thm
val REAL_HALF : thm
val REAL_IMP_LE_SUP' : thm
val REAL_IMP_SUP_LE' : thm
val REAL_INF_ASCLOSE : thm
val REAL_INF_BOUNDS : thm
val REAL_INF_LE' : thm
val REAL_INF_LE_FINITE : thm
val REAL_INF_LT_FINITE : thm
val REAL_INF_UNIQUE : thm
val REAL_LE_BETWEEN : thm
val REAL_LE_INF : thm
val REAL_LE_INF_FINITE : thm
val REAL_LE_INF_SUBSET : thm
val REAL_LE_LDIV_CANCEL : thm
val REAL_LE_LT_MUL : thm
val REAL_LE_MUL' : thm
val REAL_LE_MUL_EPSILON : thm
val REAL_LE_RDIV_EQ_NEG : thm
val REAL_LE_SQUARE_ABS : thm
val REAL_LE_SUP' : thm
val REAL_LE_SUP_EQ : thm
val REAL_LE_SUP_FINITE : thm
val REAL_LT_BETWEEN : thm
val REAL_LT_INF_FINITE : thm
val REAL_LT_INV2 : thm
val REAL_LT_LCANCEL_IMP : thm
val REAL_LT_LDIV_CANCEL : thm
val REAL_LT_LE_MUL : thm
val REAL_LT_LMUL' : thm
val REAL_LT_LMUL_0_NEG : thm
val REAL_LT_LMUL_NEG_0 : thm
val REAL_LT_LMUL_NEG_0_NEG : thm
val REAL_LT_MAX_BETWEEN : thm
val REAL_LT_MUL' : thm
val REAL_LT_POW2 : thm
val REAL_LT_RDIV_EQ_NEG : thm
val REAL_LT_RMUL' : thm
val REAL_LT_RMUL_0_NEG : thm
val REAL_LT_RMUL_NEG_0 : thm
val REAL_LT_RMUL_NEG_0_NEG : thm
val REAL_LT_SUP_FINITE : thm
val REAL_MAX_REDUCE : thm
val REAL_MIN_LE_BETWEEN : thm
val REAL_MIN_REDUCE : thm
val REAL_MUL_IDEMPOT : thm
val REAL_MUL_SUM : thm
val REAL_MUL_SUM_NUMSEG : thm
val REAL_NEG_NZ : thm
val REAL_OF_NUM_GE : thm
val REAL_OF_NUM_NPRODUCT : thm
val REAL_OF_NUM_SUM : thm
val REAL_OF_NUM_SUM_NUMSEG : thm
val REAL_POLYFUN_EQ_0 : thm
val REAL_POLYFUN_EQ_CONST : thm
val REAL_POLYFUN_FINITE_ROOTS : thm
val REAL_POLYFUN_ROOTBOUND : thm
val REAL_SUB_POLYFUN : thm
val REAL_SUB_POLYFUN_ALT : thm
val REAL_SUB_POW : thm
val REAL_SUB_POW_L1 : thm
val REAL_SUB_POW_R1 : thm
val REAL_SUP_ASCLOSE : thm
val REAL_SUP_BOUNDS : thm
val REAL_SUP_EQ_INF : thm
val REAL_SUP_LE' : thm
val REAL_SUP_LE_EQ : thm
val REAL_SUP_LE_FINITE : thm
val REAL_SUP_LE_SUBSET : thm
val REAL_SUP_LE_X : thm
val REAL_SUP_LT_FINITE : thm
val REAL_SUP_UNIQUE : thm
val REAL_WLOG_LE : thm
val REAL_WLOG_LT : thm
val REAL_X_LE_SUP : thm
val SET_PROVE_CASES : thm
val SET_RECURSION_LEMMA : thm
val SIMPLE_IMAGE_GEN : thm
val SUBSET_NUMSEG : thm
val SUBSET_RESTRICT : thm
val SUMS_SYM : thm
val SUM_0' : thm
val SUM_ABS' : thm
val SUM_ABS_BOUND : thm
val SUM_ABS_LE' : thm
val SUM_ABS_NUMSEG : thm
val SUM_ABS_TRIANGLE : thm
val SUM_ADD' : thm
val SUM_ADD_COUNT : thm
val SUM_ADD_GEN : thm
val SUM_ADD_NUMSEG : thm
val SUM_ADD_SPLIT : thm
val SUM_BIGUNION_NONZERO : thm
val SUM_BIJECTION : thm
val SUM_BOUND' : thm
val SUM_BOUND_GEN : thm
val SUM_BOUND_LT : thm
val SUM_BOUND_LT_ALL : thm
val SUM_BOUND_LT_GEN : thm
val SUM_CASES : thm
val SUM_CASES_1 : thm
val SUM_CLAUSES : thm
val SUM_CLAUSES_LEFT : thm
val SUM_CLAUSES_NUMSEG : thm
val SUM_CLAUSES_RIGHT : thm
val SUM_CLOSED : thm
val SUM_COMBINE_L : thm
val SUM_COMBINE_R : thm
val SUM_CONG : thm
val SUM_CONST : thm
val SUM_CONST_NUMSEG : thm
val SUM_DEGENERATE : thm
val SUM_DELETE : thm
val SUM_DELETE_CASES : thm
val SUM_DELTA : thm
val SUM_DIFF' : thm
val SUM_DIFFS' : thm
val SUM_DIFFS_ALT : thm
val SUM_EQ' : thm
val SUM_EQ_0' : thm
val SUM_EQ_0_NUMSEG : thm
val SUM_EQ_COUNT : thm
val SUM_EQ_GENERAL : thm
val SUM_EQ_GENERAL_INVERSES : thm
val SUM_EQ_NUMSEG : thm
val SUM_EQ_SUPERSET : thm
val SUM_GP : thm
val SUM_GP_BASIC : thm
val SUM_GP_MULTIPLIED : thm
val SUM_GROUP' : thm
val SUM_IMAGE : thm
val SUM_IMAGE_GEN : thm
val SUM_IMAGE_LE : thm
val SUM_IMAGE_NONZERO : thm
val SUM_INCL_EXCL : thm
val SUM_INJECTION : thm
val SUM_LE' : thm
val SUM_LE_INCLUDED : thm
val SUM_LE_NUMSEG : thm
val SUM_LMUL : thm
val SUM_LT' : thm
val SUM_LT_ALL : thm
val SUM_MULTICOUNT : thm
val SUM_MULTICOUNT_GEN : thm
val SUM_NEG' : thm
val SUM_OFFSET' : thm
val SUM_OFFSET_0 : thm
val SUM_PAIR : thm
val SUM_PARTIAL_PRE : thm
val SUM_PARTIAL_SUC : thm
val SUM_PERMUTATIONS_COMPOSE_L : thm
val SUM_PERMUTATIONS_COMPOSE_L_COUNT : thm
val SUM_PERMUTATIONS_COMPOSE_L_NUMSEG : thm
val SUM_PERMUTATIONS_COMPOSE_R : thm
val SUM_PERMUTATIONS_COMPOSE_R_COUNT : thm
val SUM_PERMUTATIONS_COMPOSE_R_NUMSEG : thm
val SUM_PERMUTATIONS_INVERSE : thm
val SUM_PERMUTE : thm
val SUM_PERMUTE_COUNT : thm
val SUM_PERMUTE_NUMSEG : thm
val SUM_POS_BOUND : thm
val SUM_POS_EQ_0 : thm
val SUM_POS_EQ_0_NUMSEG : thm
val SUM_POS_LE : thm
val SUM_POS_LE_NUMSEG : thm
val SUM_POS_LT : thm
val SUM_POS_LT_ALL : thm
val SUM_RESTRICT : thm
val SUM_RESTRICT_SET : thm
val SUM_RMUL : thm
val SUM_SING : thm
val SUM_SING_NUMSEG : thm
val SUM_SUB' : thm
val SUM_SUBSET : thm
val SUM_SUBSET_SIMPLE : thm
val SUM_SUB_NUMSEG : thm
val SUM_SUM_PRODUCT : thm
val SUM_SUM_RESTRICT : thm
val SUM_SUPERSET : thm
val SUM_SUPPORT : thm
val SUM_SWAP : thm
val SUM_SWAP_COUNT : thm
val SUM_SWAP_NUMSEG : thm
val SUM_TRIV_NUMSEG : thm
val SUM_UNION : thm
val SUM_UNION_EQ : thm
val SUM_UNION_LZERO : thm
val SUM_UNION_NONZERO : thm
val SUM_UNION_RZERO : thm
val SUM_ZERO_EXISTS : thm
val SUP : thm
val SUPPORT_CLAUSES : thm
val SUPPORT_DELTA : thm
val SUPPORT_EMPTY : thm
val SUPPORT_SUBSET : thm
val SUPPORT_SUPPORT : thm
val SUP_EQ : thm
val SUP_FINITE : thm
val SUP_FINITE_LEMMA : thm
val SUP_INSERT_FINITE : thm
val SUP_MONO : thm
val SUP_SING : thm
val SUP_UNION : thm
val SUP_UNIQUE : thm
val SUP_UNIQUE_FINITE : thm
val TOPOLOGICAL_SORT : thm
val TOPOLOGICAL_SORT' : thm
val TRANSITIVE_STEPWISE_LE : thm
val TRANSITIVE_STEPWISE_LE_EQ : thm
val UNION_COUNT_FROM : thm
val UNION_FROM_COUNT : thm
val UPPER_BOUND_FINITE_SET : thm
val UPPER_BOUND_FINITE_SET_REAL : thm
val inf_alt : thm
val lifted : thm
val lifted_ind : thm
val real_INFINITE : thm
val sum_real : thm
val sup_alt : thm
val iterate_grammars : type_grammar.grammar * term_grammar.grammar
(*
[permutes] Parent theory of "iterate"
[real] Parent theory of "iterate"
[FINREC_def] Definition
⊢ (∀f b s a. FINREC f b s a 0 ⇔ s = ∅ ∧ a = b) ∧
∀f b s a n.
FINREC f b s a (SUC n) ⇔
∃x c. x ∈ s ∧ FINREC f b (s DELETE x) c n ∧ a = f x c
[from_def] Definition
⊢ ∀n. from n = {m | n ≤ m}
[indicator] Definition
⊢ ∀s. indicator s = (λx. if x ∈ s then 1 else 0)
[iterate] Definition
⊢ ∀op s f.
iterate op s f =
if FINITE (support op f s) then
ITSET (λx a. op (f x) a) (support op f s) (neutral op)
else neutral op
[monoidal] Definition
⊢ ∀op.
monoidal op ⇔
(∀x y. op x y = op y x) ∧
(∀x y z. op x (op y z) = op (op x y) z) ∧
∀x. op (neutral op) x = x
[neutral] Definition
⊢ ∀op. neutral op = @x. ∀y. op x y = y ∧ op y x = y
[nproduct] Definition
⊢ nproduct = iterate $*
[nsum] Definition
⊢ nsum = iterate $+
[numseg] Definition
⊢ ∀m n. {m .. n} = {x | m ≤ x ∧ x ≤ n}
[polynomial_function] Definition
⊢ ∀p. polynomial_function p ⇔
∃m c. ∀x. p x = sum {0 .. m} (λi. c i * x pow i)
[product] Definition
⊢ product = iterate $*
[sum_def] Definition
⊢ sum = iterate $+
[support] Definition
⊢ ∀op f s. support op f s = {x | x ∈ s ∧ f x ≠ neutral op}
[ABS_LE_0] Theorem
⊢ ∀x. abs x ≤ 0 ⇔ x = 0
[ABS_LE_HALF_POW2] Theorem
⊢ ∀x y. abs (x * y) ≤ 1 / 2 * (x² + y²)
[ADD_SUB2] Theorem
⊢ ∀m n. m + n − m = n
[ADD_SUBR] Theorem
⊢ ∀m n. n − (m + n) = 0
[ADD_SUBR2] Theorem
⊢ ∀m n. m − (m + n) = 0
[BIGINTER_BIGUNION] Theorem
⊢ ∀s. BIGINTER s = 𝕌(:α) DIFF BIGUNION {𝕌(:α) DIFF t | t ∈ s}
[BIGINTER_GSPEC] Theorem
⊢ (∀P f. BIGINTER {f x | P x} = {a | ∀x. P x ⇒ a ∈ f x}) ∧
(∀P f. BIGINTER {f x y | P x y} = {a | ∀x y. P x y ⇒ a ∈ f x y}) ∧
∀P f.
BIGINTER {f x y z | P x y z} =
{a | ∀x y z. P x y z ⇒ a ∈ f x y z}
[BIGUNION_BIGINTER] Theorem
⊢ ∀s. BIGUNION s = 𝕌(:α) DIFF BIGINTER {𝕌(:α) DIFF t | t ∈ s}
[BIGUNION_GSPEC] Theorem
⊢ (∀P f. BIGUNION {f x | P x} = {a | ∃x. P x ∧ a ∈ f x}) ∧
(∀P f. BIGUNION {f x y | P x y} = {a | ∃x y. P x y ∧ a ∈ f x y}) ∧
∀P f.
BIGUNION {f x y z | P x y z} =
{a | ∃x y z. P x y z ∧ a ∈ f x y z}
[BOUNDS_LINEAR] Theorem
⊢ ∀A B C. (∀n. A * n ≤ B * n + C) ⇔ A ≤ B
[BOUNDS_LINEAR_0] Theorem
⊢ ∀A B. (∀n. A * n ≤ B) ⇔ A = 0
[CARD_BIGUNION] Theorem
⊢ ∀s. FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t u. t ∈ s ∧ u ∈ s ∧ t ≠ u ⇒ t ∩ u = ∅) ⇒
CARD (BIGUNION s) = nsum s CARD
[CARD_EQ_NSUM] Theorem
⊢ ∀s. FINITE s ⇒ CARD s = nsum s (λx. 1)
[CARD_EQ_SUM] Theorem
⊢ ∀s. FINITE s ⇒ &CARD s = sum s (λx. 1)
[CARD_NUMSEG] Theorem
⊢ ∀m n. CARD {m .. n} = n + 1 − m
[CARD_NUMSEG_1] Theorem
⊢ ∀n. CARD {1 .. n} = n
[CARD_NUMSEG_LEMMA] Theorem
⊢ ∀m d. CARD {m .. m + d} = d + 1
[CARD_UNION_EQ] Theorem
⊢ ∀s t u. FINITE u ∧ s ∩ t = ∅ ∧ s ∪ t = u ⇒ CARD s + CARD t = CARD u
[CHOOSE_SUBSET] Theorem
⊢ ∀s. FINITE s ⇒ ∀n. n ≤ CARD s ⇒ ∃t. t ⊆ s ∧ t HAS_SIZE n
[CHOOSE_SUBSET_STRONG] Theorem
⊢ ∀n s. (FINITE s ⇒ n ≤ CARD s) ⇒ ∃t. t ⊆ s ∧ t HAS_SIZE n
[COUNTABLE_FROM] Theorem
⊢ ∀n. countable (from n)
[COUNT_NUMSEG] Theorem
⊢ ∀n. 0 < n ⇒ count n = {0 .. n − 1}
[DIFF_BIGINTER2] Theorem
⊢ ∀u s. u DIFF BIGINTER s = BIGUNION {u DIFF t | t ∈ s}
[DISJOINT_COUNT_FROM] Theorem
⊢ ∀n. DISJOINT (count n) (from n)
[DISJOINT_FROM_COUNT] Theorem
⊢ ∀n. DISJOINT (from n) (count n)
[DISJOINT_NUMSEG] Theorem
⊢ ∀m n p q.
DISJOINT {m .. n} {p .. q} ⇔ n < p ∨ q < m ∨ n < m ∨ q < p
[DROP_INDICATOR] Theorem
⊢ ∀s x. indicator s x = if x ∈ s then 1 else 0
[DROP_INDICATOR_ABS_LE_1] Theorem
⊢ ∀s x. abs (indicator s x) ≤ 1
[DROP_INDICATOR_LE_1] Theorem
⊢ ∀s x. indicator s x ≤ 1
[DROP_INDICATOR_POS_LE] Theorem
⊢ ∀s x. 0 ≤ indicator s x
[EMPTY_BIGUNION] Theorem
⊢ ∀s. BIGUNION s = ∅ ⇔ ∀t. t ∈ s ⇒ t = ∅
[EXISTS_FINITE_SUBSET_IMAGE] Theorem
⊢ ∀P f s.
(∃t. FINITE t ∧ t ⊆ IMAGE f s ∧ P t) ⇔
∃t. FINITE t ∧ t ⊆ s ∧ P (IMAGE f t)
[FINITE_INDEX_NUMBERS] Theorem
⊢ ∀s. FINITE s ⇔
∃k f.
(∀i j. i ∈ k ∧ j ∈ k ∧ f i = f j ⇒ i = j) ∧ FINITE k ∧
s = IMAGE f k
[FINITE_INDEX_NUMSEG] Theorem
⊢ ∀s. FINITE s ⇔
∃f. (∀i j.
i ∈ {1 .. CARD s} ∧ j ∈ {1 .. CARD s} ∧ f i = f j ⇒
i = j) ∧ s = IMAGE f {1 .. CARD s}
[FINITE_NUMSEG] Theorem
⊢ ∀m n. FINITE {m .. n}
[FINITE_POWERSET] Theorem
⊢ ∀s. FINITE s ⇒ FINITE {t | t ⊆ s}
[FINITE_REAL_INTERVAL] Theorem
⊢ (∀a. INFINITE {x | a < x}) ∧ (∀a. INFINITE {x | a ≤ x}) ∧
(∀b. INFINITE {x | x < b}) ∧ (∀b. INFINITE {x | x ≤ b}) ∧
(∀a b. FINITE {x | a < x ∧ x < b} ⇔ b ≤ a) ∧
(∀a b. FINITE {x | a ≤ x ∧ x < b} ⇔ b ≤ a) ∧
(∀a b. FINITE {x | a < x ∧ x ≤ b} ⇔ b ≤ a) ∧
∀a b. FINITE {x | a ≤ x ∧ x ≤ b} ⇔ b ≤ a
[FINITE_RECURSION] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
ITSET f ∅ b = b ∧
∀x s.
FINITE s ⇒
ITSET f (x INSERT s) b =
if x ∈ s then ITSET f s b else f x (ITSET f s b)
[FINITE_RESTRICT] Theorem
⊢ ∀s P. FINITE s ⇒ FINITE {x | x ∈ s ∧ P x}
[FINITE_SUBSET_IMAGE] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ IMAGE f s ⇔
∃s'. FINITE s' ∧ s' ⊆ s ∧ t = IMAGE f s'
[FINITE_SUPPORT] Theorem
⊢ ∀op f s. FINITE s ⇒ FINITE (support op f s)
[FINITE_SUPPORT_DELTA] Theorem
⊢ ∀op f a.
FINITE (support op (λx. if x = a then f x else neutral op) s)
[FINREC_1_LEMMA] Theorem
⊢ ∀f b s a. FINREC f b s a (SUC 0) ⇔ ∃x. s = {x} ∧ a = f x b
[FINREC_EXISTS_LEMMA] Theorem
⊢ ∀f b s. FINITE s ⇒ ∃a n. FINREC f b s a n
[FINREC_FUN] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
∃g. g ∅ = b ∧ ∀s x. FINITE s ∧ x ∈ s ⇒ g s = f x (g (s DELETE x))
[FINREC_FUN_LEMMA] Theorem
⊢ ∀P R.
(∀s. P s ⇒ ∃a n. R s a n) ∧
(∀n1 n2 s a1 a2. R s a1 n1 ∧ R s a2 n2 ⇒ a1 = a2 ∧ n1 = n2) ⇒
∃f. ∀s a. P s ⇒ ((∃n. R s a n) ⇔ f s = a)
[FINREC_SUC_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
∀n s z.
FINREC f b s z (SUC n) ⇒
∀x. x ∈ s ⇒ ∃w. FINREC f b (s DELETE x) w n ∧ z = f x w
[FINREC_UNIQUE_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
∀n1 n2 s a1 a2.
FINREC f b s a1 n1 ∧ FINREC f b s a2 n2 ⇒ a1 = a2 ∧ n1 = n2
[FINREC_compute] Theorem
⊢ (∀f b s a. FINREC f b s a 0 ⇔ s = ∅ ∧ a = b) ∧
(∀f b s a n.
FINREC f b s a (NUMERAL (BIT1 n)) ⇔
∃x c.
x ∈ s ∧ FINREC f b (s DELETE x) c (NUMERAL (BIT1 n) − 1) ∧
a = f x c) ∧
∀f b s a n.
FINREC f b s a (NUMERAL (BIT2 n)) ⇔
∃x c.
x ∈ s ∧ FINREC f b (s DELETE x) c (NUMERAL (BIT1 n)) ∧
a = f x c
[FORALL_FINITE_SUBSET_IMAGE] Theorem
⊢ ∀P f s.
(∀t. FINITE t ∧ t ⊆ IMAGE f s ⇒ P t) ⇔
∀t. FINITE t ∧ t ⊆ s ⇒ P (IMAGE f t)
[FROM_0] Theorem
⊢ from 0 = 𝕌(:num)
[FROM_INTER_NUMSEG] Theorem
⊢ ∀k n. from k ∩ {0 .. n} = {k .. n}
[FROM_INTER_NUMSEG_GEN] Theorem
⊢ ∀k m n. from k ∩ {m .. n} = if m < k then {k .. n} else {m .. n}
[FROM_INTER_NUMSEG_MAX] Theorem
⊢ ∀m n p. from p ∩ {m .. n} = {MAX p m .. n}
[FROM_NOT_EMPTY] Theorem
⊢ ∀n. from n ≠ ∅
[FUN_IN_IMAGE] Theorem
⊢ ∀f s x. x ∈ s ⇒ f x ∈ IMAGE f s
[HAS_SIZE_NUMSEG] Theorem
⊢ ∀m n. {m .. n} HAS_SIZE n + 1 − m
[HAS_SIZE_NUMSEG_1] Theorem
⊢ ∀n. {1 .. n} HAS_SIZE n
[INDICATOR_COMPLEMENT] Theorem
⊢ ∀s. indicator (𝕌(:α) DIFF s) = (λx. 1 − indicator s x)
[INDICATOR_EMPTY] Theorem
⊢ indicator ∅ = (λx. 0)
[INF] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
(∀x. x ∈ s ⇒ inf s ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s
[INFINITE_FROM] Theorem
⊢ ∀n. INFINITE (from n)
[INF_CLOSE] Theorem
⊢ ∀p e. (∃x. x ∈ p) ∧ 0 < e ⇒ ∃x. x ∈ p ∧ x < inf p + e
[INF_DEF_ALT] Theorem
⊢ ∀p. inf p = -sup (λr. -r ∈ p)
[INF_EQ] Theorem
⊢ ∀s t.
s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ∧ t ≠ ∅ ∧
(∃b. ∀x. x ∈ t ⇒ b ≤ x) ∧
(∀a. (∀x. x ∈ s ⇒ a ≤ x) ⇔ ∀x. x ∈ t ⇒ a ≤ x) ⇒
inf s = inf t
[INF_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ inf s ∈ s ∧ ∀x. x ∈ s ⇒ inf s ≤ x
[INF_FINITE_LEMMA] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ b ≤ x
[INF_GREATER] Theorem
⊢ ∀p z. (∃x. x ∈ p) ∧ inf p < z ⇒ ∃x. x ∈ p ∧ x < z
[INF_INSERT_FINITE] Theorem
⊢ ∀x s.
FINITE s ⇒ inf (x INSERT s) = if s = ∅ then x else min x (inf s)
[INF_LE] Theorem
⊢ ∀p r. (∃z. ∀x. x ∈ p ⇒ z ≤ x) ∧ (∃x. x ∈ p ∧ x ≤ r) ⇒ inf p ≤ r
[INF_SING] Theorem
⊢ ∀a. inf {a} = a
[INF_UNIQUE_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s = a ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ a ≤ y)
[IN_FROM] Theorem
⊢ ∀m n. m ∈ from n ⇔ n ≤ m
[IN_NUMSEG] Theorem
⊢ x ∈ {m .. n} ⇔ m ≤ x ∧ x ≤ n
[IN_NUMSEG_0] Theorem
⊢ ∀m n. m ∈ {0 .. n} ⇔ m ≤ n
[IN_SUPPORT] Theorem
⊢ ∀op f x s. x ∈ support op f s ⇔ x ∈ s ∧ f x ≠ neutral op
[ITERATE_AND] Theorem
⊢ ∀p s. FINITE s ⇒ (iterate $/\ s p ⇔ ∀x. x ∈ s ⇒ p x)
[ITERATE_BIJECTION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ p x = y) ⇒
iterate op s f = iterate op s (f ∘ p)
[ITERATE_CASES] Theorem
⊢ ∀op.
monoidal op ⇒
∀s P f g.
FINITE s ⇒
iterate op s (λx. if P x then f x else g x) =
op (iterate op {x | x ∈ s ∧ P x} f)
(iterate op {x | x ∈ s ∧ ¬P x} g)
[ITERATE_CLAUSES] Theorem
⊢ ∀op.
monoidal op ⇒
(∀f. iterate op ∅ f = neutral op) ∧
∀f x s.
FINITE s ⇒
iterate op (x INSERT s) f =
if x ∈ s then iterate op s f else op (f x) (iterate op s f)
[ITERATE_CLAUSES_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
(∀f. iterate op ∅ f = neutral op) ∧
∀f x s.
monoidal op ∧ FINITE (support op f s) ⇒
iterate op (x INSERT s) f =
if x ∈ s then iterate op s f else op (f x) (iterate op s f)
[ITERATE_CLAUSES_NUMSEG] Theorem
⊢ ∀op.
monoidal op ⇒
(∀m. iterate op {m .. 0} f = if m = 0 then f 0 else neutral op) ∧
∀m n.
iterate op {m .. SUC n} f =
if m ≤ SUC n then op (iterate op {m .. n} f) (f (SUC n))
else iterate op {m .. n} f
[ITERATE_CLOSED] Theorem
⊢ ∀op.
monoidal op ⇒
∀P. P (neutral op) ∧ (∀x y. P x ∧ P y ⇒ P (op x y)) ⇒
∀f s.
(∀x. x ∈ s ∧ f x ≠ neutral op ⇒ P (f x)) ⇒
P (iterate op s f)
[ITERATE_DELETE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s a.
FINITE s ∧ a ∈ s ⇒
op (f a) (iterate op (s DELETE a) f) = iterate op s f
[ITERATE_DELTA] Theorem
⊢ ∀op.
monoidal op ⇒
∀f a s.
iterate op s (λx. if x = a then f x else neutral op) =
if a ∈ s then f a else neutral op
[ITERATE_DIFF] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ t ⊆ s ⇒
op (iterate op (s DIFF t) f) (iterate op t f) = iterate op s f
[ITERATE_DIFF_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE (support op f s) ∧ support op f t ⊆ support op f s ⇒
op (iterate op (s DIFF t) f) (iterate op t f) = iterate op s f
[ITERATE_EQ] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ iterate op s f = iterate op s g
[ITERATE_EQ_GENERAL] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ h x = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ g (h x) = f x) ⇒
iterate op s f = iterate op t g
[ITERATE_EQ_GENERAL_INVERSES] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ h (k y) = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ k (h x) = x ∧ g (h x) = f x) ⇒
iterate op s f = iterate op t g
[ITERATE_EQ_NEUTRAL] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s.
(∀x. x ∈ s ⇒ f x = neutral op) ⇒ iterate op s f = neutral op
[ITERATE_EXPAND_CASES] Theorem
⊢ ∀op f s.
iterate op s f =
if FINITE (support op f s) then iterate op (support op f s) f
else neutral op
[ITERATE_IMAGE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
iterate op (IMAGE f s) g = iterate op s (g ∘ f)
[ITERATE_IMAGE_NONZERO] Theorem
⊢ ∀op.
monoidal op ⇒
∀g f s.
FINITE s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ f x = f y ⇒ g (f x) = neutral op) ⇒
iterate op (IMAGE f s) g = iterate op s (g ∘ f)
[ITERATE_INCL_EXCL] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f.
FINITE s ∧ FINITE t ⇒
op (iterate op s f) (iterate op t f) =
op (iterate op (s ∪ t) f) (iterate op (s ∩ t) f)
[ITERATE_INJECTION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y) ⇒
iterate op s (f ∘ p) = iterate op s f
[ITERATE_ITERATE_PRODUCT] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
iterate op s (λi. iterate op (t i) (x i)) =
iterate op {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j)
[ITERATE_NONZERO_IMAGE_LEMMA] Theorem
⊢ ∀op s f g a.
monoidal op ∧ FINITE s ∧ g a = neutral op ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ∧ x ≠ y ⇒ g (f x) = neutral op) ⇒
iterate op {f x | x | x ∈ s ∧ f x ≠ a} g = iterate op s (g ∘ f)
[ITERATE_OP] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
FINITE s ⇒
iterate op s (λx. op (f x) (g x)) =
op (iterate op s f) (iterate op s g)
[ITERATE_OP_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
FINITE (support op f s) ∧ FINITE (support op g s) ⇒
iterate op s (λx. op (f x) (g x)) =
op (iterate op s f) (iterate op s g)
[ITERATE_PAIR] Theorem
⊢ ∀op.
monoidal op ⇒
∀f m n.
iterate op {2 * m .. 2 * n + 1} f =
iterate op {m .. n} (λi. op (f (2 * i)) (f (2 * i + 1)))
[ITERATE_PERMUTE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s. p permutes s ⇒ iterate op s f = iterate op s (f ∘ p)
[ITERATE_PERMUTES] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s. p PERMUTES s ⇒ iterate op s f = iterate op s (f ∘ p)
[ITERATE_RELATED] Theorem
⊢ ∀op.
monoidal op ⇒
∀R. R (neutral op) (neutral op) ∧
(∀x1 y1 x2 y2. R x1 x2 ∧ R y1 y2 ⇒ R (op x1 y1) (op x2 y2)) ⇒
∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ R (f x) (g x)) ⇒
R (iterate op s f) (iterate op s g)
[ITERATE_SING] Theorem
⊢ ∀op. monoidal op ⇒ ∀f x. iterate op {x} f = f x
[ITERATE_SOME] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s.
FINITE s ⇒
iterate (lifted op) s (λx. SOME (f x)) = SOME (iterate op s f)
[ITERATE_SUPERSET] Theorem
⊢ ∀op.
monoidal op ⇒
∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = neutral op) ⇒
iterate op v f = iterate op u f
[ITERATE_SUPPORT] Theorem
⊢ ∀op f s. iterate op (support op f s) f = iterate op s f
[ITERATE_UNION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
iterate op (s ∪ t) f = op (iterate op s f) (iterate op t f)
[ITERATE_UNION_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE (support op f s) ∧ FINITE (support op f t) ∧
DISJOINT (support op f s) (support op f t) ⇒
iterate op (s ∪ t) f = op (iterate op s f) (iterate op t f)
[ITERATE_UNION_NONZERO] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ f x = neutral op) ⇒
iterate op (s ∪ t) f = op (iterate op s f) (iterate op t f)
[ITSET_alt] Theorem
⊢ ∀f s b.
(∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
ITSET f s b =
(@g. g ∅ = b ∧
∀x s.
FINITE s ⇒
g (x INSERT s) = if x ∈ s then g s else f x (g s)) s
[LAMBDA_PAIR] Theorem
⊢ (λ(x,y). P x y) = (λp. P (FST p) (SND p))
[LE_ADD] Theorem
⊢ ∀m n. m ≤ m + n
[LE_ADDR] Theorem
⊢ ∀m n. n ≤ m + n
[LE_EXISTS] Theorem
⊢ ∀m n. m ≤ n ⇔ ∃d. n = m + d
[LE_INF] Theorem
⊢ ∀p r. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ r ≤ x) ⇒ r ≤ inf p
[LOWER_BOUND_FINITE_SET_REAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ a ≤ f x
[LT_EXISTS] Theorem
⊢ ∀m n. m < n ⇔ ∃d. n = m + SUC d
[MOD_NSUM_MOD] Theorem
⊢ ∀f n s.
FINITE s ∧ n ≠ 0 ⇒ nsum s f MOD n = nsum s (λi. f i MOD n) MOD n
[MOD_NSUM_MOD_NUMSEG] Theorem
⊢ ∀f a b n.
n ≠ 0 ⇒
nsum {a .. b} f MOD n = nsum {a .. b} (λi. f i MOD n) MOD n
[MONOIDAL_AC] Theorem
⊢ ∀op.
monoidal op ⇒
(∀a. op (neutral op) a = a) ∧ (∀a. op a (neutral op) = a) ∧
(∀a b. op a b = op b a) ∧
(∀a b c. op (op a b) c = op a (op b c)) ∧
∀a b c. op a (op b c) = op b (op a c)
[MONOIDAL_ADD] Theorem
⊢ monoidal $+
[MONOIDAL_AND] Theorem
⊢ monoidal $/\
[MONOIDAL_LIFTED] Theorem
⊢ ∀op. monoidal op ⇒ monoidal (lifted op)
[MONOIDAL_MUL] Theorem
⊢ monoidal $*
[MONOIDAL_REAL_ADD] Theorem
⊢ monoidal $+
[MONOIDAL_REAL_MUL] Theorem
⊢ monoidal $*
[NEUTRAL_ADD] Theorem
⊢ neutral $+ = 0
[NEUTRAL_AND] Theorem
⊢ neutral $/\ ⇔ T
[NEUTRAL_LIFTED] Theorem
⊢ ∀op. monoidal op ⇒ neutral (lifted op) = SOME (neutral op)
[NEUTRAL_MUL] Theorem
⊢ neutral $* = 1
[NEUTRAL_REAL_ADD] Theorem
⊢ neutral $+ = 0
[NEUTRAL_REAL_MUL] Theorem
⊢ neutral $* = 1
[NOT_EQ] Theorem
⊢ ∀a b. a ≠ b ⇔ a ≠ b
[NPRODUCT_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
nproduct {m .. n + p} f =
nproduct {m .. n} f * nproduct {n + 1 .. n + p} f
[NPRODUCT_CLAUSES] Theorem
⊢ (∀f. nproduct ∅ f = 1) ∧
∀x f s.
FINITE s ⇒
nproduct (x INSERT s) f =
if x ∈ s then nproduct s f else f x * nproduct s f
[NPRODUCT_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ nproduct {m .. n} f = f m * nproduct {m + 1 .. n} f
[NPRODUCT_CLAUSES_NUMSEG] Theorem
⊢ (∀m. nproduct {m .. 0} f = if m = 0 then f 0 else 1) ∧
∀m n.
nproduct {m .. SUC n} f =
if m ≤ SUC n then nproduct {m .. n} f * f (SUC n)
else nproduct {m .. n} f
[NPRODUCT_CLAUSES_RIGHT] Theorem
⊢ ∀f m n.
0 < n ∧ m ≤ n ⇒
nproduct {m .. n} f = nproduct {m .. n − 1} f * f n
[NPRODUCT_CLOSED] Theorem
⊢ ∀P f s.
P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (nproduct s f)
[NPRODUCT_CONG] Theorem
⊢ (∀f g s.
(∀x. x ∈ s ⇒ f x = g x) ⇒ nproduct s (λi. f i) = nproduct s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
nproduct {a .. b} (λi. f i) = nproduct {a .. b} g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒
nproduct {y | p y} (λi. f i) = nproduct {y | p y} g
[NPRODUCT_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ nproduct s (λx. c) = c ** CARD s
[NPRODUCT_CONST_NUMSEG] Theorem
⊢ ∀c m n. nproduct {m .. n} (λx. c) = c ** (n + 1 − m)
[NPRODUCT_CONST_NUMSEG_1] Theorem
⊢ ∀c n. nproduct {1 .. n} (λx. c) = c ** n
[NPRODUCT_DELETE] Theorem
⊢ ∀f s a.
FINITE s ∧ a ∈ s ⇒ f a * nproduct (s DELETE a) f = nproduct s f
[NPRODUCT_DELTA] Theorem
⊢ ∀s a.
nproduct s (λx. if x = a then b else 1) = if a ∈ s then b else 1
[NPRODUCT_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ nproduct s f = nproduct s g
[NPRODUCT_EQ_0] Theorem
⊢ ∀f s. FINITE s ⇒ (nproduct s f = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)
[NPRODUCT_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. nproduct {m .. n} f = 0 ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ f x = 0
[NPRODUCT_EQ_1] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 1) ⇒ nproduct s f = 1
[NPRODUCT_EQ_1_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 1) ⇒ nproduct {m .. n} f = 1
[NPRODUCT_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
nproduct {m .. n} f = nproduct {m .. n} g
[NPRODUCT_FACT] Theorem
⊢ ∀n. nproduct {1 .. n} (λm. m) = FACT n
[NPRODUCT_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
nproduct (IMAGE f s) g = nproduct s (g ∘ f)
[NPRODUCT_LE] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒
nproduct s f ≤ nproduct s g
[NPRODUCT_LE_NUMSEG] Theorem
⊢ ∀f m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
nproduct {m .. n} f ≤ nproduct {m .. n} g
[NPRODUCT_MUL] Theorem
⊢ ∀f g s.
FINITE s ⇒
nproduct s (λx. f x * g x) = nproduct s f * nproduct s g
[NPRODUCT_MUL_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
nproduct s (λx. f x * g x) = nproduct s f * nproduct s g
[NPRODUCT_MUL_NUMSEG] Theorem
⊢ ∀f g m n.
nproduct {m .. n} (λx. f x * g x) =
nproduct {m .. n} f * nproduct {m .. n} g
[NPRODUCT_OFFSET] Theorem
⊢ ∀f m p.
nproduct {m + p .. n + p} f = nproduct {m .. n} (λi. f (i + p))
[NPRODUCT_ONE] Theorem
⊢ ∀s. nproduct s (λn. 1) = 1
[NPRODUCT_PAIR] Theorem
⊢ ∀f m n.
nproduct {2 * m .. 2 * n + 1} f =
nproduct {m .. n} (λi. f (2 * i) * f (2 * i + 1))
[NPRODUCT_POS_LT] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < nproduct s f
[NPRODUCT_POS_LT_NUMSEG] Theorem
⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < nproduct {m .. n} f
[NPRODUCT_SING] Theorem
⊢ ∀f x. nproduct {x} f = f x
[NPRODUCT_SING_NUMSEG] Theorem
⊢ ∀f n. nproduct {n .. n} f = f n
[NPRODUCT_SUPERSET] Theorem
⊢ ∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 1) ⇒
nproduct v f = nproduct u f
[NPRODUCT_SUPPORT] Theorem
⊢ ∀f s. nproduct (support $* f s) f = nproduct s f
[NPRODUCT_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
nproduct (s ∪ t) f = nproduct s f * nproduct t f
[NSUM_0] Theorem
⊢ ∀s. nsum s (λn. 0) = 0
[NSUM_ADD] Theorem
⊢ ∀f g s. FINITE s ⇒ nsum s (λx. f x + g x) = nsum s f + nsum s g
[NSUM_ADD_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 0} ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
nsum s (λx. f x + g x) = nsum s f + nsum s g
[NSUM_ADD_NUMSEG] Theorem
⊢ ∀f g m n.
nsum {m .. n} (λi. f i + g i) = nsum {m .. n} f + nsum {m .. n} g
[NSUM_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
nsum {m .. n + p} f = nsum {m .. n} f + nsum {n + 1 .. n + p} f
[NSUM_BIGUNION_NONZERO] Theorem
⊢ ∀f s.
FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t1 t2 x. t1 ∈ s ∧ t2 ∈ s ∧ t1 ≠ t2 ∧ x ∈ t1 ∧ x ∈ t2 ⇒ f x = 0) ⇒
nsum (BIGUNION s) f = nsum s (λt. nsum t f)
[NSUM_BIJECTION] Theorem
⊢ ∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ p x = y) ⇒
nsum s f = nsum s (f ∘ p)
[NSUM_BOUND] Theorem
⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ nsum s f ≤ CARD s * b
[NSUM_BOUND_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b DIV CARD s) ⇒
nsum s f ≤ b
[NSUM_BOUND_LT] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ∧ (∃x. x ∈ s ∧ f x < b) ⇒
nsum s f < CARD s * b
[NSUM_BOUND_LT_ALL] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒ nsum s f < CARD s * b
[NSUM_BOUND_LT_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b DIV CARD s) ⇒
nsum s f < b
[NSUM_CASES] Theorem
⊢ ∀s P f g.
FINITE s ⇒
nsum s (λx. if P x then f x else g x) =
nsum {x | x ∈ s ∧ P x} f + nsum {x | x ∈ s ∧ ¬P x} g
[NSUM_CLAUSES] Theorem
⊢ (∀f. nsum ∅ f = 0) ∧
∀x f s.
FINITE s ⇒
nsum (x INSERT s) f = if x ∈ s then nsum s f else f x + nsum s f
[NSUM_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ nsum {m .. n} f = f m + nsum {m + 1 .. n} f
[NSUM_CLAUSES_NUMSEG] Theorem
⊢ (∀m. nsum {m .. 0} f = if m = 0 then f 0 else 0) ∧
∀m n.
nsum {m .. SUC n} f =
if m ≤ SUC n then nsum {m .. n} f + f (SUC n)
else nsum {m .. n} f
[NSUM_CLAUSES_RIGHT] Theorem
⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ nsum {m .. n} f = nsum {m .. n − 1} f + f n
[NSUM_CLOSED] Theorem
⊢ ∀P f s.
P 0 ∧ (∀x y. P x ∧ P y ⇒ P (x + y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (nsum s f)
[NSUM_CONG] Theorem
⊢ (∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ nsum s (λi. f i) = nsum s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
nsum {a .. b} (λi. f i) = nsum {a .. b} g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒
nsum {y | p y} (λi. f i) = nsum {y | p y} g
[NSUM_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ nsum s (λn. c) = CARD s * c
[NSUM_CONST_NUMSEG] Theorem
⊢ ∀c m n. nsum {m .. n} (λn. c) = (n + 1 − m) * c
[NSUM_DEGENERATE] Theorem
⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ nsum s f = 0
[NSUM_DELETE] Theorem
⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ f a + nsum (s DELETE a) f = nsum s f
[NSUM_DELTA] Theorem
⊢ ∀s a. nsum s (λx. if x = a then b else 0) = if a ∈ s then b else 0
[NSUM_DIFF] Theorem
⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ nsum (s DIFF t) f = nsum s f − nsum t f
[NSUM_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ nsum s f = nsum s g
[NSUM_EQ_0] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ nsum s f = 0
[NSUM_EQ_0_IFF] Theorem
⊢ ∀s. FINITE s ⇒ (nsum s f = 0 ⇔ ∀x. x ∈ s ⇒ f x = 0)
[NSUM_EQ_0_IFF_NUMSEG] Theorem
⊢ ∀f m n. nsum {m .. n} f = 0 ⇔ ∀i. m ≤ i ∧ i ≤ n ⇒ f i = 0
[NSUM_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 0) ⇒ nsum {m .. n} f = 0
[NSUM_EQ_GENERAL] Theorem
⊢ ∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ h x = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ g (h x) = f x) ⇒
nsum s f = nsum t g
[NSUM_EQ_GENERAL_INVERSES] Theorem
⊢ ∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ h (k y) = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ k (h x) = x ∧ g (h x) = f x) ⇒
nsum s f = nsum t g
[NSUM_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
nsum {m .. n} f = nsum {m .. n} g
[NSUM_EQ_SUPERSET] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ s ∧ (∀x. x ∈ t ⇒ f x = g x) ∧
(∀x. x ∈ s ∧ x ∉ t ⇒ f x = 0) ⇒
nsum s f = nsum t g
[NSUM_GROUP] Theorem
⊢ ∀f g s t.
FINITE s ∧ IMAGE f s ⊆ t ⇒
nsum t (λy. nsum {x | x ∈ s ∧ f x = y} g) = nsum s g
[NSUM_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
nsum (IMAGE f s) g = nsum s (g ∘ f)
[NSUM_IMAGE_GEN] Theorem
⊢ ∀f g s.
FINITE s ⇒
nsum s g = nsum (IMAGE f s) (λy. nsum {x | x ∈ s ∧ f x = y} g)
[NSUM_IMAGE_NONZERO] Theorem
⊢ ∀d i s.
FINITE s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ i x = i y ⇒ d (i x) = 0) ⇒
nsum (IMAGE i s) d = nsum s (d ∘ i)
[NSUM_INCL_EXCL] Theorem
⊢ ∀s t f.
FINITE s ∧ FINITE t ⇒
nsum s f + nsum t f = nsum (s ∪ t) f + nsum (s ∩ t) f
[NSUM_INJECTION] Theorem
⊢ ∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y) ⇒
nsum s (f ∘ p) = nsum s f
[NSUM_LE] Theorem
⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ nsum s f ≤ nsum s g
[NSUM_LE_GEN] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x ≤ g x) ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
nsum s f ≤ nsum s g
[NSUM_LE_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒
nsum {m .. n} f ≤ nsum {m .. n} g
[NSUM_LMUL] Theorem
⊢ ∀f c s. nsum s (λx. c * f x) = c * nsum s f
[NSUM_LT] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
nsum s f < nsum s g
[NSUM_LT_ALL] Theorem
⊢ ∀f g s.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒ nsum s f < nsum s g
[NSUM_MULTICOUNT] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k) ⇒
nsum s (λi. CARD (equiv_class R t i)) = k * CARD t
[NSUM_MULTICOUNT_GEN] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧
(∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k j) ⇒
nsum s (λi. CARD (equiv_class R t i)) = nsum t (λi. k i)
[NSUM_NSUM_PRODUCT] Theorem
⊢ ∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
nsum s (λi. nsum (t i) (x i)) =
nsum {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j)
[NSUM_NSUM_RESTRICT] Theorem
⊢ ∀R f s t.
FINITE s ∧ FINITE t ⇒
nsum s (λx. nsum (equiv_class R t x) (λy. f x y)) =
nsum t (λy. nsum {x | x ∈ s ∧ R x y} (λx. f x y))
[NSUM_OFFSET] Theorem
⊢ ∀p f m n. nsum {m + p .. n + p} f = nsum {m .. n} (λi. f (i + p))
[NSUM_OFFSET_0] Theorem
⊢ ∀f m n. m ≤ n ⇒ nsum {m .. n} f = nsum {0 .. n − m} (λi. f (i + m))
[NSUM_PAIR] Theorem
⊢ ∀f m n.
nsum {2 * m .. 2 * n + 1} f =
nsum {m .. n} (λi. f (2 * i) + f (2 * i + 1))
[NSUM_PERMUTE] Theorem
⊢ ∀f p s. p permutes s ⇒ nsum s f = nsum s (f ∘ p)
[NSUM_PERMUTE_COUNT] Theorem
⊢ ∀f p n.
p permutes count n ⇒ nsum (count n) f = nsum (count n) (f ∘ p)
[NSUM_PERMUTE_NUMSEG] Theorem
⊢ ∀f p m n.
p permutes count n DIFF count m ⇒
nsum (count n DIFF count m) f =
nsum (count n DIFF count m) (f ∘ p)
[NSUM_POS_BOUND] Theorem
⊢ ∀f b s. FINITE s ∧ nsum s f ≤ b ⇒ ∀x. x ∈ s ⇒ f x ≤ b
[NSUM_POS_LT] Theorem
⊢ ∀f s. FINITE s ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒ 0 < nsum s f
[NSUM_POS_LT_ALL] Theorem
⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < nsum s f
[NSUM_RESTRICT] Theorem
⊢ ∀f s. FINITE s ⇒ nsum s (λx. if x ∈ s then f x else 0) = nsum s f
[NSUM_RESTRICT_SET] Theorem
⊢ ∀P s f.
nsum {x | x ∈ s ∧ P x} f = nsum s (λx. if P x then f x else 0)
[NSUM_RMUL] Theorem
⊢ ∀f c s. nsum s (λx. f x * c) = nsum s f * c
[NSUM_SING] Theorem
⊢ ∀f x. nsum {x} f = f x
[NSUM_SING_NUMSEG] Theorem
⊢ ∀f n. nsum {n .. n} f = f n
[NSUM_SUBSET] Theorem
⊢ ∀u v f.
FINITE u ∧ FINITE v ∧ (∀x. x ∈ u DIFF v ⇒ f x = 0) ⇒
nsum u f ≤ nsum v f
[NSUM_SUBSET_SIMPLE] Theorem
⊢ ∀u v f. FINITE v ∧ u ⊆ v ⇒ nsum u f ≤ nsum v f
[NSUM_SUPERSET] Theorem
⊢ ∀f u v. u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒ nsum v f = nsum u f
[NSUM_SUPPORT] Theorem
⊢ ∀f s. nsum (support $+ f s) f = nsum s f
[NSUM_SWAP] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ⇒
nsum s (λi. nsum t (f i)) = nsum t (λj. nsum s (λi. f i j))
[NSUM_SWAP_NUMSEG] Theorem
⊢ ∀a b c d f.
nsum {a .. b} (λi. nsum {c .. d} (f i)) =
nsum {c .. d} (λj. nsum {a .. b} (λi. f i j))
[NSUM_TRIV_NUMSEG] Theorem
⊢ ∀f m n. n < m ⇒ nsum {m .. n} f = 0
[NSUM_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
nsum (s ∪ t) f = nsum s f + nsum t f
[NSUM_UNION_EQ] Theorem
⊢ ∀s t u.
FINITE u ∧ s ∩ t = ∅ ∧ s ∪ t = u ⇒ nsum s f + nsum t f = nsum u f
[NSUM_UNION_LZERO] Theorem
⊢ ∀f u v.
FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ f x = 0) ⇒
nsum (u ∪ v) f = nsum v f
[NSUM_UNION_NONZERO] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ f x = 0) ⇒
nsum (s ∪ t) f = nsum s f + nsum t f
[NSUM_UNION_RZERO] Theorem
⊢ ∀f u v.
FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒
nsum (u ∪ v) f = nsum u f
[NUMSEG_ADD_SPLIT] Theorem
⊢ ∀m n p. m ≤ n + 1 ⇒ {m .. n + p} = {m .. n} ∪ {n + 1 .. n + p}
[NUMSEG_CLAUSES] Theorem
⊢ (∀m. {m .. 0} = if m = 0 then {0} else ∅) ∧
∀m n.
{m .. SUC n} =
if m ≤ SUC n then SUC n INSERT {m .. n} else {m .. n}
[NUMSEG_COMBINE_L] Theorem
⊢ ∀m p n. m ≤ p ∧ p ≤ n + 1 ⇒ {m .. p − 1} ∪ {p .. n} = {m .. n}
[NUMSEG_COMBINE_R] Theorem
⊢ ∀m p n. m ≤ p + 1 ∧ p ≤ n ⇒ {m .. p} ∪ {p + 1 .. n} = {m .. n}
[NUMSEG_EMPTY] Theorem
⊢ ∀m n. {m .. n} = ∅ ⇔ n < m
[NUMSEG_LE] Theorem
⊢ ∀n. {x | x ≤ n} = {0 .. n}
[NUMSEG_LREC] Theorem
⊢ ∀m n. m ≤ n ⇒ m INSERT {m + 1 .. n} = {m .. n}
[NUMSEG_LT] Theorem
⊢ ∀n. {x | x < n} = if n = 0 then ∅ else {0 .. n − 1}
[NUMSEG_OFFSET_IMAGE] Theorem
⊢ ∀m n p. {m + p .. n + p} = IMAGE (λi. i + p) {m .. n}
[NUMSEG_REC] Theorem
⊢ ∀m n. m ≤ SUC n ⇒ {m .. SUC n} = SUC n INSERT {m .. n}
[NUMSEG_RREC] Theorem
⊢ ∀m n. m ≤ n ⇒ n INSERT {m .. n − 1} = {m .. n}
[NUMSEG_SING] Theorem
⊢ ∀n. {n .. n} = {n}
[PERMUTES_IN_NUMSEG] Theorem
⊢ ∀p n i. p permutes {1 .. n} ∧ i ∈ {1 .. n} ⇒ 1 ≤ p i ∧ p i ≤ n
[POLYNOMIAL_FUNCTION_ADD] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x + q x)
[POLYNOMIAL_FUNCTION_CONST] Theorem
⊢ ∀c. polynomial_function (λx. c)
[POLYNOMIAL_FUNCTION_FINITE_ROOTS] Theorem
⊢ ∀p a. polynomial_function p ⇒ (FINITE {x | p x = a} ⇔ ¬∀x. p x = a)
[POLYNOMIAL_FUNCTION_ID] Theorem
⊢ polynomial_function (λx. x)
[POLYNOMIAL_FUNCTION_INDUCT] Theorem
⊢ ∀P. P (λx. x) ∧ (∀c. P (λx. c)) ∧
(∀p q. P p ∧ P q ⇒ P (λx. p x + q x)) ∧
(∀p q. P p ∧ P q ⇒ P (λx. p x * q x)) ⇒
∀p. polynomial_function p ⇒ P p
[POLYNOMIAL_FUNCTION_LMUL] Theorem
⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. c * p x)
[POLYNOMIAL_FUNCTION_MUL] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x * q x)
[POLYNOMIAL_FUNCTION_NEG] Theorem
⊢ ∀p. polynomial_function (λx. -p x) ⇔ polynomial_function p
[POLYNOMIAL_FUNCTION_POW] Theorem
⊢ ∀p n. polynomial_function p ⇒ polynomial_function (λx. p x pow n)
[POLYNOMIAL_FUNCTION_RMUL] Theorem
⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. p x * c)
[POLYNOMIAL_FUNCTION_SUB] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x − q x)
[POLYNOMIAL_FUNCTION_SUM] Theorem
⊢ ∀s p.
FINITE s ∧ (∀i. i ∈ s ⇒ polynomial_function (λx. p x i)) ⇒
polynomial_function (λx. sum s (p x))
[POLYNOMIAL_FUNCTION_o] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (p ∘ q)
[POWERSET_CLAUSES] Theorem
⊢ {s | s ⊆ ∅} = {∅} ∧
∀a t.
{s | s ⊆ a INSERT t} =
{s | s ⊆ t} ∪ IMAGE (λs. a INSERT s) {s | s ⊆ t}
[POW_NEG_ODD] Theorem
⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)
[POW_POS_EVEN] Theorem
⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)
[PRODUCT_ABS] Theorem
⊢ ∀f s. FINITE s ⇒ product s (λx. abs (f x)) = abs (product s f)
[PRODUCT_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
product {m .. n + p} f =
product {m .. n} f * product {n + 1 .. n + p} f
[PRODUCT_CLAUSES] Theorem
⊢ (∀f. product ∅ f = 1) ∧
∀x f s.
FINITE s ⇒
product (x INSERT s) f =
if x ∈ s then product s f else f x * product s f
[PRODUCT_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ product {m .. n} f = f m * product {m + 1 .. n} f
[PRODUCT_CLAUSES_NUMSEG] Theorem
⊢ (∀m. product {m .. 0} f = if m = 0 then f 0 else 1) ∧
∀m n.
product {m .. SUC n} f =
if m ≤ SUC n then product {m .. n} f * f (SUC n)
else product {m .. n} f
[PRODUCT_CLAUSES_RIGHT] Theorem
⊢ ∀f m n.
0 < n ∧ m ≤ n ⇒ product {m .. n} f = product {m .. n − 1} f * f n
[PRODUCT_CLOSED] Theorem
⊢ ∀P f s.
P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (product s f)
[PRODUCT_CONG] Theorem
⊢ (∀f g s.
(∀x. x ∈ s ⇒ f x = g x) ⇒ product s (λi. f i) = product s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
product {a .. b} (λi. f i) = product {a .. b} g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒
product {y | p y} (λi. f i) = product {y | p y} g
[PRODUCT_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ product s (λx. c) = c pow CARD s
[PRODUCT_CONST_NUMSEG] Theorem
⊢ ∀c m n. product {m .. n} (λx. c) = c pow (n + 1 − m)
[PRODUCT_CONST_NUMSEG_1] Theorem
⊢ ∀c n. product {1 .. n} (λx. c) = c pow n
[PRODUCT_DELETE] Theorem
⊢ ∀f s a.
FINITE s ∧ a ∈ s ⇒ f a * product (s DELETE a) f = product s f
[PRODUCT_DELTA] Theorem
⊢ ∀s a.
product s (λx. if x = a then b else 1) = if a ∈ s then b else 1
[PRODUCT_DIV] Theorem
⊢ ∀f g s.
FINITE s ⇒ product s (λx. f x / g x) = product s f / product s g
[PRODUCT_DIV_NUMSEG] Theorem
⊢ ∀f g m n.
product {m .. n} (λx. f x / g x) =
product {m .. n} f / product {m .. n} g
[PRODUCT_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ product s f = product s g
[PRODUCT_EQ_0] Theorem
⊢ ∀f s. FINITE s ⇒ (product s f = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)
[PRODUCT_EQ_0_COUNT] Theorem
⊢ ∀f n. product (count n) f = 0 ⇔ ∃i. i < n ∧ f i = 0
[PRODUCT_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. product {m .. n} f = 0 ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ f x = 0
[PRODUCT_EQ_1] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 1) ⇒ product s f = 1
[PRODUCT_EQ_1_COUNT] Theorem
⊢ ∀f n. (∀i. i < n ⇒ f i = 1) ⇒ product (count n) f = 1
[PRODUCT_EQ_1_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 1) ⇒ product {m .. n} f = 1
[PRODUCT_EQ_COUNT] Theorem
⊢ ∀f g n.
(∀i. i < n ⇒ f i = g i) ⇒
product (count n) f = product (count n) g
[PRODUCT_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
product {m .. n} f = product {m .. n} g
[PRODUCT_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
product (IMAGE f s) g = product s (g ∘ f)
[PRODUCT_INV] Theorem
⊢ ∀f s. FINITE s ⇒ product s (λx. (f x)⁻¹) = (product s f)⁻¹
[PRODUCT_LE] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒
product s f ≤ product s g
[PRODUCT_LE_1] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ 1) ⇒ product s f ≤ 1
[PRODUCT_LE_NUMSEG] Theorem
⊢ ∀f m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
product {m .. n} f ≤ product {m .. n} g
[PRODUCT_MUL] Theorem
⊢ ∀f g s.
FINITE s ⇒ product s (λx. f x * g x) = product s f * product s g
[PRODUCT_MUL_COUNT] Theorem
⊢ ∀f g n.
product (count n) (λx. f x * g x) =
product (count n) f * product (count n) g
[PRODUCT_MUL_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
product s (λx. f x * g x) = product s f * product s g
[PRODUCT_MUL_NUMSEG] Theorem
⊢ ∀f g m n.
product {m .. n} (λx. f x * g x) =
product {m .. n} f * product {m .. n} g
[PRODUCT_NEG] Theorem
⊢ ∀f s. FINITE s ⇒ product s (λi. -f i) = -1 pow CARD s * product s f
[PRODUCT_NEG_NUMSEG] Theorem
⊢ ∀f m n.
product {m .. n} (λi. -f i) =
-1 pow (n + 1 − m) * product {m .. n} f
[PRODUCT_NEG_NUMSEG_1] Theorem
⊢ ∀f n. product {1 .. n} (λi. -f i) = -1 pow n * product {1 .. n} f
[PRODUCT_OFFSET] Theorem
⊢ ∀f m p.
product {m + p .. n + p} f = product {m .. n} (λi. f (i + p))
[PRODUCT_ONE] Theorem
⊢ ∀s. product s (λn. 1) = 1
[PRODUCT_PAIR] Theorem
⊢ ∀f m n.
product {2 * m .. 2 * n + 1} f =
product {m .. n} (λi. f (2 * i) * f (2 * i + 1))
[PRODUCT_PERMUTE] Theorem
⊢ ∀f p s. p permutes s ⇒ product s f = product s (f ∘ p)
[PRODUCT_PERMUTE_COUNT] Theorem
⊢ ∀f p n.
p permutes count n ⇒
product (count n) f = product (count n) (f ∘ p)
[PRODUCT_PERMUTE_NUMSEG] Theorem
⊢ ∀f p m n.
p permutes count n DIFF count m ⇒
product (count n DIFF count m) f =
product (count n DIFF count m) (f ∘ p)
[PRODUCT_POS_LE] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ product s f
[PRODUCT_POS_LE_NUMSEG] Theorem
⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 ≤ f x) ⇒ 0 ≤ product {m .. n} f
[PRODUCT_POS_LT] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < product s f
[PRODUCT_POS_LT_NUMSEG] Theorem
⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < product {m .. n} f
[PRODUCT_SING] Theorem
⊢ ∀f x. product {x} f = f x
[PRODUCT_SING_NUMSEG] Theorem
⊢ ∀f n. product {n .. n} f = f n
[PRODUCT_SUPERSET] Theorem
⊢ ∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 1) ⇒ product v f = product u f
[PRODUCT_SUPPORT] Theorem
⊢ ∀f s. product (support $* f s) f = product s f
[PRODUCT_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
product (s ∪ t) f = product s f * product t f
[REAL_ABS_INF_LE] Theorem
⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (inf s) ≤ a
[REAL_ABS_SUP_LE] Theorem
⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (sup s) ≤ a
[REAL_ARCH_INV'] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&n)⁻¹ < x
[REAL_ARCH_INV_SUC] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ < x
[REAL_BOUNDS_LT] Theorem
⊢ ∀x k. -k < x ∧ x < k ⇔ abs x < k
[REAL_COMPLETE] Theorem
⊢ ∀P. (∃x. P x) ∧ (∃M. ∀x. P x ⇒ x ≤ M) ⇒
∃M. (∀x. P x ⇒ x ≤ M) ∧ ∀M'. (∀x. P x ⇒ x ≤ M') ⇒ M ≤ M'
[REAL_EQ_SQUARE_ABS] Theorem
⊢ ∀x y. abs x = abs y ⇔ x² = y²
[REAL_HALF] Theorem
⊢ (∀e. 0 < e / 2 ⇔ 0 < e) ∧ (∀e. e / 2 + e / 2 = e) ∧
∀e. 2 * (e / 2) = e
[REAL_IMP_LE_SUP'] Theorem
⊢ ∀p x. (∃z. ∀r. r ∈ p ⇒ r ≤ z) ∧ (∃r. r ∈ p ∧ x ≤ r) ⇒ x ≤ sup p
[REAL_IMP_SUP_LE'] Theorem
⊢ ∀p x. (∃r. r ∈ p) ∧ (∀r. r ∈ p ⇒ r ≤ x) ⇒ sup p ≤ x
[REAL_INF_ASCLOSE] Theorem
⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (inf s − l) ≤ e
[REAL_INF_BOUNDS] Theorem
⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ inf s ∧ inf s ≤ b
[REAL_INF_LE'] Theorem
⊢ ∀p x.
(∃y. y ∈ p) ∧ (∃y. ∀z. z ∈ p ⇒ y ≤ z) ⇒
(inf p ≤ x ⇔ ∀y. (∀z. z ∈ p ⇒ y ≤ z) ⇒ y ≤ x)
[REAL_INF_LE_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s ≤ a ⇔ ∃x. x ∈ s ∧ x ≤ a)
[REAL_INF_LT_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s < a ⇔ ∃x. x ∈ s ∧ x < a)
[REAL_INF_UNIQUE] Theorem
⊢ ∀s b.
(∀x. x ∈ s ⇒ b ≤ x) ∧ (∀b'. b < b' ⇒ ∃x. x ∈ s ∧ x < b') ⇒
inf s = b
[REAL_LE_BETWEEN] Theorem
⊢ ∀a b. a ≤ b ⇔ ∃x. a ≤ x ∧ x ≤ b
[REAL_LE_INF] Theorem
⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s
[REAL_LE_INF_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ inf s ⇔ ∀x. x ∈ s ⇒ a ≤ x)
[REAL_LE_INF_SUBSET] Theorem
⊢ ∀s t. t ≠ ∅ ∧ t ⊆ s ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒ inf s ≤ inf t
[REAL_LE_LDIV_CANCEL] Theorem
⊢ ∀x y z. 0 < x ∧ 0 < y ∧ 0 < z ⇒ (z / x ≤ z / y ⇔ y ≤ x)
[REAL_LE_LT_MUL] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y
[REAL_LE_MUL'] Theorem
⊢ ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ 0 ≤ x * y
[REAL_LE_MUL_EPSILON] Theorem
⊢ ∀x y. (∀z. 0 < z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y
[REAL_LE_RDIV_EQ_NEG] Theorem
⊢ ∀x y z. z < 0 ⇒ (y / z ≤ x ⇔ x * z ≤ y)
[REAL_LE_SQUARE_ABS] Theorem
⊢ ∀x y. abs x ≤ abs y ⇔ x² ≤ y²
[REAL_LE_SUP'] Theorem
⊢ ∀s a b y. y ∈ s ∧ a ≤ y ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ sup s
[REAL_LE_SUP_EQ] Theorem
⊢ ∀p x.
(∃y. y ∈ p) ∧ (∃y. ∀z. z ∈ p ⇒ z ≤ y) ⇒
(x ≤ sup p ⇔ ∀y. (∀z. z ∈ p ⇒ z ≤ y) ⇒ x ≤ y)
[REAL_LE_SUP_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ sup s ⇔ ∃x. x ∈ s ∧ a ≤ x)
[REAL_LT_BETWEEN] Theorem
⊢ ∀a b. a < b ⇔ ∃x. a < x ∧ x < b
[REAL_LT_INF_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < inf s ⇔ ∀x. x ∈ s ⇒ a < x)
[REAL_LT_INV2] Theorem
⊢ ∀x y. 0 < x ∧ x < y ⇒ y⁻¹ < x⁻¹
[REAL_LT_LCANCEL_IMP] Theorem
⊢ ∀x y z. 0 < x ∧ x * y < x * z ⇒ y < z
[REAL_LT_LDIV_CANCEL] Theorem
⊢ ∀x y z. 0 < x ∧ 0 < y ∧ 0 < z ⇒ (z / x < z / y ⇔ y < x)
[REAL_LT_LE_MUL] Theorem
⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y
[REAL_LT_LMUL'] Theorem
⊢ ∀x y z. x < 0 ⇒ (x * y < x * z ⇔ z < y)
[REAL_LT_LMUL_0_NEG] Theorem
⊢ ∀x y. 0 < x * y ∧ x < 0 ⇒ y < 0
[REAL_LT_LMUL_NEG_0] Theorem
⊢ ∀x y. x * y < 0 ∧ 0 < x ⇒ y < 0
[REAL_LT_LMUL_NEG_0_NEG] Theorem
⊢ ∀x y. x * y < 0 ∧ x < 0 ⇒ 0 < y
[REAL_LT_MAX_BETWEEN] Theorem
⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d
[REAL_LT_MUL'] Theorem
⊢ ∀x y. x < 0 ∧ y < 0 ⇒ 0 < x * y
[REAL_LT_POW2] Theorem
⊢ ∀n. 0 < 2 pow n
[REAL_LT_RDIV_EQ_NEG] Theorem
⊢ ∀x y z. z < 0 ⇒ (y / z < x ⇔ x * z < y)
[REAL_LT_RMUL'] Theorem
⊢ ∀x y z. z < 0 ⇒ (x * z < y * z ⇔ y < x)
[REAL_LT_RMUL_0_NEG] Theorem
⊢ ∀x y. 0 < x * y ∧ y < 0 ⇒ x < 0
[REAL_LT_RMUL_NEG_0] Theorem
⊢ ∀x y. x * y < 0 ∧ 0 < y ⇒ x < 0
[REAL_LT_RMUL_NEG_0_NEG] Theorem
⊢ ∀x y. x * y < 0 ∧ y < 0 ⇒ 0 < x
[REAL_LT_SUP_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < sup s ⇔ ∃x. x ∈ s ∧ a < x)
[REAL_MAX_REDUCE] Theorem
⊢ ∀x y. x ≤ y ∨ x < y ⇒ max x y = y ∧ max y x = y
[REAL_MIN_LE_BETWEEN] Theorem
⊢ ∀x a c. min a c ≤ x ∧ x < a ⇒ c ≤ x
[REAL_MIN_REDUCE] Theorem
⊢ ∀x y. x ≤ y ∨ x < y ⇒ min x y = x ∧ min y x = x
[REAL_MUL_IDEMPOT] Theorem
⊢ ∀r. r * r = r ⇔ r = 0 ∨ r = 1
[REAL_MUL_SUM] Theorem
⊢ ∀s t f g.
FINITE s ∧ FINITE t ⇒
sum s f * sum t g = sum s (λi. sum t (λj. f i * g j))
[REAL_MUL_SUM_NUMSEG] Theorem
⊢ ∀f g m n p q.
sum {m .. n} f * sum {p .. q} g =
sum {m .. n} (λi. sum {p .. q} (λj. f i * g j))
[REAL_NEG_NZ] Theorem
⊢ ∀x. x < 0 ⇒ x ≠ 0
[REAL_OF_NUM_GE] Theorem
⊢ ∀m n. &m ≥ &n ⇔ m ≥ n
[REAL_OF_NUM_NPRODUCT] Theorem
⊢ ∀f s. FINITE s ⇒ &nproduct s f = product s (λx. &f x)
[REAL_OF_NUM_SUM] Theorem
⊢ ∀f s. FINITE s ⇒ &nsum s f = sum s (λx. &f x)
[REAL_OF_NUM_SUM_NUMSEG] Theorem
⊢ ∀f m n. &nsum {m .. n} f = sum {m .. n} (λi. &f i)
[REAL_POLYFUN_EQ_0] Theorem
⊢ ∀n c.
(∀x. sum {0 .. n} (λi. c i * x pow i) = 0) ⇔
∀i. i ∈ {0 .. n} ⇒ c i = 0
[REAL_POLYFUN_EQ_CONST] Theorem
⊢ ∀n c k.
(∀x. sum {0 .. n} (λi. c i * x pow i) = k) ⇔
c 0 = k ∧ ∀i. i ∈ {1 .. n} ⇒ c i = 0
[REAL_POLYFUN_FINITE_ROOTS] Theorem
⊢ ∀n c.
FINITE {x | sum {0 .. n} (λi. c i * x pow i) = 0} ⇔
∃i. i ∈ {0 .. n} ∧ c i ≠ 0
[REAL_POLYFUN_ROOTBOUND] Theorem
⊢ ∀n c.
¬(∀i. i ∈ {0 .. n} ⇒ c i = 0) ⇒
FINITE {x | sum {0 .. n} (λi. c i * x pow i) = 0} ∧
CARD {x | sum {0 .. n} (λi. c i * x pow i) = 0} ≤ n
[REAL_SUB_POLYFUN] Theorem
⊢ ∀a x y n.
1 ≤ n ⇒
sum {0 .. n} (λi. a i * x pow i) −
sum {0 .. n} (λi. a i * y pow i) =
(x − y) *
sum {0 .. n − 1}
(λj. sum {j + 1 .. n} (λi. a i * y pow (i − j − 1)) * x pow j)
[REAL_SUB_POLYFUN_ALT] Theorem
⊢ ∀a x y n.
1 ≤ n ⇒
sum {0 .. n} (λi. a i * x pow i) −
sum {0 .. n} (λi. a i * y pow i) =
(x − y) *
sum {0 .. n − 1}
(λj.
sum {0 .. n − j − 1} (λk. a (j + k + 1) * y pow k) *
x pow j)
[REAL_SUB_POW] Theorem
⊢ ∀x y n.
1 ≤ n ⇒
x pow n − y pow n =
(x − y) * sum {0 .. n − 1} (λi. x pow i * y pow (n − 1 − i))
[REAL_SUB_POW_L1] Theorem
⊢ ∀x n.
1 ≤ n ⇒ 1 − x pow n = (1 − x) * sum {0 .. n − 1} (λi. x pow i)
[REAL_SUB_POW_R1] Theorem
⊢ ∀x n.
1 ≤ n ⇒ x pow n − 1 = (x − 1) * sum {0 .. n − 1} (λi. x pow i)
[REAL_SUP_ASCLOSE] Theorem
⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (sup s − l) ≤ e
[REAL_SUP_BOUNDS] Theorem
⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ sup s ∧ sup s ≤ b
[REAL_SUP_EQ_INF] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃B. ∀x. x ∈ s ⇒ abs x ≤ B) ⇒
(sup s = inf s ⇔ ∃a. s = {a})
[REAL_SUP_LE'] Theorem
⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b
[REAL_SUP_LE_EQ] Theorem
⊢ ∀s y.
s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒ (sup s ≤ y ⇔ ∀x. x ∈ s ⇒ x ≤ y)
[REAL_SUP_LE_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s ≤ a ⇔ ∀x. x ∈ s ⇒ x ≤ a)
[REAL_SUP_LE_SUBSET] Theorem
⊢ ∀s t. s ≠ ∅ ∧ s ⊆ t ∧ (∃b. ∀x. x ∈ t ⇒ x ≤ b) ⇒ sup s ≤ sup t
[REAL_SUP_LE_X] Theorem
⊢ ∀P x. (∃r. P r) ∧ (∀r. P r ⇒ r ≤ x) ⇒ sup P ≤ x
[REAL_SUP_LT_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s < a ⇔ ∀x. x ∈ s ⇒ x < a)
[REAL_SUP_UNIQUE] Theorem
⊢ ∀s b.
(∀x. x ∈ s ⇒ x ≤ b) ∧ (∀b'. b' < b ⇒ ∃x. x ∈ s ∧ b' < x) ⇒
sup s = b
[REAL_WLOG_LE] Theorem
⊢ (∀x y. P x y ⇔ P y x) ∧ (∀x y. x ≤ y ⇒ P x y) ⇒ ∀x y. P x y
[REAL_WLOG_LT] Theorem
⊢ (∀x. P x x) ∧ (∀x y. P x y ⇔ P y x) ∧ (∀x y. x < y ⇒ P x y) ⇒
∀x y. P x y
[REAL_X_LE_SUP] Theorem
⊢ ∀P x.
(∃r. P r) ∧ (∃z. ∀r. P r ⇒ r ≤ z) ∧ (∃r. P r ∧ x ≤ r) ⇒ x ≤ sup P
[SET_PROVE_CASES] Theorem
⊢ ∀P. P ∅ ∧ (∀a s. a ∉ s ⇒ P (a INSERT s)) ⇒ ∀s. P s
[SET_RECURSION_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
∃g. g ∅ = b ∧
∀x s.
FINITE s ⇒
g (x INSERT s) = if x ∈ s then g s else f x (g s)
[SIMPLE_IMAGE_GEN] Theorem
⊢ ∀f P. {f x | P x} = IMAGE f {x | P x}
[SUBSET_NUMSEG] Theorem
⊢ ∀m n p q. {m .. n} ⊆ {p .. q} ⇔ n < m ∨ p ≤ m ∧ n ≤ q
[SUBSET_RESTRICT] Theorem
⊢ ∀s P. {x | x ∈ s ∧ P x} ⊆ s
[SUMS_SYM] Theorem
⊢ ∀s t. {x + y | x ∈ s ∧ y ∈ t} = {y + x | y ∈ t ∧ x ∈ s}
[SUM_0'] Theorem
⊢ ∀s. sum s (λn. 0) = 0
[SUM_ABS'] Theorem
⊢ ∀f s. FINITE s ⇒ abs (sum s f) ≤ sum s (λx. abs (f x))
[SUM_ABS_BOUND] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ b) ⇒
abs (sum s f) ≤ &CARD s * b
[SUM_ABS_LE'] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
abs (sum s f) ≤ sum s g
[SUM_ABS_NUMSEG] Theorem
⊢ ∀f m n. abs (sum {m .. n} f) ≤ sum {m .. n} (λi. abs (f i))
[SUM_ABS_TRIANGLE] Theorem
⊢ ∀s f b. FINITE s ∧ sum s (λa. abs (f a)) ≤ b ⇒ abs (sum s f) ≤ b
[SUM_ADD'] Theorem
⊢ ∀f g s. FINITE s ⇒ sum s (λx. f x + g x) = sum s f + sum s g
[SUM_ADD_COUNT] Theorem
⊢ ∀f g n.
sum (count n) (λx. f x + g x) = sum (count n) f + sum (count n) g
[SUM_ADD_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 0} ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
sum s (λx. f x + g x) = sum s f + sum s g
[SUM_ADD_NUMSEG] Theorem
⊢ ∀f g m n.
sum {m .. n} (λi. f i + g i) = sum {m .. n} f + sum {m .. n} g
[SUM_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
sum {m .. n + p} f = sum {m .. n} f + sum {n + 1 .. n + p} f
[SUM_BIGUNION_NONZERO] Theorem
⊢ ∀f s.
FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t1 t2 x. t1 ∈ s ∧ t2 ∈ s ∧ t1 ≠ t2 ∧ x ∈ t1 ∧ x ∈ t2 ⇒ f x = 0) ⇒
sum (BIGUNION s) f = sum s (λt. sum t f)
[SUM_BIJECTION] Theorem
⊢ ∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ p x = y) ⇒
sum s f = sum s (f ∘ p)
[SUM_BOUND'] Theorem
⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ sum s f ≤ &CARD s * b
[SUM_BOUND_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b / &CARD s) ⇒ sum s f ≤ b
[SUM_BOUND_LT] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ∧ (∃x. x ∈ s ∧ f x < b) ⇒
sum s f < &CARD s * b
[SUM_BOUND_LT_ALL] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒ sum s f < &CARD s * b
[SUM_BOUND_LT_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b / &CARD s) ⇒ sum s f < b
[SUM_CASES] Theorem
⊢ ∀s P f g.
FINITE s ⇒
sum s (λx. if P x then f x else g x) =
sum {x | x ∈ s ∧ P x} f + sum {x | x ∈ s ∧ ¬P x} g
[SUM_CASES_1] Theorem
⊢ ∀s a.
FINITE s ∧ a ∈ s ⇒
sum s (λx. if x = a then y else f x) = sum s f + (y − f a)
[SUM_CLAUSES] Theorem
⊢ (∀f. sum ∅ f = 0) ∧
∀x f s.
FINITE s ⇒
sum (x INSERT s) f = if x ∈ s then sum s f else f x + sum s f
[SUM_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ sum {m .. n} f = f m + sum {m + 1 .. n} f
[SUM_CLAUSES_NUMSEG] Theorem
⊢ (∀m. sum {m .. 0} f = if m = 0 then f 0 else 0) ∧
∀m n.
sum {m .. SUC n} f =
if m ≤ SUC n then sum {m .. n} f + f (SUC n) else sum {m .. n} f
[SUM_CLAUSES_RIGHT] Theorem
⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ sum {m .. n} f = sum {m .. n − 1} f + f n
[SUM_CLOSED] Theorem
⊢ ∀P f s.
P 0 ∧ (∀x y. P x ∧ P y ⇒ P (x + y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (sum s f)
[SUM_COMBINE_L] Theorem
⊢ ∀f m n p.
0 < n ∧ m ≤ n ∧ n ≤ p + 1 ⇒
sum {m .. n − 1} f + sum {n .. p} f = sum {m .. p} f
[SUM_COMBINE_R] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ∧ n ≤ p ⇒
sum {m .. n} f + sum {n + 1 .. p} f = sum {m .. p} f
[SUM_CONG] Theorem
⊢ (∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ sum s (λi. f i) = sum s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
sum {a .. b} (λi. f i) = sum {a .. b} g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒ sum {y | p y} (λi. f i) = sum {y | p y} g
[SUM_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ sum s (λn. c) = &CARD s * c
[SUM_CONST_NUMSEG] Theorem
⊢ ∀c m n. sum {m .. n} (λn. c) = &(n + 1 − m) * c
[SUM_DEGENERATE] Theorem
⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ sum s f = 0
[SUM_DELETE] Theorem
⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ sum (s DELETE a) f = sum s f − f a
[SUM_DELETE_CASES] Theorem
⊢ ∀f s a.
FINITE s ⇒
sum (s DELETE a) f = if a ∈ s then sum s f − f a else sum s f
[SUM_DELTA] Theorem
⊢ ∀s a. sum s (λx. if x = a then b else 0) = if a ∈ s then b else 0
[SUM_DIFF'] Theorem
⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ sum (s DIFF t) f = sum s f − sum t f
[SUM_DIFFS'] Theorem
⊢ ∀m n.
sum {m .. n} (λk. f k − f (k + 1)) =
if m ≤ n then f m − f (n + 1) else 0
[SUM_DIFFS_ALT] Theorem
⊢ ∀m n.
sum {m .. n} (λk. f (k + 1) − f k) =
if m ≤ n then f (n + 1) − f m else 0
[SUM_EQ'] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ sum s f = sum s g
[SUM_EQ_0'] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ sum s f = 0
[SUM_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 0) ⇒ sum {m .. n} f = 0
[SUM_EQ_COUNT] Theorem
⊢ ∀f g n. (∀i. i < n ⇒ f i = g i) ⇒ sum (count n) f = sum (count n) g
[SUM_EQ_GENERAL] Theorem
⊢ ∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ h x = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ g (h x) = f x) ⇒
sum s f = sum t g
[SUM_EQ_GENERAL_INVERSES] Theorem
⊢ ∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ h (k y) = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ k (h x) = x ∧ g (h x) = f x) ⇒
sum s f = sum t g
[SUM_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒ sum {m .. n} f = sum {m .. n} g
[SUM_EQ_SUPERSET] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ s ∧ (∀x. x ∈ t ⇒ f x = g x) ∧
(∀x. x ∈ s ∧ x ∉ t ⇒ f x = 0) ⇒
sum s f = sum t g
[SUM_GP] Theorem
⊢ ∀x m n.
sum {m .. n} (λi. x pow i) =
if n < m then 0
else if x = 1 then &(n + 1 − m)
else (x pow m − x pow SUC n) / (1 − x)
[SUM_GP_BASIC] Theorem
⊢ ∀x n. (1 − x) * sum {0 .. n} (λi. x pow i) = 1 − x pow SUC n
[SUM_GP_MULTIPLIED] Theorem
⊢ ∀x m n.
m ≤ n ⇒
(1 − x) * sum {m .. n} (λi. x pow i) = x pow m − x pow SUC n
[SUM_GROUP'] Theorem
⊢ ∀f g s t.
FINITE s ∧ IMAGE f s ⊆ t ⇒
sum t (λy. sum {x | x ∈ s ∧ f x = y} g) = sum s g
[SUM_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
sum (IMAGE f s) g = sum s (g ∘ f)
[SUM_IMAGE_GEN] Theorem
⊢ ∀f g s.
FINITE s ⇒
sum s g = sum (IMAGE f s) (λy. sum {x | x ∈ s ∧ f x = y} g)
[SUM_IMAGE_LE] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ g (f x)) ⇒
sum (IMAGE f s) g ≤ sum s (g ∘ f)
[SUM_IMAGE_NONZERO] Theorem
⊢ ∀d i s.
FINITE s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ i x = i y ⇒ d (i x) = 0) ⇒
sum (IMAGE i s) d = sum s (d ∘ i)
[SUM_INCL_EXCL] Theorem
⊢ ∀s t f.
FINITE s ∧ FINITE t ⇒
sum s f + sum t f = sum (s ∪ t) f + sum (s ∩ t) f
[SUM_INJECTION] Theorem
⊢ ∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y) ⇒
sum s (f ∘ p) = sum s f
[SUM_LE'] Theorem
⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ sum s f ≤ sum s g
[SUM_LE_INCLUDED] Theorem
⊢ ∀f g s t i.
FINITE s ∧ FINITE t ∧ (∀y. y ∈ t ⇒ 0 ≤ g y) ∧
(∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ i y = x ∧ f x ≤ g y) ⇒
sum s f ≤ sum t g
[SUM_LE_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒ sum {m .. n} f ≤ sum {m .. n} g
[SUM_LMUL] Theorem
⊢ ∀f c s. sum s (λx. c * f x) = c * sum s f
[SUM_LT'] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
sum s f < sum s g
[SUM_LT_ALL] Theorem
⊢ ∀f g s.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒ sum s f < sum s g
[SUM_MULTICOUNT] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k) ⇒
sum s (λi. &CARD (equiv_class R t i)) = &(k * CARD t)
[SUM_MULTICOUNT_GEN] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧
(∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k j) ⇒
sum s (λi. &CARD (equiv_class R t i)) = sum t (λi. &k i)
[SUM_NEG'] Theorem
⊢ ∀f s. sum s (λx. -f x) = -sum s f
[SUM_OFFSET'] Theorem
⊢ ∀p f m n. sum {m + p .. n + p} f = sum {m .. n} (λi. f (i + p))
[SUM_OFFSET_0] Theorem
⊢ ∀f m n. m ≤ n ⇒ sum {m .. n} f = sum {0 .. n − m} (λi. f (i + m))
[SUM_PAIR] Theorem
⊢ ∀f m n.
sum {2 * m .. 2 * n + 1} f =
sum {m .. n} (λi. f (2 * i) + f (2 * i + 1))
[SUM_PARTIAL_PRE] Theorem
⊢ ∀f g m n.
sum {m .. n} (λk. f k * (g k − g (k − 1))) =
if m ≤ n then
f (n + 1) * g n − f m * g (m − 1) −
sum {m .. n} (λk. g k * (f (k + 1) − f k))
else 0
[SUM_PARTIAL_SUC] Theorem
⊢ ∀f g m n.
sum {m .. n} (λk. f k * (g (k + 1) − g k)) =
if m ≤ n then
f (n + 1) * g (n + 1) − f m * g m −
sum {m .. n} (λk. g (k + 1) * (f (k + 1) − f k))
else 0
[SUM_PERMUTATIONS_COMPOSE_L] Theorem
⊢ ∀f s q.
q permutes s ⇒
sum {p | p permutes s} f = sum {p | p permutes s} (λp. f (q ∘ p))
[SUM_PERMUTATIONS_COMPOSE_L_COUNT] Theorem
⊢ ∀f n q.
q permutes count n ⇒
sum {p | p permutes count n} f =
sum {p | p permutes count n} (λp. f (q ∘ p))
[SUM_PERMUTATIONS_COMPOSE_L_NUMSEG] Theorem
⊢ ∀f m n q.
q permutes count n DIFF count m ⇒
sum {p | p permutes count n DIFF count m} f =
sum {p | p permutes count n DIFF count m} (λp. f (q ∘ p))
[SUM_PERMUTATIONS_COMPOSE_R] Theorem
⊢ ∀f s q.
q permutes s ⇒
sum {p | p permutes s} f = sum {p | p permutes s} (λp. f (p ∘ q))
[SUM_PERMUTATIONS_COMPOSE_R_COUNT] Theorem
⊢ ∀f n q.
q permutes count n ⇒
sum {p | p permutes count n} f =
sum {p | p permutes count n} (λp. f (p ∘ q))
[SUM_PERMUTATIONS_COMPOSE_R_NUMSEG] Theorem
⊢ ∀f m n q.
q permutes count n DIFF count m ⇒
sum {p | p permutes count n DIFF count m} f =
sum {p | p permutes count n DIFF count m} (λp. f (p ∘ q))
[SUM_PERMUTATIONS_INVERSE] Theorem
⊢ ∀f n.
sum {p | p permutes count n} f =
sum {p | p permutes count n} (λp. f (inverse p))
[SUM_PERMUTE] Theorem
⊢ ∀f p s. p permutes s ⇒ sum s f = sum s (f ∘ p)
[SUM_PERMUTE_COUNT] Theorem
⊢ ∀f p n.
p permutes count n ⇒ sum (count n) f = sum (count n) (f ∘ p)
[SUM_PERMUTE_NUMSEG] Theorem
⊢ ∀f p m n.
p permutes count n DIFF count m ⇒
sum (count n DIFF count m) f = sum (count n DIFF count m) (f ∘ p)
[SUM_POS_BOUND] Theorem
⊢ ∀f b s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ sum s f ≤ b ⇒
∀x. x ∈ s ⇒ f x ≤ b
[SUM_POS_EQ_0] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ sum s f = 0 ⇒
∀x. x ∈ s ⇒ f x = 0
[SUM_POS_EQ_0_NUMSEG] Theorem
⊢ ∀f m n.
(∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ∧ sum {m .. n} f = 0 ⇒
∀p. m ≤ p ∧ p ≤ n ⇒ f p = 0
[SUM_POS_LE] Theorem
⊢ ∀s. (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ sum s f
[SUM_POS_LE_NUMSEG] Theorem
⊢ ∀m n f. (∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ⇒ 0 ≤ sum {m .. n} f
[SUM_POS_LT] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒
0 < sum s f
[SUM_POS_LT_ALL] Theorem
⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < sum s f
[SUM_RESTRICT] Theorem
⊢ ∀f s. FINITE s ⇒ sum s (λx. if x ∈ s then f x else 0) = sum s f
[SUM_RESTRICT_SET] Theorem
⊢ ∀P s f.
sum {x | x ∈ s ∧ P x} f = sum s (λx. if P x then f x else 0)
[SUM_RMUL] Theorem
⊢ ∀f c s. sum s (λx. f x * c) = sum s f * c
[SUM_SING] Theorem
⊢ ∀f x. sum {x} f = f x
[SUM_SING_NUMSEG] Theorem
⊢ ∀f n. sum {n .. n} f = f n
[SUM_SUB'] Theorem
⊢ ∀f g s. FINITE s ⇒ sum s (λx. f x − g x) = sum s f − sum s g
[SUM_SUBSET] Theorem
⊢ ∀u v f.
FINITE u ∧ FINITE v ∧ (∀x. x ∈ u DIFF v ⇒ f x ≤ 0) ∧
(∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒
sum u f ≤ sum v f
[SUM_SUBSET_SIMPLE] Theorem
⊢ ∀u v f.
FINITE v ∧ u ⊆ v ∧ (∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒
sum u f ≤ sum v f
[SUM_SUB_NUMSEG] Theorem
⊢ ∀f g m n.
sum {m .. n} (λi. f i − g i) = sum {m .. n} f − sum {m .. n} g
[SUM_SUM_PRODUCT] Theorem
⊢ ∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
sum s (λi. sum (t i) (x i)) =
sum {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j)
[SUM_SUM_RESTRICT] Theorem
⊢ ∀R f s t.
FINITE s ∧ FINITE t ⇒
sum s (λx. sum (equiv_class R t x) (λy. f x y)) =
sum t (λy. sum {x | x ∈ s ∧ R x y} (λx. f x y))
[SUM_SUPERSET] Theorem
⊢ ∀f u v. u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒ sum v f = sum u f
[SUM_SUPPORT] Theorem
⊢ ∀f s. sum (support $+ f s) f = sum s f
[SUM_SWAP] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ⇒
sum s (λi. sum t (f i)) = sum t (λj. sum s (λi. f i j))
[SUM_SWAP_COUNT] Theorem
⊢ ∀f m n.
sum (count m) (λi. sum (count n) (f i)) =
sum (count n) (λj. sum (count m) (λi. f i j))
[SUM_SWAP_NUMSEG] Theorem
⊢ ∀a b c d f.
sum {a .. b} (λi. sum {c .. d} (f i)) =
sum {c .. d} (λj. sum {a .. b} (λi. f i j))
[SUM_TRIV_NUMSEG] Theorem
⊢ ∀f m n. n < m ⇒ sum {m .. n} f = 0
[SUM_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
sum (s ∪ t) f = sum s f + sum t f
[SUM_UNION_EQ] Theorem
⊢ ∀s t u.
FINITE u ∧ s ∩ t = ∅ ∧ s ∪ t = u ⇒ sum s f + sum t f = sum u f
[SUM_UNION_LZERO] Theorem
⊢ ∀f u v.
FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ f x = 0) ⇒
sum (u ∪ v) f = sum v f
[SUM_UNION_NONZERO] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ f x = 0) ⇒
sum (s ∪ t) f = sum s f + sum t f
[SUM_UNION_RZERO] Theorem
⊢ ∀f u v.
FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒
sum (u ∪ v) f = sum u f
[SUM_ZERO_EXISTS] Theorem
⊢ ∀u s.
FINITE s ∧ sum s u = 0 ⇒
(∀i. i ∈ s ⇒ u i = 0) ∨ ∃j k. j ∈ s ∧ u j < 0 ∧ k ∈ s ∧ u k > 0
[SUP] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒
(∀x. x ∈ s ⇒ x ≤ sup s) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b
[SUPPORT_CLAUSES] Theorem
⊢ (∀f. support op f ∅ = ∅) ∧
(∀f x s.
support op f (x INSERT s) =
if f x = neutral op then support op f s
else x INSERT support op f s) ∧
(∀f x s. support op f (s DELETE x) = support op f s DELETE x) ∧
(∀f s t. support op f (s ∪ t) = support op f s ∪ support op f t) ∧
(∀f s t. support op f (s ∩ t) = support op f s ∩ support op f t) ∧
(∀f s t.
support op f (s DIFF t) = support op f s DIFF support op f t) ∧
∀f g s. support op g (IMAGE f s) = IMAGE f (support op (g ∘ f) s)
[SUPPORT_DELTA] Theorem
⊢ ∀op s f a.
support op (λx. if x = a then f x else neutral op) s =
if a ∈ s then support op f {a} else ∅
[SUPPORT_EMPTY] Theorem
⊢ ∀op f s. (∀x. x ∈ s ⇒ f x = neutral op) ⇔ support op f s = ∅
[SUPPORT_SUBSET] Theorem
⊢ ∀op f s. support op f s ⊆ s
[SUPPORT_SUPPORT] Theorem
⊢ ∀op f s. support op f (support op f s) = support op f s
[SUP_EQ] Theorem
⊢ ∀s t. (∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇔ ∀x. x ∈ t ⇒ x ≤ b) ⇒ sup s = sup t
[SUP_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ sup s ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ sup s
[SUP_FINITE_LEMMA] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ b
[SUP_INSERT_FINITE] Theorem
⊢ ∀x s.
FINITE s ⇒ sup (x INSERT s) = if s = ∅ then x else max x (sup s)
[SUP_MONO] Theorem
⊢ ∀p q.
(∃b. ∀n. p n ≤ b) ∧ (∃c. ∀n. q n ≤ c) ∧ (∀n. p n ≤ q n) ⇒
sup (IMAGE p 𝕌(:num)) ≤ sup (IMAGE q 𝕌(:num))
[SUP_SING] Theorem
⊢ ∀a. sup {a} = a
[SUP_UNION] Theorem
⊢ ∀s t.
s ≠ ∅ ∧ t ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ∧ (∃c. ∀x. x ∈ t ⇒ x ≤ c) ⇒
sup (s ∪ t) = max (sup s) (sup t)
[SUP_UNIQUE] Theorem
⊢ ∀s b. (∀c. (∀x. x ∈ s ⇒ x ≤ c) ⇔ b ≤ c) ⇒ sup s = b
[SUP_UNIQUE_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ (sup s = a ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ a)
[TOPOLOGICAL_SORT] Theorem
⊢ ∀ $<<.
(∀x y. x << y ∧ y << x ⇒ x = y) ∧
(∀x y z. x << y ∧ y << z ⇒ x << z) ⇒
∀n s.
s HAS_SIZE n ⇒
∃f. s = IMAGE f {1 .. n} ∧
∀j k. j ∈ {1 .. n} ∧ k ∈ {1 .. n} ∧ j < k ⇒ ¬(f k << f j)
[TOPOLOGICAL_SORT'] Theorem
⊢ ∀R s n.
transitive R ∧ antisymmetric R ∧ s HAS_SIZE n ⇒
∃f. s = IMAGE f (count n) ∧
∀j k. j < n ∧ k < n ∧ j < k ⇒ ¬R (f k) (f j)
[TRANSITIVE_STEPWISE_LE] Theorem
⊢ ∀R. (∀x. R x x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
(∀n. R n (SUC n)) ⇒
∀m n. m ≤ n ⇒ R m n
[TRANSITIVE_STEPWISE_LE_EQ] Theorem
⊢ ∀R. (∀x. R x x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
((∀m n. m ≤ n ⇒ R m n) ⇔ ∀n. R n (SUC n))
[UNION_COUNT_FROM] Theorem
⊢ ∀n. count n ∪ from n = 𝕌(:num)
[UNION_FROM_COUNT] Theorem
⊢ ∀n. from n ∪ count n = 𝕌(:num)
[UPPER_BOUND_FINITE_SET] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a
[UPPER_BOUND_FINITE_SET_REAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a
[inf_alt] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
inf s =
@a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
[lifted] Theorem
⊢ lifted op NONE v0 = NONE ∧ lifted op (SOME v5) NONE = NONE ∧
lifted op (SOME x) (SOME y) = SOME (op x y)
[lifted_ind] Theorem
⊢ ∀P. (∀op v0. P op NONE v0) ∧ (∀op v5. P op (SOME v5) NONE) ∧
(∀op x y. P op (SOME x) (SOME y)) ⇒
∀v v1 v2. P v v1 v2
[real_INFINITE] Theorem
⊢ INFINITE 𝕌(:real)
[sum_real] Theorem
⊢ ∀f n. sum {0 .. n} f = sum (0,SUC n) f
[sup_alt] Theorem
⊢ sup s = @a. (∀x. x ∈ s ⇒ x ≤ a) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ b
*)
end
HOL 4, Trindemossen-1