Theory iterate

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

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

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

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

⊢ nproduct = iterate $*

⊢ nsum = iterate $+

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

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

⊢ ∀m n. m + n − m = n

⊢ ∀m n. n − (m + n) = 0

⊢ ∀m n. m − (m + n) = 0

⊢ ∀s. BIGINTER s = 𝕌(:α) DIFF BIGUNION {𝕌(:α) DIFF t | t ∈ s}

⊢ ∀s. BIGUNION s = 𝕌(:α) DIFF BIGINTER {𝕌(:α) DIFF t | t ∈ s}

⊢ ∀A B C. (∀n. A * n ≤ B * n + C) ⇔ A ≤ B

⊢ ∀A B. (∀n. A * n ≤ B) ⇔ A = 0

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

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

⊢ ∀m n. CARD {m .. n} = n + 1 − m

⊢ ∀n. CARD {1 .. n} = n

⊢ ∀m d. CARD {m .. m + d} = d + 1

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

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

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

⊢ ∀n. 0 < n ⇒ count n = {0 .. n − 1}

⊢ ∀u s. u DIFF BIGINTER s = BIGUNION {u DIFF t | t ∈ s}

⊢ ∀m n p q. DISJOINT {m .. n} {p .. q} ⇔ n < p ∨ q < m ∨ n < m ∨ q < p

⊢ ∀s. BIGUNION s = ∅ ⇔ ∀t. t ∈ s ⇒ t = ∅

⊢ ∀P f s.
    (∃t. FINITE t ∧ t ⊆ IMAGE f s ∧ P t) ⇔
    ∃t. FINITE t ∧ t ⊆ s ∧ P (IMAGE f t)

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

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

⊢ ∀m n. FINITE {m .. n}

⊢ ∀n. FINITE {m | m ≤ n}

⊢ ∀n. FINITE {m | m < n}

⊢ ∀s. FINITE s ⇒ FINITE {t | t ⊆ s}

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

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

⊢ ∀f s t.
    FINITE t ∧ t ⊆ IMAGE f s ⇔ ∃s'. FINITE s' ∧ s' ⊆ s ∧ t = IMAGE f s'

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

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

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

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

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

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

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

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

⊢ (∀f b s a. FINREC f b s a 0 ⇔ s = ∅ ∧ a = b) ∧
  (∀f b s a n.
     FINREC f b s a <..num comp'n..> ⇔
     ∃x c.
       x ∈ s ∧ FINREC f b (s DELETE x) c (<..num comp'n..> − 1) ∧ a = f x c) ∧
  ∀f b s a n.
    FINREC f b s a <..num comp'n..> ⇔
    ∃x c. x ∈ s ∧ FINREC f b (s DELETE x) c <..num comp'n..> ∧ a = f x c

⊢ ∀P f s.
    (∀t. FINITE t ∧ t ⊆ IMAGE f s ⇒ P t) ⇔
    ∀t. FINITE t ∧ t ⊆ s ⇒ P (IMAGE f t)

⊢ ∀k n. from k ∩ {0 .. n} = {k .. n}

⊢ ∀k m n. from k ∩ {m .. n} = if m < k then {k .. n} else {m .. n}

⊢ ∀m n p. from p ∩ {m .. n} = {MAX p m .. n}

⊢ ∀f s x. x ∈ s ⇒ f x ∈ IMAGE f s

⊢ ∀m n. {m .. n} HAS_SIZE n + 1 − m

⊢ ∀n. {1 .. n} HAS_SIZE n

⊢ ∀n. {m | m ≤ n} HAS_SIZE n + 1

⊢ ∀n. {m | m < n} HAS_SIZE n

⊢ ∀n. INFINITE (from n)

⊢ x ∈ {m .. n} ⇔ m ≤ x ∧ x ≤ n

⊢ ∀m n. m ∈ {0 .. n} ⇔ m ≤ n

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

⊢ ∀p s. FINITE s ⇒ (iterate $/\ s p ⇔ ∀x. x ∈ s ⇒ p x)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀op f s.
    iterate op s f =
    if FINITE (support op f s) then iterate op (support op f s) f
    else neutral op

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

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

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

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

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

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

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

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

⊢ ∀op.
    monoidal op ⇒
    ∀f p s. p permutes s ⇒ iterate op s f = iterate op s (f ∘ p)

⊢ ∀op.
    monoidal op ⇒
    ∀f p s. p PERMUTES s ⇒ iterate op s f = iterate op s (f ∘ p)

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

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

⊢ ∀op.
    monoidal op ⇒
    ∀f s.
      FINITE s ⇒
      iterate (lifted op) s (λx. SOME (f x)) = SOME (iterate op s f)

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

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

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

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

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

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

⊢ (λ(x,y). P x y) = (λp. P (FST p) (SND p))

⊢ ∀m n. m ≤ m + n

⊢ ∀m n. n ≤ m + n

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

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

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

⊢ monoidal $/\

⊢ ∀op. monoidal op ⇒ monoidal (lifted op)

⊢ monoidal $*

⊢ neutral $+ = 0

⊢ neutral $/\ ⇔ T

⊢ ∀op. monoidal op ⇒ neutral (lifted op) = SOME (neutral op)

⊢ neutral $* = 1

⊢ ∀a b. a ≠ b ⇔ a ≠ b

⊢ ∀f m n p.
    m ≤ n + 1 ⇒
    nproduct {m .. n + p} f =
    nproduct {m .. n} f * nproduct {n + 1 .. n + p} f

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

⊢ ∀f m n. m ≤ n ⇒ nproduct {m .. n} f = f m * nproduct {m + 1 .. n} f

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

⊢ ∀f m n.
    0 < n ∧ m ≤ n ⇒ nproduct {m .. n} f = nproduct {m .. n − 1} f * f n

⊢ ∀P f s.
    P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
    P (nproduct s f)

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

⊢ ∀c s. FINITE s ⇒ nproduct s (λx. c) = c ** CARD s

⊢ ∀c m n. nproduct {m .. n} (λx. c) = c ** (n + 1 − m)

⊢ ∀c n. nproduct {1 .. n} (λx. c) = c ** n

⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ f a * nproduct (s DELETE a) f = nproduct s f

⊢ ∀s a. nproduct s (λx. if x = a then b else 1) = if a ∈ s then b else 1

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

⊢ ∀f s. FINITE s ⇒ (nproduct s f = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)

⊢ ∀f m n. nproduct {m .. n} f = 0 ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ f x = 0

⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 1) ⇒ nproduct s f = 1

⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 1) ⇒ nproduct {m .. n} f = 1

