Theory "iterate"

Parents util_prob cardinal

Signature

Constant	Type
..	:num -> num -> num -> bool
FINREC	:(α -> β -> β) -> β -> (α -> bool) -> β -> num -> bool
ITSET	:(β -> α -> α) -> (β -> bool) -> α -> α
Sum	:(α -> bool) -> (α -> real) -> real
inf	:(real -> bool) -> real
iterate	:(β -> β -> β) -> (α -> bool) -> (α -> β) -> β
monoidal	:(α -> α -> α) -> bool
neutral	:(α -> α -> α) -> α
nsum	:(α -> bool) -> (α -> num) -> num
polynomial_function	:(real -> real) -> bool
support	:(β -> β -> β) -> (α -> β) -> (α -> bool) -> α -> bool

Definitions

support

⊢ ∀op f s. support op f s = {x | x ∈ s ∧ f x ≠ neutral op}

sum_def

⊢ sum = iterate $+

polynomial_function

⊢ ∀p. polynomial_function p ⇔ ∃m c. ∀x. p x = sum (0 .. m) (λi. c i * x pow i)

numseg

⊢ ∀m n. m .. n = {x | m ≤ x ∧ x ≤ n}

nsum_def

⊢ nsum = iterate $+

neutral

⊢ ∀op. neutral op = @x. ∀y. (op x y = y) ∧ (op y x = y)

monoidal

⊢ ∀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

ITSET_def

⊢ ∀f s b.
      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

iterate

⊢ ∀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

inf

⊢ ∀s. inf s = @a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a

FINREC_def

⊢ (∀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)

Theorems

UPPER_BOUND_FINITE_SET_REAL

⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a

TOPOLOGICAL_SORT

⊢ ∀ $<<.
      (∀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)

TH

⊢ (∀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)

SUPPORT_SUPPORT

⊢ ∀op f s. support op f (support op f s) = support op f s

SUPPORT_SUBSET

⊢ ∀op f s. support op f s ⊆ s

SUPPORT_EMPTY

⊢ ∀op f s. (∀x. x ∈ s ⇒ (f x = neutral op)) ⇔ (support op f s = ∅)

SUPPORT_DELTA

⊢ ∀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_CLAUSES

⊢ (∀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)

SUP_UNIQUE_FINITE

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ((sup s = a) ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ a)

SUP_UNIQUE

⊢ ∀s b. (∀c. (∀x. x ∈ s ⇒ x ≤ c) ⇔ b ≤ c) ⇒ (sup s = b)

SUP_UNION

⊢ ∀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_SING

⊢ ∀a. sup {a} = a

SUP_INSERT_FINITE

⊢ ∀x s. FINITE s ⇒ (sup (x INSERT s) = if s = ∅ then x else max x (sup s))

SUP_FINITE_LEMMA

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ b

SUP_FINITE

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ sup s ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ sup s

SUP_EQ

⊢ ∀s t. (∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇔ ∀x. x ∈ t ⇒ x ≤ b) ⇒ (sup s = sup t)

sup_alt

⊢ sup s = @a. (∀x. x ∈ s ⇒ x ≤ a) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ b

SUP

⊢ ∀s.
      s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒
      (∀x. x ∈ s ⇒ x ≤ sup s) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b

SUM_ZERO_EXISTS

⊢ ∀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

SUM_UNION_RZERO

⊢ ∀f u v.
      FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 0)) ⇒ (sum (u ∪ v) f = sum u f)

SUM_UNION_NONZERO

⊢ ∀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_LZERO

⊢ ∀f u v.
      FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ (f x = 0)) ⇒ (sum (u ∪ v) f = sum v f)

SUM_UNION_EQ

⊢ ∀s t u. FINITE u ∧ (s ∩ t = ∅) ∧ (s ∪ t = u) ⇒ (sum s f + sum t f = sum u f)

SUM_UNION

⊢ ∀f s t.
      FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒ (sum (s ∪ t) f = sum s f + sum t f)

SUM_TRIV_NUMSEG

⊢ ∀f m n. n < m ⇒ (sum (m .. n) f = 0)

SUM_SWAP_NUMSEG

⊢ ∀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_SWAP

⊢ ∀f s t.
      FINITE s ∧ FINITE t ⇒
      (sum s (λi. sum t (f i)) = sum t (λj. sum s (λi. f i j)))

SUM_SUPPORT

⊢ ∀f s. sum (support $+ f s) f = sum s f

SUM_SUPERSET

⊢ ∀f u v. u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 0)) ⇒ (sum v f = sum u f)

SUM_SUM_RESTRICT

⊢ ∀R f s t.
      FINITE s ∧ FINITE t ⇒
      (sum s (λx. sum {y | y ∈ t ∧ R x y} (λy. f x y)) =
       sum t (λy. sum {x | x ∈ s ∧ R x y} (λx. f x y)))

SUM_SUM_PRODUCT

⊢ ∀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_SUBSET_SIMPLE

⊢ ∀u v f. FINITE v ∧ u ⊆ v ∧ (∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒ sum u f ≤ sum v f

SUM_SUBSET

⊢ ∀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_SUB_NUMSEG

⊢ ∀f g m n. sum (m .. n) (λi. f i − g i) = sum (m .. n) f − sum (m .. n) g

SUM_SUB

⊢ ∀f g s. FINITE s ⇒ (sum s (λx. f x − g x) = sum s f − sum s g)

SUM_SING_NUMSEG

⊢ ∀f n. sum (n .. n) f = f n

SUM_SING

⊢ ∀f x. sum {x} f = f x

SUM_RMUL

⊢ ∀f c s. sum s (λx. f x * c) = sum s f * c

SUM_RESTRICT_SET

⊢ ∀P s f. sum {x | x ∈ s ∧ P x} f = sum s (λx. if P x then f x else 0)

SUM_RESTRICT

⊢ ∀f s. FINITE s ⇒ (sum s (λx. if x ∈ s then f x else 0) = sum s f)

SUM_POS_LT_ALL

⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < sum s f

SUM_POS_LT

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒ 0 < sum s f

SUM_POS_LE_NUMSEG

⊢ ∀m n f. (∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ⇒ 0 ≤ sum (m .. n) f

SUM_POS_LE

⊢ ∀s. (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ sum s f

SUM_POS_EQ_0_NUMSEG

⊢ ∀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_EQ_0

⊢ ∀f s.
      FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (sum s f = 0) ⇒ ∀x. x ∈ s ⇒ (f x = 0)

SUM_POS_BOUND

⊢ ∀f b s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ sum s f ≤ b ⇒ ∀x. x ∈ s ⇒ f x ≤ b

SUM_PARTIAL_SUC

⊢ ∀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_PARTIAL_PRE

⊢ ∀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_PAIR

⊢ ∀f m n.
      sum (2 * m .. 2 * n + 1) f =
      sum (m .. n) (λi. f (2 * i) + f (2 * i + 1))

SUM_OFFSET_0

⊢ ∀f m n. m ≤ n ⇒ (sum (m .. n) f = sum (0 .. n − m) (λi. f (i + m)))

SUM_OFFSET

⊢ ∀p f m n. sum (m + p .. n + p) f = sum (m .. n) (λi. f (i + p))

SUM_NEG

⊢ ∀f s. sum s (λx. -f x) = -sum s f

SUM_MULTICOUNT_GEN

⊢ ∀R s t k.
      FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ (CARD {i | i ∈ s ∧ R i j} = k j)) ⇒
      (sum s (λi. &CARD {j | j ∈ t ∧ R i j}) = sum t (λi. &k i))

SUM_MULTICOUNT

⊢ ∀R s t k.
      FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ (CARD {i | i ∈ s ∧ R i j} = k)) ⇒
      (sum s (λi. &CARD {j | j ∈ t ∧ R i j}) = &(k * CARD t))

SUM_LT_ALL

⊢ ∀f g s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒ sum s f < sum s g

SUM_LT

⊢ ∀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_LMUL

⊢ ∀f c s. sum s (λx. c * f x) = c * sum s f

SUM_LE_NUMSEG

⊢ ∀f g m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒ sum (m .. n) f ≤ sum (m .. n) g

SUM_LE_INCLUDED

⊢ ∀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

⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ sum s f ≤ sum s g

SUM_INJECTION

⊢ ∀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_INCL_EXCL

⊢ ∀s t f.
      FINITE s ∧ FINITE t ⇒
      (sum s f + sum t f = sum (s ∪ t) f + sum (s ∩ t) f)

SUM_IMAGE_NONZERO

⊢ ∀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_IMAGE_LE

⊢ ∀f g s.
      FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ g (f x)) ⇒ sum (IMAGE f s) g ≤ sum s (g ∘ f)

SUM_IMAGE_GEN

⊢ ∀f g s.
      FINITE s ⇒
      (sum s g = sum (IMAGE f s) (λy. sum {x | x ∈ s ∧ (f x = y)} g))

SUM_IMAGE

⊢ ∀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_GROUP

⊢ ∀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_EQ_SUPERSET

⊢ ∀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_EQ_NUMSEG

⊢ ∀f g m n.
      (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = g i)) ⇒ (sum (m .. n) f = sum (m .. n) g)

SUM_EQ_GENERAL_INVERSES

⊢ ∀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_GENERAL

⊢ ∀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_0_NUMSEG

⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = 0)) ⇒ (sum (m .. n) f = 0)

SUM_EQ_0

⊢ ∀f s. (∀x. x ∈ s ⇒ (f x = 0)) ⇒ (sum s f = 0)