⊢ ∀f g m n.
    (∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
    nproduct {m .. n} f = nproduct {m .. n} g

⊢ ∀n. nproduct {1 .. n} (λm. m) = FACT n

⊢ ∀f g s.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    nproduct (IMAGE f s) g = nproduct s (g ∘ f)

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

⊢ ∀f m n.
    (∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
    nproduct {m .. n} f ≤ nproduct {m .. n} g

⊢ ∀f g s.
    FINITE s ⇒ nproduct s (λx. f x * g x) = nproduct s f * nproduct s g

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

⊢ ∀f g m n.
    nproduct {m .. n} (λx. f x * g x) =
    nproduct {m .. n} f * nproduct {m .. n} g

⊢ ∀f m p. nproduct {m + p .. n + p} f = nproduct {m .. n} (λi. f (i + p))

⊢ ∀s. nproduct s (λn. 1) = 1

⊢ ∀f m n.
    nproduct {2 * m .. 2 * n + 1} f =
    nproduct {m .. n} (λi. f (2 * i) * f (2 * i + 1))

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

⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < nproduct {m .. n} f

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

⊢ ∀f n. nproduct {n .. n} f = f n

⊢ ∀f u v.
    u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 1) ⇒ nproduct v f = nproduct u f

⊢ ∀f s. nproduct (support $* f s) f = nproduct s f

⊢ ∀f s t.
    FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
    nproduct (s ∪ t) f = nproduct s f * nproduct t f

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

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

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

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

⊢ ∀f m n p.
    m ≤ n + 1 ⇒
    nsum {m .. n + p} f = nsum {m .. n} f + nsum {n + 1 .. n + p} f

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

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

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

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

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

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

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

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

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

⊢ ∀f m n. m ≤ n ⇒ nsum {m .. n} f = f m + nsum {m + 1 .. n} f

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

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

⊢ ∀P f s.
    P 0 ∧ (∀x y. P x ∧ P y ⇒ P (x + y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
    P (nsum s f)

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

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

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

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

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

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

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

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

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

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

⊢ ∀f m n. nsum {m .. n} f = 0 ⇔ ∀i. m ≤ i ∧ i ≤ n ⇒ f i = 0

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

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

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

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

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

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

⊢ ∀f g s.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    nsum (IMAGE f s) g = nsum s (g ∘ f)

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

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

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

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

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

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x ≤ g x) ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
    nsum s f ≤ nsum s g

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀f p s. p permutes s ⇒ nsum s f = nsum s (f ∘ p)

⊢ ∀f p n. p permutes count n ⇒ nsum (count n) f = nsum (count n) (f ∘ p)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀f m n. n < m ⇒ nsum {m .. n} f = 0

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

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

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

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

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

⊢ ∀m n p. m ≤ n + 1 ⇒ {m .. n + p} = {m .. n} ∪ {n + 1 .. n + p}

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

⊢ ∀m p n. m ≤ p ∧ p ≤ n + 1 ⇒ {m .. p − 1} ∪ {p .. n} = {m .. n}

⊢ ∀m p n. m ≤ p + 1 ∧ p ≤ n ⇒ {m .. p} ∪ {p + 1 .. n} = {m .. n}

⊢ ∀m n. {m .. n} = ∅ ⇔ n < m

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

⊢ ∀m n. m ≤ n ⇒ m INSERT {m + 1 .. n} = {m .. n}

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

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

⊢ ∀m n. m ≤ SUC n ⇒ {m .. SUC n} = SUC n INSERT {m .. n}

⊢ ∀m n. m ≤ n ⇒ n INSERT {m .. n − 1} = {m .. n}

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

⊢ {s | s ⊆ ∅} = {∅} ∧
  ∀a t.
    {s | s ⊆ a INSERT t} = {s | s ⊆ t} ∪ IMAGE (λs. a INSERT s) {s | s ⊆ t}

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

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

⊢ ∀f P. {f x | P x} = IMAGE f {x | P x}

⊢ ∀m n p q. {m .. n} ⊆ {p .. q} ⇔ n < m ∨ p ≤ m ∧ n ≤ q

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

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

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

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

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

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

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

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

⊢ ∀P. (∀m n. P m n ⇒ P n m) ∧ (∀m n. P m (m + n)) ⇒ ∀m n. P m n

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

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

⊢ ∀R. (∀x y z. R x y ∧ R y z ⇒ R x z) ∧ (∀n. R n (SUC n)) ⇒
      ∀m n. m < n ⇒ R m n

⊢ ∀R. (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
      ((∀m n. m < n ⇒ R m n) ⇔ ∀n. R n (SUC n))

⊢ ∀P. (∀d n. P n (d + n)) ⇒ ∀m n. m ≤ n ⇒ P m n

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

⊢ lifted op NONE v0 = NONE ∧ lifted op (SOME v5) NONE = NONE ∧
  lifted op (SOME x) (SOME y) = SOME (op x y)

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