SUM_EQ

⊢ ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (sum s f = sum s g)

SUM_DIFFS_ALT

⊢ ∀m n.
      sum (m .. n) (λk. f (k + 1) − f k) =
      if m ≤ n then f (n + 1) − f m else 0

SUM_DIFFS

⊢ ∀m n.
      sum (m .. n) (λk. f k − f (k + 1)) =
      if m ≤ n then f m − f (n + 1) else 0

SUM_DIFF

⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ (sum (s DIFF t) f = sum s f − sum t f)

SUM_DELTA

⊢ ∀s a. sum s (λx. if x = a then b else 0) = if a ∈ s then b else 0

SUM_DELETE_CASES

⊢ ∀f s a.
      FINITE s ⇒
      (sum (s DELETE a) f = if a ∈ s then sum s f − f a else sum s f)

SUM_DELETE

⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ (sum (s DELETE a) f = sum s f − f a)

SUM_DEGENERATE

⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ (sum s f = 0)

SUM_CONST_NUMSEG

⊢ ∀c m n. sum (m .. n) (λn. c) = &(n + 1 − m) * c

SUM_CONST

⊢ ∀c s. FINITE s ⇒ (sum s (λn. c) = &CARD s * c)

SUM_COMBINE_R

⊢ ∀f m n p.
      m ≤ n + 1 ∧ n ≤ p ⇒
      (sum (m .. n) f + sum (n + 1 .. p) f = sum (m .. p) f)

SUM_COMBINE_L

⊢ ∀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_CLOSED

⊢ ∀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_CLAUSES_RIGHT

⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ (sum (m .. n) f = sum (m .. n − 1) f + f n)

SUM_CLAUSES_NUMSEG

⊢ (∀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_LEFT

⊢ ∀f m n. m ≤ n ⇒ (sum (m .. n) f = f m + sum (m + 1 .. n) f)

SUM_CLAUSES

⊢ (∀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_CASES_1

⊢ ∀s a.
      FINITE s ∧ a ∈ s ⇒
      (sum s (λx. if x = a then y else f x) = sum s f + (y − f a))

SUM_CASES

⊢ ∀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_BOUND_LT_GEN

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b / &CARD s) ⇒ sum s f < b

SUM_BOUND_LT_ALL

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒ sum s f < &CARD s * b

SUM_BOUND_LT

⊢ ∀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_GEN

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b / &CARD s) ⇒ sum s f ≤ b

SUM_BOUND

⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ sum s f ≤ &CARD s * b

SUM_BIJECTION

⊢ ∀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_BIGUNION_NONZERO

⊢ ∀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_ADD_SPLIT

⊢ ∀f m n p.
      m ≤ n + 1 ⇒
      (sum (m .. n + p) f = sum (m .. n) f + sum (n + 1 .. n + p) f)

SUM_ADD_NUMSEG

⊢ ∀f g m n. sum (m .. n) (λi. f i + g i) = sum (m .. n) f + sum (m .. n) g

SUM_ADD_GEN

⊢ ∀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

⊢ ∀f g s. FINITE s ⇒ (sum s (λx. f x + g x) = sum s f + sum s g)

SUM_ABS_NUMSEG

⊢ ∀f m n. abs (sum (m .. n) f) ≤ sum (m .. n) (λi. abs (f i))

SUM_ABS_LE

⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒ abs (sum s f) ≤ sum s g

SUM_ABS_BOUND

⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ b) ⇒ abs (sum s f) ≤ &CARD s * b

SUM_ABS

⊢ ∀f s. FINITE s ⇒ abs (sum s f) ≤ sum s (λx. abs (f x))

SUM_0

⊢ ∀s. sum s (λn. 0) = 0

SUBSET_RESTRICT

⊢ ∀s P. {x | x ∈ s ∧ P x} ⊆ s

SUBSET_NUMSEG

⊢ ∀m n p q. (m .. n) ⊆ (p .. q) ⇔ n < m ∨ p ≤ m ∧ n ≤ q

SIMP_REAL_ARCH

⊢ ∀x. ∃n. x ≤ &n

SET_RECURSION_LEMMA

⊢ ∀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))

SET_PROVE_CASES

⊢ ∀P. P ∅ ∧ (∀a s. a ∉ s ⇒ P (a INSERT s)) ⇒ ∀s. P s

REAL_WLOG_LT

⊢ (∀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_SUP_UNIQUE

⊢ ∀s b. (∀x. x ∈ s ⇒ x ≤ b) ∧ (∀b'. b' < b ⇒ ∃x. x ∈ s ∧ b' < x) ⇒ (sup s = b)

REAL_SUP_LT_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s < a ⇔ ∀x. x ∈ s ⇒ x < a)

REAL_SUP_LE_SUBSET

⊢ ∀s t. s ≠ ∅ ∧ s ⊆ t ∧ (∃b. ∀x. x ∈ t ⇒ x ≤ b) ⇒ sup s ≤ sup t

REAL_SUP_LE_S

⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b

REAL_SUP_LE_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s ≤ a ⇔ ∀x. x ∈ s ⇒ x ≤ a)

REAL_SUP_LE_EQ

⊢ ∀s y. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒ (sup s ≤ y ⇔ ∀x. x ∈ s ⇒ x ≤ y)

REAL_SUP_EQ_INF

⊢ ∀s. s ≠ ∅ ∧ (∃B. ∀x. x ∈ s ⇒ abs x ≤ B) ⇒ ((sup s = inf s) ⇔ ∃a. s = {a})

REAL_SUP_BOUNDS

⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ sup s ∧ sup s ≤ b

REAL_SUP_ASCLOSE

⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (sup s − l) ≤ e

REAL_SUB_POW_R1

⊢ ∀x n. 1 ≤ n ⇒ (x pow n − 1 = (x − 1) * sum (0 .. n − 1) (λi. x pow i))

REAL_SUB_POW_L1

⊢ ∀x n. 1 ≤ n ⇒ (1 − x pow n = (1 − x) * sum (0 .. n − 1) (λi. x pow i))

REAL_SUB_POW

⊢ ∀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_POLYFUN_ALT

⊢ ∀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_POLYFUN

⊢ ∀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_POLYFUN_ROOTBOUND

⊢ ∀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_POLYFUN_FINITE_ROOTS

⊢ ∀n c.
      FINITE {x | sum (0 .. n) (λi. c i * x pow i) = 0} ⇔
      ∃i. i ∈ (0 .. n) ∧ c i ≠ 0

REAL_POLYFUN_EQ_CONST

⊢ ∀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_EQ_0

⊢ ∀n c.
      (∀x. sum (0 .. n) (λi. c i * x pow i) = 0) ⇔
      ∀i. i ∈ (0 .. n) ⇒ (c i = 0)

REAL_OF_NUM_SUM_NUMSEG

⊢ ∀f m n. &nsum (m .. n) f = sum (m .. n) (λi. &f i)

REAL_OF_NUM_SUM

⊢ ∀f s. FINITE s ⇒ (&nsum s f = sum s (λx. &f x))

REAL_LT_SUP_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < sup s ⇔ ∃x. x ∈ s ∧ a < x)

REAL_LT_INF_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < inf s ⇔ ∀x. x ∈ s ⇒ a < x)

REAL_LT_BETWEEN

⊢ ∀a b. a < b ⇔ ∃x. a < x ∧ x < b

REAL_LE_SUP_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ sup s ⇔ ∃x. x ∈ s ∧ a ≤ x)

REAL_LE_SUP

⊢ ∀s a b y. y ∈ s ∧ a ≤ y ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ sup s

REAL_LE_INF_SUBSET

⊢ ∀s t. t ≠ ∅ ∧ t ⊆ s ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒ inf s ≤ inf t

REAL_LE_INF_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ inf s ⇔ ∀x. x ∈ s ⇒ a ≤ x)

REAL_LE_INF

⊢ ∀b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s

real_INFINITE

⊢ INFINITE 𝕌(:real)

REAL_INF_UNIQUE

⊢ ∀s b. (∀x. x ∈ s ⇒ b ≤ x) ∧ (∀b'. b < b' ⇒ ∃x. x ∈ s ∧ x < b') ⇒ (inf s = b)

REAL_INF_LT_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s < a ⇔ ∃x. x ∈ s ∧ x < a)

REAL_INF_LE_FINITE

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s ≤ a ⇔ ∃x. x ∈ s ∧ x ≤ a)

REAL_INF_BOUNDS

⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ inf s ∧ inf s ≤ b

REAL_INF_ASCLOSE

⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (inf s − l) ≤ e

REAL_COMPLETE

⊢ ∀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_ABS_SUP_LE

⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (sup s) ≤ a

REAL_ABS_INF_LE

⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (inf s) ≤ a

POLYNOMIAL_FUNCTION_SUM

⊢ ∀s p.
      FINITE s ∧ (∀i. i ∈ s ⇒ polynomial_function (λx. p x i)) ⇒
      polynomial_function (λx. sum s (p x))

POLYNOMIAL_FUNCTION_SUB

⊢ ∀p q.
      polynomial_function p ∧ polynomial_function q ⇒
      polynomial_function (λx. p x − q x)

POLYNOMIAL_FUNCTION_RMUL

⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. p x * c)

POLYNOMIAL_FUNCTION_POW

⊢ ∀p n. polynomial_function p ⇒ polynomial_function (λx. p x pow n)

POLYNOMIAL_FUNCTION_o

⊢ ∀p q.
      polynomial_function p ∧ polynomial_function q ⇒
      polynomial_function (p ∘ q)

POLYNOMIAL_FUNCTION_NEG

⊢ ∀p. polynomial_function (λx. -p x) ⇔ polynomial_function p

POLYNOMIAL_FUNCTION_MUL

⊢ ∀p q.
      polynomial_function p ∧ polynomial_function q ⇒
      polynomial_function (λx. p x * q x)

POLYNOMIAL_FUNCTION_LMUL

⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. c * p x)

POLYNOMIAL_FUNCTION_INDUCT

⊢ ∀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_ID

⊢ polynomial_function (λx. x)

POLYNOMIAL_FUNCTION_FINITE_ROOTS

⊢ ∀p a. polynomial_function p ⇒ (FINITE {x | p x = a} ⇔ ¬∀x. p x = a)

POLYNOMIAL_FUNCTION_CONST

⊢ ∀c. polynomial_function (λx. c)

POLYNOMIAL_FUNCTION_ADD

⊢ ∀p q.
      polynomial_function p ∧ polynomial_function q ⇒
      polynomial_function (λx. p x + q x)

NUMSEG_SING

⊢ ∀n. n .. n = {n}

NUMSEG_RREC

⊢ ∀m n. m ≤ n ⇒ (n INSERT (m .. n − 1) = m .. n)

NUMSEG_REC

⊢ ∀m n. m ≤ SUC n ⇒ (m .. SUC n = SUC n INSERT (m .. n))

NUMSEG_OFFSET_IMAGE

⊢ ∀m n p. m + p .. n + p = IMAGE (λi. i + p) (m .. n)

NUMSEG_LT

⊢ ∀n. {x | x < n} = if n = 0 then ∅ else 0 .. n − 1

NUMSEG_LREC

⊢ ∀m n. m ≤ n ⇒ (m INSERT (m + 1 .. n) = m .. n)

NUMSEG_LE

⊢ ∀n. {x | x ≤ n} = 0 .. n

NUMSEG_EMPTY

⊢ ∀m n. (m .. n = ∅) ⇔ n < m

NUMSEG_COMBINE_R

⊢ ∀m p n. m ≤ p + 1 ∧ p ≤ n ⇒ ((m .. p) ∪ (p + 1 .. n) = m .. n)

NUMSEG_COMBINE_L

⊢ ∀m p n. m ≤ p ∧ p ≤ n + 1 ⇒ ((m .. p − 1) ∪ (p .. n) = m .. n)

NUMSEG_CLAUSES

⊢ (∀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_ADD_SPLIT

⊢ ∀m n p. m ≤ n + 1 ⇒ (m .. n + p = (m .. n) ∪ (n + 1 .. n + p))

NSUM_UNION_RZERO

⊢ ∀f u v.
      FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 0)) ⇒ (nsum (u ∪ v) f = nsum u f)

NSUM_UNION_NONZERO

⊢ ∀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_LZERO

⊢ ∀f u v.
      FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ (f x = 0)) ⇒ (nsum (u ∪ v) f = nsum v f)

NSUM_UNION_EQ

⊢ ∀s t u.
      FINITE u ∧ (s ∩ t = ∅) ∧ (s ∪ t = u) ⇒ (nsum s f + nsum t f = nsum u f)

NSUM_UNION

⊢ ∀f s t.
      FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
      (nsum (s ∪ t) f = nsum s f + nsum t f)

NSUM_TRIV_NUMSEG

⊢ ∀f m n. n < m ⇒ (nsum (m .. n) f = 0)

NSUM_SWAP_NUMSEG

⊢ ∀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_SWAP

⊢ ∀f s t.
      FINITE s ∧ FINITE t ⇒
      (nsum s (λi. nsum t (f i)) = nsum t (λj. nsum s (λi. f i j)))

NSUM_SUPPORT

⊢ ∀f s. nsum (support $+ f s) f = nsum s f

NSUM_SUPERSET

⊢ ∀f u v. u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 0)) ⇒ (nsum v f = nsum u f)

NSUM_SUBSET_SIMPLE

⊢ ∀u v f. FINITE v ∧ u ⊆ v ⇒ nsum u f ≤ nsum v f

NSUM_SUBSET

⊢ ∀u v f.
      FINITE u ∧ FINITE v ∧ (∀x. x ∈ u DIFF v ⇒ (f x = 0)) ⇒
      nsum u f ≤ nsum v f

NSUM_SING_NUMSEG

⊢ ∀f n. nsum (n .. n) f = f n

NSUM_SING

⊢ ∀f x. nsum {x} f = f x

NSUM_RMUL

⊢ ∀f c s. nsum s (λx. f x * c) = nsum s f * c

NSUM_RESTRICT_SET

⊢ ∀P s f. nsum {x | x ∈ s ∧ P x} f = nsum s (λx. if P x then f x else 0)

NSUM_RESTRICT

⊢ ∀f s. FINITE s ⇒ (nsum s (λx. if x ∈ s then f x else 0) = nsum s f)

NSUM_POS_LT_ALL

⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < nsum s f

NSUM_POS_LT

⊢ ∀f s. FINITE s ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒ 0 < nsum s f

NSUM_POS_BOUND

⊢ ∀f b s. FINITE s ∧ nsum s f ≤ b ⇒ ∀x. x ∈ s ⇒ f x ≤ b

NSUM_PAIR

⊢ ∀f m n.
      nsum (2 * m .. 2 * n + 1) f =
      nsum (m .. n) (λi. f (2 * i) + f (2 * i + 1))

NSUM_OFFSET_0

⊢ ∀f m n. m ≤ n ⇒ (nsum (m .. n) f = nsum (0 .. n − m) (λi. f (i + m)))

NSUM_OFFSET

⊢ ∀p f m n. nsum (m + p .. n + p) f = nsum (m .. n) (λi. f (i + p))

NSUM_NSUM_RESTRICT

⊢ ∀R f s t.
      FINITE s ∧ FINITE t ⇒
      (nsum s (λx. nsum {y | y ∈ t ∧ R x y} (λy. f x y)) =
       nsum t (λy. nsum {x | x ∈ s ∧ R x y} (λx. f x y)))

NSUM_NSUM_PRODUCT

⊢ ∀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_MULTICOUNT_GEN

⊢ ∀R s t k.
      FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ (CARD {i | i ∈ s ∧ R i j} = k j)) ⇒
      (nsum s (λi. CARD {j | j ∈ t ∧ R i j}) = nsum t (λi. k i))

NSUM_MULTICOUNT

⊢ ∀R s t k.
      FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ (CARD {i | i ∈ s ∧ R i j} = k)) ⇒
      (nsum s (λi. CARD {j | j ∈ t ∧ R i j}) = k * CARD t)

NSUM_LT_ALL

⊢ ∀f g s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒ nsum s f < nsum s g

NSUM_LT

⊢ ∀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_LMUL

⊢ ∀f c s. nsum s (λx. c * f x) = c * nsum s f

NSUM_LE_NUMSEG

⊢ ∀f g m n.
      (∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒ nsum (m .. n) f ≤ nsum (m .. n) g

NSUM_LE_GEN

⊢ ∀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

⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ nsum s f ≤ nsum s g

NSUM_INJECTION

⊢ ∀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_INCL_EXCL

⊢ ∀s t f.
      FINITE s ∧ FINITE t ⇒
      (nsum s f + nsum t f = nsum (s ∪ t) f + nsum (s ∩ t) f)

NSUM_IMAGE_NONZERO

⊢ ∀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_IMAGE_GEN

⊢ ∀f g s.
      FINITE s ⇒
      (nsum s g = nsum (IMAGE f s) (λy. nsum {x | x ∈ s ∧ (f x = y)} g))

NSUM_IMAGE

⊢ ∀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_GROUP

⊢ ∀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_EQ_SUPERSET

⊢ ∀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_EQ_NUMSEG

⊢ ∀f g m n.
      (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = g i)) ⇒ (nsum (m .. n) f = nsum (m .. n) g)

NSUM_EQ_GENERAL_INVERSES

⊢ ∀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_GENERAL

⊢ ∀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_0_NUMSEG

⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = 0)) ⇒ (nsum (m .. n) f = 0)

NSUM_EQ_0_IFF_NUMSEG

⊢ ∀f m n. (nsum (m .. n) f = 0) ⇔ ∀i. m ≤ i ∧ i ≤ n ⇒ (f i = 0)

NSUM_EQ_0_IFF

⊢ ∀s. FINITE s ⇒ ((nsum s f = 0) ⇔ ∀x. x ∈ s ⇒ (f x = 0))

NSUM_EQ_0

⊢ ∀f s. (∀x. x ∈ s ⇒ (f x = 0)) ⇒ (nsum s f = 0)

NSUM_EQ

⊢ ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (nsum s f = nsum s g)

NSUM_DIFF

⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ (nsum (s DIFF t) f = nsum s f − nsum t f)

NSUM_DELTA

⊢ ∀s a. nsum s (λx. if x = a then b else 0) = if a ∈ s then b else 0

NSUM_DELETE

⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ (f a + nsum (s DELETE a) f = nsum s f)

NSUM_DEGENERATE

⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ (nsum s f = 0)

NSUM_CONST_NUMSEG

⊢ ∀c m n. nsum (m .. n) (λn. c) = (n + 1 − m) * c

NSUM_CONST

⊢ ∀c s. FINITE s ⇒ (nsum s (λn. c) = CARD s * c)

NSUM_CLOSED

⊢ ∀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_CLAUSES_RIGHT

⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ (nsum (m .. n) f = nsum (m .. n − 1) f + f n)

NSUM_CLAUSES_NUMSEG

⊢ (∀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_LEFT

⊢ ∀f m n. m ≤ n ⇒ (nsum (m .. n) f = f m + nsum (m + 1 .. n) f)

NSUM_CLAUSES

⊢ (∀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_CASES

⊢ ∀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_BOUND_LT_GEN

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b DIV CARD s) ⇒ nsum s f < b

NSUM_BOUND_LT_ALL

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒ nsum s f < CARD s * b

NSUM_BOUND_LT

⊢ ∀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_GEN

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b DIV CARD s) ⇒ nsum s f ≤ b

NSUM_BOUND

⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ nsum s f ≤ CARD s * b

NSUM_BIJECTION

⊢ ∀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_BIGUNION_NONZERO

⊢ ∀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_ADD_SPLIT

⊢ ∀f m n p.
      m ≤ n + 1 ⇒
      (nsum (m .. n + p) f = nsum (m .. n) f + nsum (n + 1 .. n + p) f)

NSUM_ADD_NUMSEG

⊢ ∀f g m n. nsum (m .. n) (λi. f i + g i) = nsum (m .. n) f + nsum (m .. n) g

NSUM_ADD_GEN

⊢ ∀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

⊢ ∀f g s. FINITE s ⇒ (nsum s (λx. f x + g x) = nsum s f + nsum s g)

NSUM_0

⊢ ∀s. nsum s (λn. 0) = 0

NEUTRAL_REAL_MUL

⊢ neutral $* = 1

NEUTRAL_REAL_ADD

⊢ neutral $+ = 0

NEUTRAL_MUL

⊢ neutral $* = 1

NEUTRAL_ADD

⊢ neutral $+ = 0

MONOIDAL_REAL_MUL

⊢ monoidal $*

MONOIDAL_REAL_ADD

⊢ monoidal $+

MONOIDAL_MUL

⊢ monoidal $*

MONOIDAL_ADD

⊢ monoidal $+

MONOIDAL_AC

⊢ ∀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)

MOD_NSUM_MOD_NUMSEG

⊢ ∀f a b n.
      n ≠ 0 ⇒ (nsum (a .. b) f MOD n = nsum (a .. b) (λi. f i MOD n) MOD n)

MOD_NSUM_MOD

⊢ ∀f n s. FINITE s ∧ n ≠ 0 ⇒ (nsum s f MOD n = nsum s (λi. f i MOD n) MOD n)

LOWER_BOUND_FINITE_SET_REAL

⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ a ≤ f x

ITERATE_UNION_NONZERO

⊢ ∀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))

ITERATE_UNION_GEN

⊢ ∀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

⊢ ∀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_SUPPORT

⊢ ∀op f s. iterate op (support op f s) f = iterate op s f

ITERATE_SUPERSET

⊢ ∀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_SING

⊢ ∀op. monoidal op ⇒ ∀f x. iterate op {x} f = f x

ITERATE_RELATED

⊢ ∀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_PAIR

⊢ ∀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_OP_GEN

⊢ ∀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_OP

⊢ ∀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_ITERATE_PRODUCT

⊢ ∀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_INJECTION

⊢ ∀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_INCL_EXCL

⊢ ∀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_IMAGE_NONZERO

⊢ ∀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_IMAGE

⊢ ∀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_EXPAND_CASES

⊢ ∀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_EQ_NEUTRAL

⊢ ∀op.
      monoidal op ⇒
      ∀f s. (∀x. x ∈ s ⇒ (f x = neutral op)) ⇒ (iterate op s f = neutral op)

ITERATE_EQ_GENERAL_INVERSES

⊢ ∀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_GENERAL

⊢ ∀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

⊢ ∀op.
      monoidal op ⇒
      ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (iterate op s f = iterate op s g)

ITERATE_DIFF_GEN

⊢ ∀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_DIFF

⊢ ∀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_DELTA

⊢ ∀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_DELETE

⊢ ∀op.
      monoidal op ⇒
      ∀f s a.
          FINITE s ∧ a ∈ s ⇒
          (op (f a) (iterate op (s DELETE a) f) = iterate op s f)

ITERATE_CLOSED

⊢ ∀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_CLAUSES_NUMSEG

⊢ ∀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_CLAUSES_GEN

⊢ ∀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

⊢ ∀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_CASES

⊢ ∀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_BIJECTION

⊢ ∀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))

INF_UNIQUE_FINITE

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ((inf s = a) ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ a ≤ y)

INF_SING

⊢ ∀a. inf {a} = a

INF_INSERT_FINITE

⊢ ∀x s. FINITE s ⇒ (inf (x INSERT s) = if s = ∅ then x else min x (inf s))

INF_FINITE_LEMMA

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ b ≤ x

INF_FINITE

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ inf s ∈ s ∧ ∀x. x ∈ s ⇒ inf s ≤ x

INF_EQ

⊢ ∀s t. (∀a. (∀x. x ∈ s ⇒ a ≤ x) ⇔ ∀x. x ∈ t ⇒ a ≤ x) ⇒ (inf s = inf t)

INF

⊢ ∀s.
      s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
      (∀x. x ∈ s ⇒ inf s ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s

IN_SUPPORT

⊢ ∀op f x s. x ∈ support op f s ⇔ x ∈ s ∧ f x ≠ neutral op

IN_NUMSEG_0

⊢ ∀m n. m ∈ (0 .. n) ⇔ m ≤ n

IN_NUMSEG

⊢ ∀m n p. p ∈ (m .. n) ⇔ m ≤ p ∧ p ≤ n

HAS_SIZE_NUMSEG_1

⊢ ∀n. (1 .. n) HAS_SIZE n

HAS_SIZE_NUMSEG

⊢ ∀m n. (m .. n) HAS_SIZE n + 1 − m

FORALL_IN_GSPEC

⊢ (∀P f. (∀z. z ∈ {f x | P x} ⇒ Q z) ⇔ ∀x. P x ⇒ Q (f x)) ∧
  (∀P f. (∀z. z ∈ {f x y | P x y} ⇒ Q z) ⇔ ∀x y. P x y ⇒ Q (f x y)) ∧
  ∀P f. (∀z. z ∈ {f w x y | P w x y} ⇒ Q z) ⇔ ∀w x y. P w x y ⇒ Q (f w x y)

FINREC_UNIQUE_LEMMA

⊢ ∀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_SUC_LEMMA

⊢ ∀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_FUN_LEMMA

⊢ ∀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_FUN

⊢ ∀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_EXISTS_LEMMA

⊢ ∀f b s. FINITE s ⇒ ∃a n. FINREC f b s a n

FINREC_compute

⊢ (∀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)

FINREC_1_LEMMA

⊢ ∀f b s a. FINREC f b s a (SUC 0) ⇔ ∃x. (s = {x}) ∧ (a = f x b)

FINITE_SUPPORT_DELTA

⊢ ∀op f a. FINITE (support op (λx. if x = a then f x else neutral op) s)

FINITE_SUPPORT

⊢ ∀op f s. FINITE s ⇒ FINITE (support op f s)

FINITE_RESTRICT

⊢ ∀s P. FINITE s ⇒ FINITE {x | x ∈ s ∧ P x}

FINITE_RECURSION

⊢ ∀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_REAL_INTERVAL

⊢ (∀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_NUMSEG

⊢ ∀m n. FINITE (m .. n)

FINITE_INDEX_NUMSEG

⊢ ∀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_INDEX_NUMBERS

⊢ ∀s.
      FINITE s ⇔
      ∃k f.
          (∀i j. i ∈ k ∧ j ∈ k ∧ (f i = f j) ⇒ (i = j)) ∧ FINITE k ∧
          (s = IMAGE f k)

DISJOINT_NUMSEG

⊢ ∀m n p q. DISJOINT (m .. n) (p .. q) ⇔ n < p ∨ q < m ∨ n < m ∨ q < p

CHOOSE_SUBSET_STRONG

⊢ ∀n s. (FINITE s ⇒ n ≤ CARD s) ⇒ ∃t. t ⊆ s ∧ t HAS_SIZE n

CHOOSE_SUBSET

⊢ ∀s. FINITE s ⇒ ∀n. n ≤ CARD s ⇒ ∃t. t ⊆ s ∧ t HAS_SIZE n

CARD_UNION_EQ

⊢ ∀s t u. FINITE u ∧ (s ∩ t = ∅) ∧ (s ∪ t = u) ⇒ (CARD s + CARD t = CARD u)

CARD_NUMSEG_LEMMA

⊢ ∀m d. CARD (m .. m + d) = d + 1

CARD_NUMSEG_1

⊢ ∀n. CARD (1 .. n) = n

CARD_NUMSEG

⊢ ∀m n. CARD (m .. n) = n + 1 − m

CARD_EQ_SUM

⊢ ∀s. FINITE s ⇒ (&CARD s = sum s (λx. 1))

CARD_EQ_NSUM

⊢ ∀s. FINITE s ⇒ (CARD s = nsum s (λx. 1))

CARD_BIGUNION

⊢ ∀s.
      FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
      (∀t u. t ∈ s ∧ u ∈ s ∧ t ≠ u ⇒ (t ∩ u = ∅)) ⇒
      (CARD (BIGUNION s) = nsum s CARD)