Package hol-real: HOL real theories
Information
| name | hol-real |
| version | 1.1 |
| description | HOL real theories |
| author | HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> |
| license | MIT |
| checksum | 18f940b3fc00364d54716adb8c40e8e3e5f8f480 |
| requires | base hol-base hol-integer |
| show | Data.Bool Data.List Data.Pair Function HOL4 Number.Natural Number.Real Relation |
Files
- Package tarball hol-real-1.1.tgz
- Theory source file hol-real.thy (included in the package tarball)
Defined Type Operators
- HOL4
- topology
- topology.metric
- topology.topology
- topology
Defined Constants
- HOL4
- integral
- integral.integrable
- integral.integral
- intreal
- intreal.is_int
- intreal.real_of_int
- intreal.INT_CEILING
- intreal.INT_FLOOR
- lim
- lim.contl
- lim.differentiable
- lim.diffl
- lim.tends_real_real
- nets
- nets.bounded
- nets.dorder
- nets.tends
- nets.tendsto
- poly
- poly.##
- poly.degree
- poly.diff
- poly.normalize
- poly.poly
- poly.poly_add
- poly.poly_diff_aux
- poly.poly_divides
- poly.poly_exp
- poly.poly_mul
- poly.poly_neg
- poly.poly_order
- poly.rsquarefree
- powser
- powser.diffs
- real
- real./
- real.inf
- real.pos
- real.sum
- real.sum_tupled
- real.sup
- real.NUM_CEILING
- real.NUM_FLOOR
- real_sigma
- real_sigma.REAL_SUM_IMAGE
- realax
- realax.inv
- realax.real_0
- realax.real_1
- seq
- seq.-->
- seq.cauchy
- seq.convergent
- seq.lim
- seq.mono
- seq.subseq
- seq.suminf
- seq.summable
- seq.sums
- topology
- topology.closed
- topology.dist
- topology.ismet
- topology.istopology
- topology.limpt
- topology.metric
- topology.mr1
- topology.mtop
- topology.neigh
- topology.open
- topology.re_intersect
- topology.re_union
- topology.topology
- topology.B
- transc
- transc.acs
- transc.asn
- transc.atn
- transc.cos
- transc.division
- transc.dsize
- transc.exp
- transc.fine
- transc.gauge
- transc.ln
- transc.pi
- transc.root
- transc.rpow
- transc.rsum
- transc.sin
- transc.sqrt
- transc.tan
- transc.tdiv
- transc.Dint
- integral
Theorems
⊦ nets.dorder (≥)
⊦ ¬pred_set.FINITE pred_set.UNIV
⊦ ¬(realax.real_1 = realax.real_0)
⊦ realax.real_0 = 0
⊦ realax.inv realax.real_0 = realax.real_0
⊦ 0 < transc.pi
⊦ ∀n. 0 ≤ n
⊦ ∀x. x ≤ x
⊦ ∀p. poly.poly_divides p p
⊦ ∀m. topology.ismet (topology.dist m)
⊦ ∀k. seq.--> (λx. k) k
⊦ realax.real_1 = 1
⊦ transc.sin transc.pi = 0
⊦ transc.tan transc.pi = 0
⊦ ∀n. 0 < suc n
⊦ ∀x. ¬(x < x)
⊦ ∀x. x ≤ real.pos x
⊦ ∀x. x ≤ abs x
⊦ ∀x0. lim.tends_real_real (λh. h) x0 x0
⊦ (>) = λx y. y < x
⊦ (≥) = λx y. y ≤ x
⊦ 0 < 1
⊦ 0 ≤ 1
⊦ realax.inv 0 = 0
⊦ transc.sin 0 = 0
⊦ transc.sqrt 0 = 0
⊦ transc.tan 0 = 0
⊦ ~0 = 0
⊦ abs 0 = 0
⊦ ∀n. 0 ≤ fromNatural n
⊦ ∀k x. lim.contl (λx. k) x
⊦ ∀x. x ≤ fromNatural (real.NUM_CEILING x)
⊦ ∀x. 0 < transc.exp x
⊦ ∀x. 0 ≤ real.pos x
⊦ ∀x. 0 ≤ transc.exp x
⊦ ∀x. 0 ≤ abs x
⊦ ∀x. realax.inv (realax.inv x) = x
⊦ ∀x. transc.ln (transc.exp x) = x
⊦ ∀y. transc.tan (transc.atn y) = y
⊦ ∀x. ~~x = x
⊦ ∀%%genvar%%779. realax.real_1 * %%genvar%%779 = %%genvar%%779
⊦ ∀%%genvar%%777. realax.real_0 + %%genvar%%777 = %%genvar%%777
⊦ ∀x. max x x = x
⊦ ∀x. min x x = x
⊦ ∀x. lim.diffl transc.exp (transc.exp x) x
⊦ ∀x. lim.diffl transc.sin (transc.cos x) x
⊦ ∀x. topology.limpt (topology.mtop topology.mr1) x pred_set.UNIV
⊦ ∀f. seq.cauchy f ⇔ seq.convergent f
⊦ ∀y. ∃n. y < fromNatural n
⊦ ¬(1 = 0)
⊦ topology.ismet (pair.UNCURRY (λx y. abs (y - x)))
⊦ (≤) = λx y. ¬(y < x)
⊦ real./ = λx y. x * realax.inv y
⊦ (-) = λx y. x + ~y
⊦ poly.poly_neg = poly.## (~1)
⊦ transc.cos transc.pi = ~1
⊦ transc.cos 0 = 1
⊦ transc.exp 0 = 1
⊦ transc.ln 1 = 0
⊦ transc.cos (fromNatural (arithmetic.BIT2 0)) < 0
⊦ ∀n. abs (fromNatural n) = fromNatural n
⊦ ∀k x. lim.tends_real_real (λx. k) k x
⊦ ∀x. ¬(transc.exp x = 0)
⊦ ∀x. 0 ≤ x * x
⊦ ∀x. transc.cos (~x) = transc.cos x
⊦ ∀x. abs (~x) = abs x
⊦ ∀x. abs (abs x) = abs x
⊦ ∀x. x - x = 0
⊦ ∀x. x + 0 = x
⊦ ∀x. x - 0 = x
⊦ ∀x. x ↑ 1 = x
⊦ ∀%%genvar%%775. ~%%genvar%%775 + %%genvar%%775 = realax.real_0
⊦ ∀x. 0 + x = x
⊦ ∀x. lim.diffl transc.cos (~transc.sin x) x
⊦ ∀p. poly.poly (poly.normalize p) = poly.poly p
⊦ ∀x y. x ≤ max x y
⊦ ∀x y. y ≤ max x y
⊦ ∀x y. min x y ≤ x
⊦ ∀x y. min x y ≤ y
⊦ ∀x. real.sup (λr. r = x) = x
⊦ ∀x. lim.diffl (λh. h) 1 x
⊦ ∀m x. nets.dorder (nets.tendsto (m, x))
⊦ realax.inv 1 = 1
⊦ transc.sqrt 1 = 1
⊦ abs 1 = 1
⊦ ∀n. ¬(fromNatural (factorial n) = 0)
⊦ ∀k x. lim.diffl (λx. k) 0 x
⊦ ∀x. ¬(transc.cos (transc.atn x) = 0)
⊦ ∀x. transc.sqrt x = transc.root (arithmetic.BIT2 0) x
⊦ ∀x. 0 ≤ x ↑ arithmetic.BIT2 0
⊦ ∀x. transc.exp (~x) = realax.inv (transc.exp x)
⊦ ∀x. transc.sin (~x) = ~transc.sin x
⊦ ∀x. transc.tan (~x) = ~transc.tan x
⊦ ∀x. abs (transc.cos x) ≤ 1
⊦ ∀x. abs (transc.sin x) ≤ 1
⊦ ∀x. x * 0 = 0
⊦ ∀x. x + ~x = 0
⊦ ∀x. real./ 0 x = 0
⊦ ∀x. 0 * x = 0
⊦ ∀x. ~x + x = 0
⊦ ∀x. 0 - x = ~x
⊦ ∀x. real./ x 1 = x
⊦ ∀x. x * 1 = x
⊦ ∀x. 1 * x = x
⊦ ∀l x. lim.contl (λx. poly.poly l x) x
⊦ ∀l x. lim.differentiable (λx. poly.poly l x) x
⊦ ∀p. poly.degree p = prim_rec.PRE (length (poly.normalize p))
⊦ ∀p. poly.poly (poly.poly_add p []) = poly.poly p
⊦ ∀f. seq.convergent f ⇔ seq.--> f (seq.lim f)
⊦ ∀f. seq.summable f ⇒ seq.--> f 0
⊦ ∀f. seq.summable f ⇒ seq.sums f (seq.suminf f)
⊦ ∀f l. seq.sums f l ⇒ seq.summable f
⊦ ∀f. seq.convergent f ⇔ ∃l. seq.--> f l
⊦ ∀f. seq.convergent f ⇔ seq.convergent (λn. ~f n)
⊦ ∀f. seq.summable f ⇔ ∃s. seq.sums f s
⊦ ∀f. seq.lim f = select l. seq.--> f l
⊦ ∀f. seq.suminf f = select s. seq.sums f s
⊦ ∀f. seq.summable (λk. abs (f k)) ⇒ seq.summable f
⊦ topology.mr1 = topology.metric (pair.UNCURRY (λx y. abs (y - x)))
⊦ max = λx y. if x ≤ y then y else x
⊦ min = λx y. if x ≤ y then x else y
⊦ transc.cos (real./ transc.pi (fromNatural (arithmetic.BIT2 0))) = 0
⊦ ∀n. fromNatural n < fromNatural (arithmetic.BIT2 0) ↑ n
⊦ ∀n. transc.sin (fromNatural n * transc.pi) = 0
⊦ ∀n. transc.tan (fromNatural n * transc.pi) = 0
⊦ ∀n. transc.root (suc n) 0 = 0
⊦ ∀n. 0 ↑ suc n = 0
⊦ ∀x. intreal.is_int x ⇔ x = intreal.real_of_int (intreal.INT_FLOOR x)
⊦ ∀x. realax.inv x = real./ 1 x
⊦ ∀x. transc.tan x = real./ (transc.sin x) (transc.cos x)
⊦ ∀x. transc.cos (x + transc.pi) = ~transc.cos x
⊦ ∀x. transc.sin (x + transc.pi) = ~transc.sin x
⊦ ∀x. x ↑ arithmetic.BIT2 0 = x * x
⊦ ∀f. seq.cauchy f ⇒ nets.bounded (topology.mr1, (≥)) f
⊦ ∀a b c. integral.integrable (a, b) (λx. c)
⊦ ∀x y. x > y ⇔ y < x
⊦ ∀x y. x ≥ y ⇔ y ≤ x
⊦ ∀x y. x * y = y * x
⊦ ∀x y. x + y = y + x
⊦ ∀x y. x = y ⇒ x ≤ y
⊦ ∀x y. x < y ⇒ x ≤ y
⊦ ∀x y. x < y ∨ y ≤ x
⊦ ∀x y. x ≤ y ∨ y < x
⊦ ∀x y. x ≤ y ∨ y ≤ x
⊦ ∀x y. y + (x - y) = x
⊦ ∀x y. x - (x - y) = y
⊦ ∀x y. x - y + y = x
⊦ ∀x y. x + y - x = y
⊦ ∀x y. x + y - y = x
⊦ ∀x. ∃n. x < fromNatural (arithmetic.BIT2 0) ↑ n
⊦ ∀x.
intreal.INT_CEILING x =
integer.LEAST_INT (λi. x ≤ intreal.real_of_int i)
⊦ ∀x. real.NUM_CEILING x = while.LEAST (λn. x ≤ fromNatural n)
⊦ ∀x. transc.ln x = select u. transc.exp u = x
⊦ ∀f. seq.subseq f ⇒ ∀n. n ≤ f n
⊦ ∀p. real.inf p = ~real.sup (λr. p (~r))
⊦ ∀f a. transc.Dint (a, a) f 0
⊦ 0 ≤ x ⇒ fromNatural (real.NUM_FLOOR x) ≤ x
⊦ transc.sin (real./ transc.pi (fromNatural (arithmetic.BIT2 0))) = 1
⊦ ∀n. 1 ≤ fromNatural (arithmetic.BIT2 0) ↑ n
⊦ ∀n. 1 ↑ n = 1
⊦ ∀x. ~x = ~1 * x
⊦ ∀x. x + x = fromNatural (arithmetic.BIT2 0) * x
⊦ ∀x. x ≤ ~x ⇔ x ≤ 0
⊦ ∀x. abs x = x ⇔ 0 ≤ x
⊦ ∀x. ~x ≤ x ⇔ 0 ≤ x
⊦ ∀x. 0 < x ⇒ transc.ln x < x
⊦ ∀x. 0 ≤ x ⇒ real.pos x = x
⊦ ∀p.
poly.poly (poly.diff (poly.poly_neg p)) =
poly.poly (poly.poly_neg (poly.diff p))
⊦ ∀s. ∃f. seq.subseq f ∧ seq.mono (λn. s (f n))
⊦ abs = λx. if 0 ≤ x then x else ~x
⊦ ∀x y. ¬(x < y ∧ y < x)
⊦ ∀x y. ¬(x < y ∧ y ≤ x)
⊦ ∀x y. ¬(x ≤ y ∧ y < x)
⊦ ∀x y. y < x ⇔ ¬(x ≤ y)
⊦ ∀x y. x ≤ y ⇔ ¬(y < x)
⊦ ∀x y. real./ x y = x * realax.inv y
⊦ ∀x y. x - y = x + ~y
⊦ ∀x y. x < y ⇒ ¬(x = y)
⊦ ∀x y. x < y ⇒ ¬(y < x)
⊦ ∀x y. ¬(x < y) ⇔ y ≤ x
⊦ ∀x y. ¬(x ≤ y) ⇔ y < x
⊦ ∀x y. ~(x - y) = y - x
⊦ ∀x y. x - ~y = x + y
⊦ ∀x y. x - (x + y) = ~y
⊦ ∀x y. x - y - x = ~y
⊦ ∀m x. topology.dist m (x, x) = 0
⊦ ∀L S'. topology.closed L S' ⇔ topology.open L (pred_set.COMPL S')
⊦ ∀f e.
real_sigma.REAL_SUM_IMAGE f (pred_set.INSERT e pred_set.EMPTY) = f e
⊦ ∀f x. seq.sums f x ⇒ x = seq.suminf f
⊦ ∀x x1. real.sum x x1 = real.sum_tupled (x, x1)
⊦ powser.diffs (λn. realax.inv (fromNatural (factorial n))) =
λn. realax.inv (fromNatural (factorial n))
⊦ real./ (fromNatural (arithmetic.BIT2 0))
(fromNatural (arithmetic.BIT2 0)) = 1
⊦ ∀n. fromNatural (suc n) = fromNatural n + 1
⊦ ∀n. ¬(n = 0) ⇒ 0 < fromNatural n
⊦ ∀n. transc.root (suc n) 1 = 1
⊦ ∀n. fromNatural n + 1 = fromNatural (suc n)
⊦ ∀a b. transc.Dint (a, b) (λx. 0) 0
⊦ ∀x. 0 < x ⇒ ¬(x = 0)
⊦ ∀x. 0 < x ⇒ 0 < realax.inv x
⊦ ∀x. 0 < x ⇒ 0 < transc.sqrt x
⊦ ∀x. 0 < x ⇒ lim.diffl transc.ln (realax.inv x) x
⊦ ∀x. 0 ≤ x ⇒ 0 ≤ realax.inv x
⊦ ∀x. 0 ≤ x ⇒ 0 ≤ transc.sqrt x
⊦ ∀x. x = 0 ∨ 0 < abs x
⊦ ∀x. 0 ≤ x ∨ 0 ≤ ~x
⊦ ∀x. real.pos x = 0 ⇔ x ≤ 0
⊦ ∀x. realax.inv x = 0 ⇔ x = 0
⊦ ∀x. ~x = 0 ⇔ x = 0
⊦ ∀x. abs x = 0 ⇔ x = 0
⊦ ∀x. ~x < 0 ⇔ 0 < x
⊦ ∀x. 0 < realax.inv x ⇔ 0 < x
⊦ ∀x. 0 < ~x ⇔ x < 0
⊦ ∀x. real.pos x ≤ 0 ⇔ x ≤ 0
⊦ ∀x. ~x ≤ 0 ⇔ 0 ≤ x
⊦ ∀x. 0 ≤ realax.inv x ⇔ 0 ≤ x
⊦ ∀x. 0 ≤ ~x ⇔ x ≤ 0
⊦ ∀x. transc.exp (transc.ln x) = x ⇔ 0 < x
⊦ ∀x. abs (x ↑ arithmetic.BIT2 0) = x ↑ arithmetic.BIT2 0
⊦ ∀x. abs x ↑ arithmetic.BIT2 0 = x ↑ arithmetic.BIT2 0
⊦ ∀r. r < 1 ⇒ real.NUM_FLOOR r = 0
⊦ ∀x. transc.exp x * transc.exp (~x) = 1
⊦ ∀x. transc.exp (~x) * transc.exp x = 1
⊦ ∀p. poly.poly p = poly.poly [] ⇒ poly.degree p = 0
⊦ ∀c. powser.diffs (λn. ~c n) = λn. ~powser.diffs c n
⊦ ∀i j. integer.int_lt i j ⇒ intreal.real_of_int i < intreal.real_of_int j
⊦ ∀x n. fromNatural x ↑ n = fromNatural (x ↑ n)
⊦ ∀m n. suc m = suc n ⇔ m = n
⊦ ∀m n. fromNatural m = fromNatural n ⇔ m = n
⊦ ∀m n. fromNatural m < fromNatural n ⇔ m < n
⊦ ∀m n. fromNatural m ≤ fromNatural n ⇔ m ≤ n
⊦ ∀x n. realax.inv x ↑ n = realax.inv (x ↑ n)
⊦ ∀c n. abs c ↑ n = abs (c ↑ n)
⊦ ∀x n. x ≤ fromNatural n ⇒ real.NUM_CEILING x ≤ n
⊦ ∀a b. transc.rpow a b = transc.exp (b * transc.ln a)
⊦ ∀x y. x < y ⇒ transc.exp x < transc.exp y
⊦ ∀x y. x ≤ y ⇒ real.pos x ≤ real.pos y
⊦ ∀x y. ~x = y ⇔ x = ~y
⊦ ∀x y. ~(x * y) = x * ~y
⊦ ∀x y. ~(x * y) = ~x * y
⊦ ∀x y. abs (x - y) = abs (y - x)
⊦ ∀x y. x * ~y = ~(x * y)
⊦ ∀x y. ~x * y = ~(x * y)
⊦ ∀x y. ~x - y = ~(x + y)
⊦ ∀x y. realax.inv x = realax.inv y ⇔ x = y
⊦ ∀x y. transc.exp x = transc.exp y ⇔ x = y
⊦ ∀x y. ~x = ~y ⇔ x = y
⊦ ∀x y. transc.exp x < transc.exp y ⇔ x < y
⊦ ∀x y. ~x < ~y ⇔ y < x
⊦ ∀x y. transc.exp x ≤ transc.exp y ⇔ x ≤ y
⊦ ∀x y. ~x ≤ ~y ⇔ y ≤ x
⊦ ∀x y. ~x * ~y = x * y
⊦ ∀x y. ~x - ~y = y - x
⊦ ∀y. 0 < y ⇒ ∃x. transc.exp x = y
⊦ ∀p x. poly.poly (poly.poly_neg p) x = ~poly.poly p x
⊦ ∀p q. poly.poly p = poly.poly [] ⇒ poly.poly_divides q p
⊦ ∀L P.
pred_set.SUBSET P (topology.open L) ⇒
topology.open L (pred_set.BIGUNION P)
⊦ ∀s. pred_set.FINITE s ⇒ real_sigma.REAL_SUM_IMAGE (λx. 0) s = 0
⊦ ∀f. seq.subseq f ⇔ ∀n. f n < f (suc n)
⊦ ∀f n. real.sum (n, 1) f = f n
⊦ ∀c. powser.diffs c = λn. fromNatural (suc n) * c (suc n)
⊦ ∀f x. lim.contl f x ⇔ lim.tends_real_real f (f x) x
⊦ 0 ≤ x ⇒ transc.sqrt (x ↑ arithmetic.BIT2 0) = x
⊦ ∀m n. real.sum (m, n) (λr. 0) = 0
⊦ ∀n. abs (~1 ↑ n) = 1
⊦ ∀x. real.pos x = if 0 ≤ x then x else 0
⊦ ∀x.
transc.cos x =
transc.sin (real./ transc.pi (fromNatural (arithmetic.BIT2 0)) - x)
⊦ ∀x.
transc.sin x =
transc.cos (real./ transc.pi (fromNatural (arithmetic.BIT2 0)) - x)
⊦ ∀x. abs x = if 0 ≤ x then x else ~x
⊦ ∀%%genvar%%772.
¬(%%genvar%%772 = realax.real_0) ⇒
realax.inv %%genvar%%772 * %%genvar%%772 = realax.real_1
⊦ ∀x. 0 < x ⇒ 1 < transc.exp x
⊦ ∀x. ¬(x = 0) ⇔ 0 < abs x
⊦ ∀x. ¬(x = 0) ⇒ realax.inv (realax.inv x) = x
⊦ ∀x. 1 ≤ x ⇒ 0 ≤ transc.ln x
⊦ ∀x. 0 ≤ x + x ⇔ 0 ≤ x
⊦ ∀x.
transc.cos (x + fromNatural (arithmetic.BIT2 0) * transc.pi) =
transc.cos x
⊦ ∀x.
transc.sin (x + fromNatural (arithmetic.BIT2 0) * transc.pi) =
transc.sin x
⊦ ∀x.
transc.tan (x + fromNatural (arithmetic.BIT2 0) * transc.pi) =
transc.tan x
⊦ ∀l x. lim.diffl (λx. poly.poly l x) (poly.poly (poly.diff l) x) x
⊦ ∀m x y. 0 ≤ topology.dist m (x, y)
⊦ ∀P Q. topology.re_intersect P Q = λx. P x ∧ Q x
⊦ ∀P Q. topology.re_union P Q = λx. P x ∨ Q x
⊦ ∀f l. seq.--> f l ⇔ seq.--> (λn. f (suc n)) l
⊦ ∀f. nets.bounded (topology.mr1, (≥)) f ∧ seq.mono f ⇒ seq.convergent f
⊦ ∀f l x. lim.diffl f l x ⇒ lim.contl f x
⊦ ∀f x. lim.differentiable f x ⇔ ∃l. lim.diffl f l x
⊦ ∀f x. lim.contl f x ⇒ lim.contl (λx. ~f x) x
⊦ ∀m n. fromNatural m * fromNatural n = fromNatural (m * n)
⊦ ∀m n. fromNatural m + fromNatural n = fromNatural (m + n)
⊦ ∀n x. transc.exp (fromNatural n * x) = transc.exp x ↑ n
⊦ ∀n r. real.sum (0, n) r = real_sigma.REAL_SUM_IMAGE r (pred_set.count n)
⊦ ∀x y. max x y = ~min (~x) (~y)
⊦ ∀x y. max x y = if x ≤ y then y else x
⊦ ∀x y. min x y = ~max (~x) (~y)
⊦ ∀x y. min x y = if x ≤ y then x else y
⊦ ∀x y. transc.exp (x + y) = transc.exp x * transc.exp y
⊦ ∀x y. transc.exp (x - y) = real./ (transc.exp x) (transc.exp y)
⊦ ∀x y. ~(x + y) = ~x + ~y
⊦ ∀x y. abs (x * y) = abs x * abs y
⊦ ∀x y. abs (x + y) ≤ abs x + abs y
⊦ ∀x y. x < x + y ⇔ 0 < y
⊦ ∀x y. y < x + y ⇔ 0 < x
⊦ ∀x y. x ≤ x + y ⇔ 0 ≤ y
⊦ ∀x y. y ≤ x + y ⇔ 0 ≤ x
⊦ ∀x y. x + y = x ⇔ y = 0
⊦ ∀x y. x + y = y ⇔ x = 0
⊦ ∀x y. topology.dist topology.mr1 (x, y) = abs (y - x)
⊦ ∀x y. abs x - abs y ≤ abs (x - y)
⊦ ∀x y. 0 < x - y ⇔ y < x
⊦ ∀x y. 0 ≤ x - y ⇔ y ≤ x
⊦ ∀x y. x - y = 0 ⇔ x = y
⊦ ∀x d. topology.dist topology.mr1 (x, x + d) = abs d
⊦ ∀x d. topology.dist topology.mr1 (x, x - d) = abs d
⊦ ∀x. real.NUM_FLOOR x = while.LEAST (λn. fromNatural (n + 1) > x)
⊦ ∀f n. real_sigma.REAL_SUM_IMAGE f (pred_set.count n) = real.sum (0, n) f
⊦ ∀f. seq.--> (λk. abs (f k)) 0 ⇔ seq.--> f 0
⊦ x < fromNatural n ⇔ real.NUM_FLOOR (x + 1) ≤ n
⊦ real.NUM_FLOOR x ≤ y ⇔ x < fromNatural y + 1
⊦ fromNatural n ≤ x ⇔ n < real.NUM_FLOOR (x + 1)
⊦ real./ 3 3 = 1
⊦ ∀n. transc.cos (fromNatural n * transc.pi) = ~1 ↑ n
⊦ ∀n. ¬(fromNatural n = 0) ⇔ 0 < fromNatural n
⊦ ∀a. ¬(poly.poly (a :: 1 :: []) = poly.poly [])
⊦ ∀x. realax.inv x = if x = 0 then 0 else inv x
⊦ ∀x. 0 < x ⇒ transc.ln (realax.inv x) = ~transc.ln x
⊦ ∀a. 0 < a ⇒ transc.rpow a 1 = a
⊦ ∀x. 0 ≤ x ⇒ transc.sqrt (realax.inv x) = realax.inv (transc.sqrt x)
⊦ ∀x. 0 ≤ x ⇒ real./ x (transc.sqrt x) = transc.sqrt x
⊦ ∀x. 0 ≤ x ⇒ transc.sqrt x ↑ arithmetic.BIT2 0 = x
⊦ ∀x. ¬(x = 0) ⇒ ¬(realax.inv x = 0)
⊦ ∀x. 0 < x * x ⇔ ¬(x = 0)
⊦ ∀x. transc.sqrt x ↑ arithmetic.BIT2 0 = x ⇔ 0 ≤ x
⊦ ∀d. real./ d (fromNatural (arithmetic.BIT2 0)) < d ⇔ 0 < d
⊦ ∀x. lim.diffl transc.atn (realax.inv (1 + x ↑ arithmetic.BIT2 0)) x
⊦ ∀p. poly.poly p = poly.poly [] ⇒ poly.poly (poly.diff p) = poly.poly []
⊦ ∀D a b. transc.division (a, b) D ⇒ a ≤ b
⊦ ∀x x0. seq.--> x x0 ⇔ seq.--> (λn. ~x n) (~x0)
⊦ ∀f l. seq.--> f l ⇒ seq.--> (λk. abs (f k)) (abs l)
⊦ ∀x x0. seq.sums x x0 ⇒ seq.sums (λn. ~x n) (~x0)
⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n
⊦ ∀n x. x ↑ n = 0 ⇒ x = 0
⊦ ∀x n. 0 < x ⇒ 0 < x ↑ n
⊦ ∀x y. x ≤ y ⇔ x < y ∨ x = y
⊦ ∀x y. x ≤ y ⇒ x < y + 1
⊦ ∀x y. x = y ∨ x < y ∨ y < x
⊦ ∀x y. x ≤ ~y ⇔ x + y ≤ 0
⊦ ∀x y. ~x ≤ y ⇔ 0 ≤ x + y
⊦ ∀a b. 0 < a ⇒ 0 < transc.rpow a b
⊦ ∀x y. x + y = 0 ⇔ x = ~y
⊦ ∀x y. x + y = 0 ⇔ y = ~x
⊦ ∀x y. abs (x - y) < y ⇒ 0 < x
⊦ ∀x y. abs (abs x - abs y) ≤ abs (x - y)
⊦ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y
⊦ ∀x y. transc.exp (x + y) * transc.exp (~x) = transc.exp y
⊦ ∀x.
intreal.INT_FLOOR x =
integer.LEAST_INT
(λi.
x <
intreal.real_of_int (integer.int_add i (integer.int_of_num 1)))
⊦ ∀x. 0 ≤ x ⇒ ∀n. 0 ≤ x ↑ n
⊦ ∀p n.
poly.poly (poly.poly_diff_aux n (poly.poly_neg p)) =
poly.poly (poly.poly_neg (poly.poly_diff_aux n p))
⊦ ∀p c.
poly.poly (poly.diff (poly.## c p)) =
poly.poly (poly.## c (poly.diff p))
⊦ ∀p. poly.poly p = poly.poly [] ⇔ all (λc. c = 0) p
⊦ ∀x x0. seq.--> x x0 ⇔ nets.tends x x0 (topology.mtop topology.mr1, (≥))
⊦ 0 ≤ y ⇒ (x ≤ real.NUM_FLOOR y ⇔ fromNatural x ≤ y)
⊦ ∀n. ~1 ↑ (arithmetic.BIT2 0 * n) = 1
⊦ ∀a. 0 < a ⇒ transc.rpow a 0 = 1
⊦ ∀x. 0 ≤ x ⇒ 1 + x ≤ transc.exp x
⊦ ∀x. 0 ≤ x ⇒ transc.ln (1 + x) ≤ x
⊦ ∀x. ¬(x = 0) ⇒ ~realax.inv x = realax.inv (~x)
⊦ ∀x. ¬(x = 0) ⇒ abs (realax.inv x) = realax.inv (abs x)
⊦ ∀x. ¬(x = 0) ⇒ real./ x x = 1
⊦ ∀x.
x - real./ x (fromNatural (arithmetic.BIT2 0)) =
real./ x (fromNatural (arithmetic.BIT2 0))
⊦ ∀d. 0 < real./ d (fromNatural (arithmetic.BIT2 0)) ⇔ 0 < d
⊦ ∀x.
seq.sums
(λn. (let n ← n in realax.inv (fromNatural (factorial n))) * x ↑ n)
(transc.exp x)
⊦ ∀x.
real./ x (fromNatural (arithmetic.BIT2 0)) +
real./ x (fromNatural (arithmetic.BIT2 0)) = x
⊦ ∀l. poly.diff l = if l = [] then [] else poly.poly_diff_aux 1 (tail l)
⊦ ∀D a b. transc.division (a, b) D ⇒ D 0 = a
⊦ ∀f s. seq.sums f s ⇔ seq.--> (λn. real.sum (0, n) f) s
⊦ 0 = realax.real_0 ∧
∀n. fromNatural (suc n) = fromNatural n + realax.real_1
⊦ ∀m n. m < n ⇔ m ≤ n ∧ ¬(m = n)
⊦ ∀n x. 0 < x ⇒ 0 < transc.root (suc n) x
⊦ ∀n x. 0 ≤ x ⇒ 0 ≤ transc.root (suc n) x
⊦ ∀n x. x ↑ suc n = 0 ⇔ x = 0
⊦ ∀x n. 0 < x ⇒ 0 < x ↑ suc n
⊦ ∀a b c. transc.Dint (a, b) (λx. c) (c * (b - a))
⊦ ∀x y. x < y ⇔ x ≤ y ∧ ¬(x = y)
⊦ ∀x y. x * y = 1 ⇒ x = realax.inv y
⊦ ∀x y. x * y = 1 ⇒ y = realax.inv x
⊦ ∀x y. abs (x - y) < ~y ⇒ x < 0
⊦ ∀c. abs c < 1 ⇒ seq.--> (λn. c ↑ n) 0
⊦ ∀p n.
poly.poly (poly.poly_diff_aux (suc n) p) =
poly.poly (poly.poly_add (poly.poly_diff_aux n p) p)
⊦ ∀p1 p2.
poly.poly (poly.diff (poly.poly_add p1 p2)) =
poly.poly (poly.poly_add (poly.diff p1) (poly.diff p2))
⊦ ∀s N. ∃k. ∀n. n < N ⇒ abs (s n) < k
⊦ ∀f.
nets.bounded (topology.mr1, (≥)) (λn. ~f n) ⇔
nets.bounded (topology.mr1, (≥)) f
⊦ poly.poly_neg [] = [] ∧ poly.poly_neg (h :: t) = ~h :: poly.poly_neg t
⊦ ∀x m n. (x ↑ m) ↑ n = x ↑ (m * n)
⊦ ∀x y z. y < z ⇒ x + y < x + z
⊦ ∀x y z. y ≤ z ⇒ x + y ≤ x + z
⊦ ∀x y z. x = y - z ⇔ x + z = y
⊦ ∀x y z. x < y - z ⇔ x + z < y
⊦ ∀x y z. x ≤ y - z ⇔ x + z ≤ y
⊦ ∀x y z. x - y = z ⇔ x = z + y
⊦ ∀x y z. x + y < z ⇔ x < z - y
⊦ ∀x y z. x - y < z ⇔ x < z + y
⊦ ∀x y z. x - y ≤ z ⇔ x ≤ z + y
⊦ ∀x y z. x * (y * z) = x * y * z
⊦ ∀x y z. x + (y + z) = x + y + z
⊦ ∀x y z. x + y = x + z ⇔ y = z
⊦ ∀x y z. x + z = y + z ⇔ x = y
⊦ ∀x y z. x + y < x + z ⇔ y < z
⊦ ∀x y z. x + z < y + z ⇔ x < y
⊦ ∀x y z. x + y ≤ x + z ⇔ y ≤ z
⊦ ∀x y z. x + z ≤ y + z ⇔ x ≤ y
⊦ ∀x y z. x - z ≤ y - z ⇔ x ≤ y
⊦ ∀a b c. a - b + (b - c) = a - c
⊦ ∀x y z. x < y ∧ y < z ⇒ x < z
⊦ ∀x y z. x < y ∧ y ≤ z ⇒ x < z
⊦ ∀x y z. x ≤ y ∧ y < z ⇒ x < z
⊦ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
⊦ ∀x y. x < y ⇒ ∃z. x < z ∧ z < y
⊦ ∀x y. 1 < x ⇒ ∃n. y < x ↑ n
⊦ ∀x.
transc.exp x =
seq.suminf
(λn. (let n ← n in realax.inv (fromNatural (factorial n))) * x ↑ n)
⊦ ∀x. 0 < x ⇒ ∀y. ∃n. y < fromNatural n * x
⊦ ∀a. 0 < a ⇒ transc.rpow 1 a = 1
⊦ ∀x. ¬(x = 0) ⇒ x * realax.inv x = 1
⊦ ∀x. ¬(x = 0) ⇒ realax.inv x * x = 1
⊦ ∀x. 1 < x ⇒ 1 < x ↑ arithmetic.BIT2 0
⊦ ∀x. 1 ≤ x ⇒ 1 ≤ x ↑ arithmetic.BIT2 0
⊦ ∀x. ~1 ≤ transc.cos x ∧ transc.cos x ≤ 1
⊦ ∀x. ~1 ≤ transc.sin x ∧ transc.sin x ≤ 1
⊦ ∀x. 0 < x ∧ x < transc.pi ⇒ 0 < transc.sin x
⊦ ∀x. 0 ≤ x ∧ x ≤ transc.pi ⇒ 0 ≤ transc.sin x
⊦ ∀x. 0 ≤ x ∧ x ≤ transc.pi ⇒ transc.acs (transc.cos x) = x
⊦ ∀p m n. m ≤ n ⇒ poly.poly_divides (poly.poly_exp p m) (poly.poly_exp p n)
⊦ ∀p n x. poly.poly (poly.poly_exp p n) x = poly.poly p x ↑ n
⊦ ∀p c x. poly.poly (poly.## c p) x = c * poly.poly p x
⊦ ∀p q r.
poly.poly_divides p q ∧ poly.poly_divides q r ⇒ poly.poly_divides p r
⊦ ∀p1 p2.
poly.poly_divides p1 p2 ⇔
∃q. poly.poly p2 = poly.poly (poly.poly_mul p1 q)
⊦ ∀m x y. topology.dist m (x, y) = topology.dist m (y, x)
⊦ ∀top S'. topology.closed top S' ⇔ ∀x. topology.limpt top x S' ⇒ S' x
⊦ ∀D a b. transc.division (a, b) D ⇒ D (transc.dsize D) = b
⊦ ∀x x1 x2. seq.--> x x1 ∧ seq.--> x x2 ⇒ x1 = x2
⊦ ∀f.
seq.summable (λk. abs (f k)) ⇒
abs (seq.suminf f) ≤ seq.suminf (λk. abs (f k))
⊦ ∀s. nets.bounded (topology.mr1, (≥)) s ⇔ ∃k. ∀n. abs (s n) < k
⊦ ∀n x. 1 ≤ x ⇒ 1 ≤ x ↑ n
⊦ ∀a n. 0 < a ⇒ a ↑ n = transc.rpow a (fromNatural n)
⊦ ∀c n. ¬(c = 0) ⇒ ¬(c ↑ n = 0)
⊦ ∀a b f i. b < a ⇒ transc.Dint (a, b) f i
⊦ ∀a b. a ≤ b ⇒ a ≤ real./ (a + b) (fromNatural (arithmetic.BIT2 0))
⊦ ∀a b. a ≤ b ⇒ real./ (a + b) (fromNatural (arithmetic.BIT2 0)) ≤ b
⊦ ∀x k. abs x ≤ k ⇔ ~k ≤ x ∧ x ≤ k
⊦ ∀x y. ¬(y = 0) ⇒ y * real./ x y = x
⊦ ∀x y. ¬(y = 0) ⇒ real./ x y * y = x
⊦ ∀a b. ¬(0 = a) ⇒ ¬(transc.rpow a b = 0)
⊦ ∀x y. realax.real_0 < x ∧ realax.real_0 < y ⇒ realax.real_0 < x * y
⊦ ∀x y. abs (x - y) < abs y ⇒ ¬(x = 0)
⊦ ∀x. 0 < x ⇒ ∃y. 0 < y ∧ y < x
⊦ ∀c. abs c < 1 ⇒ seq.--> (λn. abs c ↑ n) 0
⊦ ∀p q.
poly.poly p = poly.poly q ⇒
poly.poly (poly.diff p) = poly.poly (poly.diff q)
⊦ ∀f s.
real_sigma.REAL_SUM_IMAGE f s = pred_set.ITSET (λe acc. f e + acc) s 0
⊦ ∀D a b. transc.division (a, b) D ⇒ ∀r. a ≤ D r
⊦ ∀D a b. transc.division (a, b) D ⇒ ∀r. D r ≤ b
⊦ ∀x y z. y < x + ~z ⇔ y + z < x
⊦ ∀x y z. x + ~y < z ⇔ x < z + y
⊦ ∀x y d. abs (x - y) < d ⇒ y < x + d
⊦ ∀a b. a = b ⇒ transc.dsize (λn. if n = 0 then a else b) = 0
⊦ ∀a b. a ≤ b ⇒ integral.integral (a, b) (λx. 0) = 0
⊦ ∀x. x = 0 ∨ 0 < x ∨ 0 < ~x
⊦ ∀r.
intreal.real_of_int (intreal.INT_FLOOR r) ≤ r ∧
r <
intreal.real_of_int
(integer.int_add (intreal.INT_FLOOR r) (integer.int_of_num 1))
⊦ ∀r.
intreal.real_of_int
(integer.int_sub (intreal.INT_CEILING r) (integer.int_of_num 1)) <
r ∧ r ≤ intreal.real_of_int (intreal.INT_CEILING r)
⊦ ∀x.
transc.sin x ↑ arithmetic.BIT2 0 + transc.cos x ↑ arithmetic.BIT2 0 = 1
⊦ ∀q. length (poly.poly_mul (~a :: 1 :: []) q) = suc (length q)
⊦ ∀m x y. topology.dist m (x, y) = 0 ⇔ x = y
⊦ ∀S' top x. topology.open top S' ∧ S' x ⇒ topology.neigh top (S', x)
⊦ ∀P.
pred_set.FINITE P ⇒
∀f.
real_sigma.REAL_SUM_IMAGE (λx. ~f x) P =
~real_sigma.REAL_SUM_IMAGE f P
⊦ ∀f. seq.subseq f ⇔ ∀m n. m < n ⇒ f m < f n
⊦ ∀s f.
nets.bounded (topology.mr1, (≥)) s ⇒
nets.bounded (topology.mr1, (≥)) (λn. s (f n))
⊦ ∀E g. transc.gauge E g ⇔ ∀x. E x ⇒ 0 < g x
⊦ ∀f x. lim.contl f x ⇔ lim.tends_real_real (λh. f (x + h)) (f x) 0
⊦ ∀n x. 0 ≤ x ⇒ transc.root (suc n) (x ↑ suc n) = x
⊦ ∀n x. 0 ≤ x ⇒ transc.root (suc n) x ↑ suc n = x
⊦ ∀a n. ¬(poly.poly (poly.poly_exp (a :: 1 :: []) n) = poly.poly [])
⊦ ∀x y. real./ x y = if y = 0 then 0 else x / y
⊦ ∀a b. 0 < a ⇒ transc.ln (transc.rpow a b) = b * transc.ln a
⊦ ∀a b. 0 < a ⇒ transc.rpow (realax.inv a) b = realax.inv (transc.rpow a b)
⊦ ∀x d. 0 < d ⇒ topology.dist topology.mr1 (x, x + d) = d
⊦ ∀x d. 0 < d ⇒ topology.dist topology.mr1 (x, x - d) = d
⊦ ∀x d. 0 ≤ d ⇒ topology.dist topology.mr1 (x, x + d) = d
⊦ ∀x d. 0 ≤ d ⇒ topology.dist topology.mr1 (x, x - d) = d
⊦ ∀x y. 0 < x ∧ x < y ⇒ realax.inv y < realax.inv x
⊦ ∀x y. 0 < x ∧ x ≤ y ⇒ realax.inv y ≤ realax.inv x
⊦ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ transc.sqrt x ≤ transc.sqrt y
⊦ ∀t h.
poly.poly (poly.diff (h :: t)) =
poly.poly (poly.poly_add (0 :: poly.diff t) t)
⊦ ∀p.
poly.poly (poly.diff p) = poly.poly [] ⇒
∃h. poly.poly p = poly.poly (h :: [])
⊦ ∀f. seq.subseq f ⇒ ∀N1 N2. ∃n. n ≥ N1 ∧ f n ≥ N2
⊦ ∀x x0 c. seq.sums x x0 ⇒ seq.sums (λn. c * x n) (c * x0)
⊦ ∀x x0 c. seq.sums x x0 ⇒ seq.sums (λn. real./ (x n) c) (real./ x0 c)
⊦ ∀d p a b. transc.tdiv (a, b) (d, p) ⇒ a ≤ b
⊦ ∀f.
seq.summable f ⇒
seq.sums (λn. real.sum (arithmetic.BIT2 0 * n, arithmetic.BIT2 0) f)
(seq.suminf f)
⊦ ∀f l x. lim.tends_real_real f l x ⇔ lim.tends_real_real (λx. ~f x) (~l) x
⊦ ∀f l x. lim.diffl f l x ⇒ lim.diffl (λx. ~f x) (~l) x
⊦ ∀f. (∀x. lim.diffl f 0 x) ⇒ ∀x y. f x = f y
⊦ (∀a. topology.metric (topology.dist a) = a) ∧
∀r. topology.ismet r ⇔ topology.dist (topology.metric r) = r
⊦ (∀a. topology.topology (topology.open a) = a) ∧
∀r. topology.istopology r ⇔ topology.open (topology.topology r) = r
⊦ ∀i.
intreal.real_of_int i =
if integer.int_lt i (integer.int_of_num 0) then
~fromNatural (integer.Num (integer.int_neg i))
else fromNatural (integer.Num i)
⊦ ∀n x y. (x * y) ↑ n = x ↑ n * y ↑ n
⊦ ∀n x. lim.diffl (λx. x ↑ n) (fromNatural n * x ↑ arithmetic.- n 1) x
⊦ ∀x m n. x ↑ (m + n) = x ↑ m * x ↑ n
⊦ ∀x y n. real./ x y ↑ n = real./ (x ↑ n) (y ↑ n)
⊦ ∀x y z. z < min x y ⇔ z < x ∧ z < y
⊦ ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y
⊦ ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y
⊦ ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z
⊦ ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z
⊦ ∀a b c. transc.rpow a (b + c) = transc.rpow a b * transc.rpow a c
⊦ ∀a b c.
transc.rpow a (b - c) = real./ (transc.rpow a b) (transc.rpow a c)
⊦ ∀x y z. x * (y + z) = x * y + x * z
⊦ ∀x y z. x * (y - z) = x * y - x * z
⊦ ∀x y z. (x + y) * z = x * z + y * z
⊦ ∀x y z. (x - y) * z = x * z - y * z
⊦ ∀x y z. real./ y x + real./ z x = real./ (y + z) x
⊦ ∀z x y. max (x + z) (y + z) = max x y + z
⊦ ∀z x y. max (x - z) (y - z) = max x y - z
⊦ ∀z x y. min (x + z) (y + z) = min x y + z
⊦ ∀z x y. min (x - z) (y - z) = min x y - z
⊦ ∀z x y. x * y + (z - x) * y = z * y
⊦ ∀z x y. y * x + y * (z - x) = y * z
⊦ ∀a b. a < b ⇒ transc.dsize (λn. if n = 0 then a else b) = 1
⊦ ∀a b. a ≤ b ⇒ transc.division (a, b) (λn. if n = 0 then a else b)
⊦ ∀x p1 p2.
poly.poly (poly.poly_mul p1 p2) x = poly.poly p1 x * poly.poly p2 x
⊦ ∀x.
transc.sin (fromNatural (arithmetic.BIT2 0) * x) =
fromNatural (arithmetic.BIT2 0) * (transc.sin x * transc.cos x)
⊦ ∀x.
¬(transc.cos x = 0) ⇒
lim.diffl transc.tan (realax.inv (transc.cos x ↑ arithmetic.BIT2 0)) x
⊦ ∀x. 0 < x ∧ x < fromNatural (arithmetic.BIT2 0) ⇒ 0 < transc.sin x
⊦ ∀p c n.
poly.poly (poly.poly_diff_aux n (poly.## c p)) =
poly.poly (poly.## c (poly.poly_diff_aux n p))
⊦ ∀p1 p2 x.
poly.poly (poly.poly_add p1 p2) x = poly.poly p1 x + poly.poly p2 x
⊦ ∀p q a.
poly.poly p = poly.poly q ⇒ poly.poly_order a p = poly.poly_order a q
⊦ ∀p q r.
poly.poly (poly.poly_mul p (poly.poly_mul q r)) =
poly.poly (poly.poly_mul (poly.poly_mul p q) r)
⊦ ∀p q r.
poly.poly_divides p q ∧ poly.poly_divides p r ⇒
poly.poly_divides p (poly.poly_add q r)
⊦ ∀p q r.
poly.poly_divides p q ∧ poly.poly_divides p (poly.poly_add q r) ⇒
poly.poly_divides p r
⊦ ∀p q r.
poly.poly_divides p r ∧ poly.poly_divides p (poly.poly_add q r) ⇒
poly.poly_divides p q
⊦ ∀m x y. ¬(x = y) ⇒ 0 < topology.dist m (x, y)
⊦ ∀m x e. 0 < e ⇒ topology.open (topology.mtop m) (topology.B m (x, e))
⊦ ∀g x x0.
nets.tends x x0 (topology.mtop topology.mr1, g) ⇒
nets.bounded (topology.mr1, g) x
⊦ ∃!x. 0 ≤ x ∧ x ≤ fromNatural (arithmetic.BIT2 0) ∧ transc.cos x = 0
⊦ ∀n x. 0 < x ⇒ transc.ln (x ↑ n) = fromNatural n * transc.ln x
⊦ ∀x y f. (∀n. x ≤ f n) ∧ seq.--> f y ⇒ x ≤ y
⊦ ∀x y f. (∀n. f n ≤ x) ∧ seq.--> f y ⇒ y ≤ x
⊦ ∀a b f. integral.integrable (a, b) f ⇔ ∃i. transc.Dint (a, b) f i
⊦ ∀a b f. integral.integral (a, b) f = select i. transc.Dint (a, b) f i
⊦ ∀x y. (x + y) * (x - y) = x * x - y * y
⊦ ∀y z.
real./ (real./ y (fromNatural (arithmetic.BIT2 0)))
(real./ z (fromNatural (arithmetic.BIT2 0))) = real./ y z
⊦ ∀y z.
real./ y (fromNatural (arithmetic.BIT2 0)) *
real./ (fromNatural (arithmetic.BIT2 0)) z = real./ y z
⊦ ∀y z.
real./ (fromNatural (arithmetic.BIT2 0)) y *
real./ z (fromNatural (arithmetic.BIT2 0)) = real./ z y
⊦ ∀c. ¬(c = 0) ⇒ ∀n. realax.inv (c ↑ n) = realax.inv c ↑ n
⊦ ∀x.
¬(x = 0) ⇒
lim.diffl (λx. realax.inv x) (~(realax.inv x ↑ arithmetic.BIT2 0)) x
⊦ ∀m x e. topology.B m (x, e) = λy. topology.dist m (x, y) < e
⊦ ∀f n. real.sum (n, arithmetic.BIT2 0) f = f n + f (n + 1)
⊦ ∀d a b. transc.division (a, b) d ⇒ ∀n. d n ≤ d (suc n)
⊦ ∀f l x. lim.tends_real_real f l x ⇔ lim.tends_real_real (λx. f x - l) 0 x
⊦ 0 < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
real./ transc.pi (fromNatural (arithmetic.BIT2 0)) <
fromNatural (arithmetic.BIT2 0)
⊦ ∀a b c. transc.rpow a (b + c) * transc.rpow a (~b) = transc.rpow a c
⊦ ∀x y. (∀e. 0 < e ⇒ x ≤ y + e) ⇒ x ≤ y
⊦ ∀a b. transc.Dint (a, b) (λx. if x = a then 1 else 0) 0
⊦ ∀a b. transc.Dint (a, b) (λx. if x = b then 1 else 0) 0
⊦ ∀x. 0 < x ∧ x < 1 ⇒ 1 < realax.inv x
⊦ ∀D a b. transc.division (a, b) D ⇒ (a = b ⇔ transc.dsize D = 0)
⊦ ∀p z. p z ∧ (∀x. p x ⇒ z ≤ x) ⇒ real.inf p = z
⊦ ∀p z. p z ∧ (∀r. p r ⇒ r ≤ z) ⇒ real.sup p = z
⊦ ∀n d. 1 < n ⇒ (d < fromNatural n * d ⇔ 0 < d)
⊦ ∀n d. 1 < n ⇒ (real./ d (fromNatural n) < d ⇔ 0 < d)
⊦ ∀n x.
0 ≤ x ⇒
transc.root (suc n) (realax.inv x) = realax.inv (transc.root (suc n) x)
⊦ ∀x y.
transc.cos (x + y) =
transc.cos x * transc.cos y - transc.sin x * transc.sin y
⊦ ∀x y.
transc.sin (x + y) =
transc.sin x * transc.cos y + transc.cos x * transc.sin y
⊦ ∀x y. 0 < x ⇒ (0 < x * y ⇔ 0 < y)
⊦ ∀y z. 0 < z ⇒ (0 < real./ y z ⇔ 0 < y)
⊦ ∀x y. 0 < y ⇒ (0 < x * y ⇔ 0 < x)
⊦ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0
⊦ ∀x y. 0 ≤ x ∧ x < y ⇒ real./ x y < 1
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < real./ x y
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y
⊦ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y
⊦ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y
⊦ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ real./ x y
⊦ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
⊦ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y
⊦ ∀x y. x ↑ arithmetic.BIT2 0 = y ∧ 0 ≤ x ⇒ x = transc.sqrt y
⊦ ∀r.
intreal.INT_CEILING r =
bool.LET
(λi.
if intreal.real_of_int i = r then i
else integer.int_add i (integer.int_of_num 1))
(intreal.INT_FLOOR r)
⊦ ∀y. transc.acs y = select x. 0 ≤ x ∧ x ≤ transc.pi ∧ transc.cos x = y
⊦ ∀y. ¬(y = 0) ⇒ ∀x. abs (real./ x y) = real./ (abs x) (abs y)
⊦ ∀x. abs x < 1 ⇒ seq.sums (λn. x ↑ n) (realax.inv (1 - x))
⊦ ∀p1 p2.
poly.poly (poly.diff (poly.poly_mul p1 p2)) =
poly.poly
(poly.poly_add (poly.poly_mul p1 (poly.diff p2))
(poly.poly_mul (poly.diff p1) p2))
⊦ ∀p.
¬(poly.poly p = poly.poly []) ⇒
pred_set.FINITE (pred_set.GSPEC (λx. (x, poly.poly p x = 0)))
⊦ ∀f m n. abs (real.sum (m, n) f) ≤ real.sum (m, n) (λn. abs (f n))
⊦ ∀f n d. real.sum (n, d) (λn. ~f n) = ~real.sum (n, d) f
⊦ ∀P. real.sup P = select s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
⊦ ∀f l m x. lim.diffl f l x ∧ lim.diffl f m x ⇒ l = m
⊦ ∀f l m x. lim.tends_real_real f l x ∧ lim.tends_real_real f m x ⇒ l = m
⊦ ∀f g x. lim.contl f x ∧ lim.contl g (f x) ⇒ lim.contl (λx. g (f x)) x
⊦ poly.## c [] = [] ∧ poly.## c (h :: t) = c * h :: poly.## c t
⊦ 0 ≤ x ∧ 0 < y ⇒ fromNatural (real.NUM_FLOOR (real./ x y)) * y ≤ x
⊦ ∀d n p.
poly.poly (poly.poly_exp p (n + d)) =
poly.poly (poly.poly_mul (poly.poly_exp p n) (poly.poly_exp p d))
⊦ ∀n.
even n ⇒
transc.sqrt (fromNatural (arithmetic.BIT2 0) ↑ n) =
fromNatural (arithmetic.BIT2 0) ↑ (n div arithmetic.BIT2 0)
⊦ ∀x k p. abs x ≤ k ⇒ abs (poly.poly p x) ≤ poly.poly (map abs p) k
⊦ ∀x.
transc.cos (fromNatural (arithmetic.BIT2 0) * x) =
transc.cos x ↑ arithmetic.BIT2 0 - transc.sin x ↑ arithmetic.BIT2 0
⊦ ∀y.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) < transc.atn y ∧
transc.atn y < real./ transc.pi (fromNatural (arithmetic.BIT2 0))
⊦ ∀x.
0 < x ∧ x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
0 < transc.cos x
⊦ ∀x.
0 < x ∧ x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
0 < transc.sin x
⊦ ∀x.
0 < x ∧ x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
0 < transc.tan x
⊦ ∀x.
0 ≤ x ∧ x ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
0 ≤ transc.cos x
⊦ ∀x.
0 ≤ x ∧ x ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
0 ≤ transc.sin x
⊦ ∀y. ~1 ≤ y ∧ y ≤ 1 ⇒ transc.cos (transc.acs y) = y
⊦ ∀y. ~1 ≤ y ∧ y ≤ 1 ⇒ transc.sin (transc.asn y) = y
⊦ ∀p1 p2 n.
poly.poly (poly.poly_diff_aux n (poly.poly_add p1 p2)) =
poly.poly
(poly.poly_add (poly.poly_diff_aux n p1) (poly.poly_diff_aux n p2))
⊦ ∀m x e. 0 < e ⇒ topology.neigh (topology.mtop m) (topology.B m (x, e), x)
⊦ ∀x x0.
seq.--> x x0 ∧ ¬(x0 = 0) ⇒
seq.--> (λn. realax.inv (x n)) (realax.inv x0)
⊦ ∀f.
seq.summable f ⇒
∀k. seq.sums (λn. f (n + k)) (seq.suminf f - real.sum (0, k) f)
⊦ ∀P. (∃x. P x) ⇒ ∃d x. (let x ← x in P (x + d)) ∧ 0 < x
⊦ ∀f l x0.
lim.tends_real_real f l x0 ⇔
nets.tends f l
(topology.mtop topology.mr1, nets.tendsto (topology.mr1, x0))
⊦ ∀f x. lim.contl f x ∧ ¬(f x = 0) ⇒ lim.contl (λx. realax.inv (f x)) x
⊦ ∀n d. ¬(n = 0) ⇒ (0 < real./ d (fromNatural n) ⇔ 0 < d)
⊦ ∀n x.
0 < x ⇒
transc.root (suc n) x =
transc.exp (real./ (transc.ln x) (fromNatural (suc n)))
⊦ ∀n x.
0 < x ⇒
transc.exp (real./ (transc.ln x) (fromNatural (suc n))) ↑ suc n = x
⊦ ∀a b c. a ≤ b ⇒ integral.integral (a, b) (λx. c) = c * (b - a)
⊦ ∀a b c. transc.Dint (a, b) (λx. if x = c then 1 else 0) 0
⊦ ∀y z. real./ (real./ y 3) (real./ z 3) = real./ y z
⊦ ∀y z. real./ y 3 * real./ 3 z = real./ y z
⊦ ∀y z. real./ 3 y * real./ z 3 = real./ z y
⊦ ∀p n. all (λc. c = 0) (poly.poly_diff_aux (suc n) p) ⇔ all (λc. c = 0) p
⊦ ∀P.
pred_set.FINITE P ⇒
∀f c.
real_sigma.REAL_SUM_IMAGE (λx. c * f x) P =
c * real_sigma.REAL_SUM_IMAGE f P
⊦ ∀P.
pred_set.FINITE P ⇒
real_sigma.REAL_SUM_IMAGE (λs. if bool.IN s P then 1 else 0) P =
fromNatural (pred_set.CARD P)
⊦ ∀f. (∀n. 0 ≤ f n) ⇒ ∀m n. 0 ≤ real.sum (m, n) f
⊦ ∀p z. (∃r. p r) ∧ real.inf p < z ⇒ ∃x. p x ∧ x < z
⊦ ∀p r. (∃r. p r) ∧ (∀x. p x ⇒ r ≤ x) ⇒ r ≤ real.inf p
⊦ ∀p x. (∃r. p r) ∧ (∀r. p r ⇒ r ≤ x) ⇒ real.sup p ≤ x
⊦ ∀g m x.
lim.diffl g m x ⇒
lim.diffl (λx. transc.exp (g x)) (transc.exp (g x) * m) x
⊦ ∀f g x. lim.contl f x ∧ lim.contl g x ⇒ lim.contl (λx. f x * g x) x
⊦ ∀f g x. lim.contl f x ∧ lim.contl g x ⇒ lim.contl (λx. f x + g x) x
⊦ ∀f g x. lim.contl f x ∧ lim.contl g x ⇒ lim.contl (λx. f x - g x) x
⊦ ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x ↑ n ≤ y ↑ n
⊦ ∀a b c. 0 < a ⇒ transc.rpow (transc.rpow a b) c = transc.rpow a (b * c)
⊦ ∀x y z. 0 < x ⇒ (x * y < x * z ⇔ y < z)
⊦ ∀x y z. 0 < x ⇒ (x * y ≤ x * z ⇔ y ≤ z)
⊦ ∀x y z. 0 < z ⇒ (x = real./ y z ⇔ x * z = y)
⊦ ∀x y z. 0 < z ⇒ (x < real./ y z ⇔ x * z < y)
⊦ ∀x y z. 0 < z ⇒ (x ≤ real./ y z ⇔ x * z ≤ y)
⊦ ∀x y z. 0 < z ⇒ (real./ x z = y ⇔ x = y * z)
⊦ ∀x y z. 0 < z ⇒ (real./ x z < y ⇔ x < y * z)
⊦ ∀x y z. 0 < z ⇒ (real./ x z ≤ y ⇔ x ≤ y * z)
⊦ ∀x y z. 0 < z ⇒ (real./ x z < real./ y z ⇔ x < y)
⊦ ∀x y z. 0 < z ⇒ (x * z < y * z ⇔ x < y)
⊦ ∀x y z. 0 < z ⇒ (x * z ≤ y * z ⇔ x ≤ y)
⊦ ∀x y z. x * y = x * z ⇔ x = 0 ∨ y = z
⊦ ∀x y z. x * z = y * z ⇔ z = 0 ∨ x = y
⊦ ∀x y h. abs h < abs y - abs x ⇒ abs (x + h) < abs y
⊦ ∀x y z. x < y ∧ 0 < z ⇒ x * z < y * z
⊦ ∀x y z. y < z ∧ 0 < x ⇒ x * y < x * z
⊦ ∀x y z. x ≤ y ∧ 0 ≤ z ⇒ x * z ≤ y * z
⊦ ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z
⊦ ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ y * x ≤ z * x
⊦ ∀x y z. 0 < x ∧ y ≤ z * x ⇒ real./ y x ≤ z
⊦ ∀x y z. 0 < x ∧ y * x ≤ z ⇒ y ≤ real./ z x
⊦ ∀x y z. x < z ∧ abs (y - x) < z - x ⇒ y < z
⊦ ∀x.
0 ≤ transc.cos x ⇒
transc.cos x = transc.sqrt (1 - transc.sin x ↑ arithmetic.BIT2 0)
⊦ ∀x.
0 ≤ transc.sin x ⇒
transc.sin x = transc.sqrt (1 - transc.cos x ↑ arithmetic.BIT2 0)
⊦ ∀x. x - real./ x 3 = real./ (fromNatural (arithmetic.BIT2 0) * x) 3
⊦ ∀S' top.
topology.open top S' ⇔
pred_set.BIGUNION
(pred_set.GSPEC
(λP. (P, topology.open top P ∧ pred_set.SUBSET P S'))) = S'
⊦ ∀P.
pred_set.FINITE P ⇒
∀f.
real_sigma.REAL_SUM_IMAGE f P =
real_sigma.REAL_SUM_IMAGE (λx. if bool.IN x P then f x else 0) P
⊦ ∀%%genvar%%1142.
pred_set.FINITE %%genvar%%1142 ⇒
∀f.
real_sigma.REAL_SUM_IMAGE f
(pred_set.INTER %%genvar%%1142 (λp. ¬(f p = 0))) =
real_sigma.REAL_SUM_IMAGE f %%genvar%%1142
⊦ ∀f k.
seq.summable f ∧ 0 < k ⇒
seq.sums (λn. real.sum (n * k, k) f) (seq.suminf f)
⊦ ∀f. seq.mono f ⇔ (∀n. f (suc n) ≥ f n) ∨ ∀n. f (suc n) ≤ f n
⊦ ∀f c l x. lim.diffl f l x ⇒ lim.diffl (λx. c * f x) (c * l) x
⊦ ∀f a b.
integral.integrable (a, b) f ⇒
transc.Dint (a, b) f (integral.integral (a, b) f)
⊦ ∀%%genvar%%4008 i.
intreal.INT_CEILING %%genvar%%4008 = i ⇔
intreal.real_of_int (integer.int_sub i (integer.int_of_num 1)) <
%%genvar%%4008 ∧ %%genvar%%4008 ≤ intreal.real_of_int i
⊦ ∀r i.
intreal.INT_FLOOR r = i ⇔
intreal.real_of_int i ≤ r ∧
r < intreal.real_of_int (integer.int_add i (integer.int_of_num 1))
⊦ ∀a n. 0 < a ⇒ transc.rpow a (fromNatural n + 1) = a ↑ suc n
⊦ ∀a b c d. a + b - (c + d) = a - c + (b - d)
⊦ ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z
⊦ ∀w x y z. w < x ∧ y ≤ z ⇒ w + y < x + z
⊦ ∀w x y z. w ≤ x ∧ y < z ⇒ w + y < x + z
⊦ ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z
⊦ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2
⊦ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2
⊦ ∀x t. 0 < x ⇒ real./ (transc.rpow x t) x = transc.rpow x (t - 1)
⊦ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ transc.root (suc n) x ≤ transc.root (suc n) y
⊦ ∀h t.
poly.poly (h :: t) = poly.poly [] ⇒ h = 0 ∧ poly.poly t = poly.poly []
⊦ ∀p n.
poly.poly (poly.diff (poly.poly_exp p (suc n))) =
poly.poly
(poly.poly_mul (poly.## (fromNatural (suc n)) (poly.poly_exp p n))
(poly.diff p))
⊦ ∀p n.
poly.poly (poly.poly_exp p n) = poly.poly [] ⇔
poly.poly p = poly.poly [] ∧ ¬(n = 0)
⊦ ∀p q m n.
poly.poly_divides (poly.poly_exp p n) q ∧ m ≤ n ⇒
poly.poly_divides (poly.poly_exp p m) q
⊦ ∀p.
poly.rsquarefree p ⇔
∀a. ¬(poly.poly p a = 0 ∧ poly.poly (poly.diff p) a = 0)
⊦ ∀s f z.
pred_set.FINITE s ⇒
real_sigma.REAL_SUM_IMAGE f s =
real_sigma.REAL_SUM_IMAGE (λx. if bool.IN x s then f x else z) s
⊦ ∀D a b n. transc.division (a, b) D ∧ n < transc.dsize D ⇒ D n < b
⊦ ∀d a b. transc.division (a, b) d ⇒ ∀n. a ≤ d n ∧ d n ≤ b
⊦ ∀f k k'. (∀n. k ≤ f n ∧ f n ≤ k') ⇒ nets.bounded (topology.mr1, (≥)) f
⊦ poly.diff [] = [] ∧ poly.diff (c :: []) = [] ∧
poly.diff (h :: t) = poly.poly_diff_aux 1 t
⊦ ∀m n x. 1 < x ∧ m < n ⇒ x ↑ m < x ↑ n
⊦ ∀m n x. 1 ≤ x ∧ m ≤ n ⇒ x ↑ m ≤ x ↑ n
⊦ ∀m n. real.sum (m, n) (λi. d (suc i) - d i) = d (m + n) - d m
⊦ ∀x y z. ¬(x = 0) ⇒ (y = z ⇔ x * y = x * z)
⊦ ∀x y z. ¬(x = 0) ⇒ real./ (real./ y x) (real./ z x) = real./ y z
⊦ ∀c a b. ¬(c = 0) ⇒ real./ (c * a) (c * b) = real./ a b
⊦ ∀c a b. ¬(c = 0) ⇒ real./ (a * c) (b * c) = real./ a b
⊦ ∀x y z. ¬(x = 0) ⇒ real./ x y * real./ z x = real./ z y
⊦ ∀x y z. ¬(x = 0) ⇒ real./ y x * real./ x z = real./ y z
⊦ ∀a b c. 1 < a ⇒ (transc.rpow a b < transc.rpow a c ⇔ b < c)
⊦ ∀a b c. 1 < a ⇒ (transc.rpow a b ≤ transc.rpow a c ⇔ b ≤ c)
⊦ ∀x y z. x < z ∧ topology.dist topology.mr1 (x, y) < z - x ⇒ y < z
⊦ ∀x y z. ¬(x = 0) ∧ x * y = x * z ⇒ y = z
⊦ ∀x y z. ¬(z = 0) ∧ x * z = y * z ⇒ x = y
⊦ ∀c. c ≤ 0 ⇒ ∀x y. abs x ≤ c * abs y ⇒ x = 0
⊦ ∀x. ~1 < x ∧ x < 1 ⇒ ¬(transc.cos (transc.asn x) = 0)
⊦ ∀x. ~1 < x ∧ x < 1 ⇒ ¬(transc.sin (transc.acs x) = 0)
⊦ ∀x.
~1 < x ∧ x < 1 ⇒
lim.diffl transc.asn (realax.inv (transc.cos (transc.asn x))) x
⊦ ∀f m n.
abs (real.sum (m, n) (λn. abs (f n))) = real.sum (m, n) (λn. abs (f n))
⊦ ∀f n. (∀m. n ≤ m ⇒ f m = 0) ⇒ seq.sums f (real.sum (0, n) f)
⊦ ∀f g.
(∀n. f n ≤ g n) ∧ seq.summable f ∧ seq.summable g ⇒
seq.suminf f ≤ seq.suminf g
⊦ ∀f. (∀y. ∃N. ∀n. n ≥ N ⇒ f n > y) ⇒ seq.--> (λn. realax.inv (f n)) 0
⊦ ∀x y. (x ≤ y ⇒ max x y = y) ∧ (y ≤ x ⇒ max x y = x)
⊦ ∀x y. (x ≤ y ⇒ min x y = x) ∧ (y ≤ x ⇒ min x y = y)
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ (transc.ln x = transc.ln y ⇔ x = y)
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ (realax.inv x < realax.inv y ⇔ y < x)
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ (transc.ln x < transc.ln y ⇔ x < y)
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ (transc.ln x ≤ transc.ln y ⇔ x ≤ y)
⊦ ∀p a.
poly.poly p a = 0 ⇔
poly.poly p = poly.poly [] ∨ ¬(poly.poly_order a p = 0)
⊦ ∀p q.
poly.poly (poly.poly_mul p q) = poly.poly [] ⇔
poly.poly p = poly.poly [] ∨ poly.poly q = poly.poly []
⊦ ∀top N x.
topology.neigh top (N, x) ⇔
∃P. topology.open top P ∧ pred_set.SUBSET P N ∧ P x
⊦ ∀S' top.
topology.open top S' ⇔
∀x. S' x ⇒ ∃N. topology.neigh top (N, x) ∧ pred_set.SUBSET N S'
⊦ ∀f g. (∃N. ∀n. n ≥ N ⇒ abs (f n) ≤ g n) ∧ seq.summable g ⇒ seq.summable f
⊦ z = real./ x y ⇔
if y = 0 then z = marker.unint (real./ x y) else y * z = x
⊦ real./ x y = z ⇔
if y = 0 then marker.unint (real./ x y) = z else x = y * z
⊦ x * real./ y z =
if z = 0 then x * marker.unint (real./ y z) else real./ (x * y) z
⊦ real./ x y * z =
if y = 0 then marker.unint (real./ x y) * z else real./ (x * z) y
⊦ 0 ≤ x ∧ 0 < y ⇒ x < fromNatural (real.NUM_FLOOR (real./ x y) + 1) * y
⊦ ∀n x y. 0 ≤ x ∧ x < y ⇒ x ↑ suc n < y ↑ suc n
⊦ ∀x z d. x - d ≤ z ∧ z ≤ x + d ⇔ abs (z - x) ≤ d
⊦ ∀x y.
0 < x ⇒ lim.diffl (λx. transc.rpow x y) (y * transc.rpow x (y - 1)) x
⊦ ∀x.
~1 < x ∧ x < 1 ⇒
lim.diffl transc.acs (realax.inv (~transc.sin (transc.acs x))) x
⊦ ∀f m k n. real.sum (m + k, n) f = real.sum (m, n) (λr. f (r + k))
⊦ ∀f c m n. real.sum (m, n) (λn. c * f n) = c * real.sum (m, n) f
⊦ ∀d a b. transc.division (a, b) d ⇒ ∀m n. m ≤ n ⇒ d m ≤ d n
⊦ ∀f g.
(∀n. abs (f n) ≤ g n) ∧ seq.summable g ⇒
seq.summable f ∧ seq.suminf f ≤ seq.suminf g
⊦ ∀f.
nets.bounded (topology.mr1, (≥)) f ∧ (∀m n. m ≥ n ⇒ f m ≥ f n) ⇒
seq.convergent f
⊦ ∀f a b i. transc.Dint (a, b) f i ⇒ transc.Dint (a, b) (λx. ~f x) (~i)
⊦ (∀n. n < 0 ⇔ ⊥) ∧ ∀m n. m < suc n ⇔ m = n ∨ m < n
⊦ (∀x. x ↑ 0 = 1) ∧ ∀x n. x ↑ suc n = x * x ↑ n
⊦ ∀a b d n. transc.division (a, b) d ∧ d (suc n) = d n ⇒ transc.dsize d ≤ n
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ transc.ln (real./ x y) = transc.ln x - transc.ln y
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ transc.ln (x * y) = transc.ln x + transc.ln y
⊦ ∀x y.
0 ≤ x ∧ 0 ≤ y ⇒
transc.sqrt (real./ x y) = real./ (transc.sqrt x) (transc.sqrt y)
⊦ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ transc.sqrt (x * y) = transc.sqrt x * transc.sqrt y
⊦ ∀x y. x * x + y * y = 0 ⇔ x = 0 ∧ y = 0
⊦ ∀r.
real.NUM_CEILING r =
bool.LET (λn. if r ≤ 0 ∨ r = fromNatural n then n else n + 1)
(real.NUM_FLOOR r)
⊦ ∀m x y z.
topology.dist m (x, z) ≤
topology.dist m (x, y) + topology.dist m (y, z)
⊦ ∀S' top.
topology.open top S' ⇔
∀x. S' x ⇒ ∃P. P x ∧ topology.open top P ∧ pred_set.SUBSET P S'
⊦ ∀s f f'.
pred_set.FINITE s ⇒
real_sigma.REAL_SUM_IMAGE (λx. f x - f' x) s =
real_sigma.REAL_SUM_IMAGE f s - real_sigma.REAL_SUM_IMAGE f' s
⊦ ∀P.
pred_set.FINITE P ⇒
∀f x.
(∀y. f y = x) ⇒
real_sigma.REAL_SUM_IMAGE f P = fromNatural (pred_set.CARD P) * x
⊦ ∀s.
pred_set.FINITE s ⇒
∀f f'.
real_sigma.REAL_SUM_IMAGE (λx. f x + f' x) s =
real_sigma.REAL_SUM_IMAGE f s + real_sigma.REAL_SUM_IMAGE f' s
⊦ ∀f n d. real.sum (n, d) (λn. f (suc n) - f n) = f (n + d) - f n
⊦ ∀f x n. (∀n. f n ≤ f (n + 1)) ∧ seq.--> f x ⇒ f n ≤ x
⊦ ∀f x n. (∀n. f (n + 1) ≤ f n) ∧ seq.--> f x ⇒ x ≤ f n
⊦ ∀D a b.
transc.division (a, b) D ⇒ ∀n. n < transc.dsize D ⇒ D 0 < D (suc n)
⊦ ∀D a b.
transc.division (a, b) D ⇒
∀n. n < transc.dsize D ⇒ D n < D (transc.dsize D)
⊦ ∀D a b.
transc.division (a, b) D ∧ ¬(transc.dsize D = 0) ⇒ ∀n. a < D (suc n)
⊦ ∀p e. (∃r. p r) ∧ 0 < e ⇒ ∃x. p x ∧ x < real.inf p + e
⊦ ∀f l x.
lim.diffl f l x ⇔
lim.tends_real_real (λh. real./ (f (x + h) - f x) h) l 0
⊦ ∀f l x.
lim.tends_real_real f l x ∧ ¬(l = 0) ⇒
lim.tends_real_real (λx. realax.inv (f x)) (realax.inv l) x
⊦ ∀f a b.
(∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒ integral.integrable (a, b) f
⊦ ∀g x x0.
nets.tends x x0 (topology.mtop topology.mr1, g) ⇒
nets.tends (λn. abs (x n)) (abs x0) (topology.mtop topology.mr1, g)
⊦ ∀n x. transc.root n x = select u. (0 < x ⇒ 0 < u) ∧ u ↑ n = x
⊦ ∀x.
0 ≤ x ∧ x ≤ transc.pi ⇒
transc.sin x = transc.sqrt (1 - transc.cos x ↑ arithmetic.BIT2 0)
⊦ ∀x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) < x ∧
x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
0 < transc.cos x
⊦ ∀x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) < x ∧
x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
transc.atn (transc.tan x) = x
⊦ ∀x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ≤ x ∧
x ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
0 ≤ transc.cos x
⊦ ∀x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ≤ x ∧
x ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
transc.asn (transc.sin x) = x
⊦ ∀x.
(transc.sin (~x) + transc.sin x) ↑ arithmetic.BIT2 0 +
(transc.cos (~x) - transc.cos x) ↑ arithmetic.BIT2 0 = 0
⊦ ∀f s.
pred_set.FINITE s ∧ (∀x. bool.IN x s ⇒ 0 ≤ f x) ⇒
0 ≤ real_sigma.REAL_SUM_IMAGE f s
⊦ ∀f m n. real.sum (m, n) f = real.sum (0, m + n) f - real.sum (0, m) f
⊦ ∀f n p. real.sum (0, n) f + real.sum (n, p) f = real.sum (0, n + p) f
⊦ ∀x x0 y y0.
seq.--> x x0 ∧ seq.--> y y0 ⇒ seq.--> (λn. x n * y n) (x0 * y0)
⊦ ∀x x0 y y0.
seq.--> x x0 ∧ seq.--> y y0 ⇒ seq.--> (λn. x n + y n) (x0 + y0)
⊦ ∀x x0 y y0.
seq.--> x x0 ∧ seq.--> y y0 ⇒ seq.--> (λn. x n - y n) (x0 - y0)
⊦ ∀x x0 y y0.
seq.sums x x0 ∧ seq.sums y y0 ⇒ seq.sums (λn. x n + y n) (x0 + y0)
⊦ ∀x x0 y y0.
seq.sums x x0 ∧ seq.sums y y0 ⇒ seq.sums (λn. x n - y n) (x0 - y0)
⊦ transc.pi =
fromNatural (arithmetic.BIT2 0) *
select x. 0 ≤ x ∧ x ≤ fromNatural (arithmetic.BIT2 0) ∧ transc.cos x = 0
⊦ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) =
select x. 0 ≤ x ∧ x ≤ fromNatural (arithmetic.BIT2 0) ∧ transc.cos x = 0
⊦ ∀n k f.
real.sum (0, n) (λm. real.sum (m * k, k) f) = real.sum (0, n * k) f
⊦ ∀m n.
fromNatural m - fromNatural n =
if arithmetic.- m n = 0 then ~fromNatural (arithmetic.- n m)
else fromNatural (arithmetic.- m n)
⊦ ∀n f c.
real.sum (0, n) f - fromNatural n * c = real.sum (0, n) (λp. f p - c)
⊦ ∀x n. 0 ≤ x ⇒ 1 + fromNatural n * x ≤ (1 + x) ↑ n
⊦ ∀w x y z. abs w < y ∧ abs x < z ⇒ abs (w * x) < y * z
⊦ ∀a b d n.
transc.division (a, b) d ∧ d n < d (suc n) ⇒ suc n ≤ transc.dsize d
⊦ ∀x y. 0 ≤ x ∧ 0 ≤ y ∧ y ↑ arithmetic.BIT2 0 = x ⇒ transc.sqrt x = y
⊦ ∀y.
∃!x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) < x ∧
x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
transc.tan x = y
⊦ ∀e. 0 < e ⇒ ∀n. 1 + fromNatural n * e ≤ (1 + e) ↑ n
⊦ ∀d. (∃z. ∀x. P x ⇒ x < z) ⇒ ∃z. ∀x. (let x ← x in P (x + d)) ⇒ x < z
⊦ ∀t h.
∃q r.
h :: t = poly.poly_add (r :: []) (poly.poly_mul (~a :: 1 :: []) q)
⊦ ∀a s.
pred_set.FINITE s ⇒
real_sigma.REAL_SUM_IMAGE a s ↑ arithmetic.BIT2 0 =
real_sigma.REAL_SUM_IMAGE (pair.UNCURRY (λi j. a i * a j))
(pred_set.CROSS s s)
⊦ ∀f m. (∀n. m ≤ n ⇒ 0 ≤ f n) ⇒ ∀n. 0 ≤ real.sum (m, n) f
⊦ ∀f a b i. a ≤ b ∧ transc.Dint (a, b) f i ⇒ integral.integral (a, b) f = i
⊦ ∀g x x0.
nets.tends x x0 (topology.mtop topology.mr1, g) ⇔
nets.tends (λn. x n - x0) 0 (topology.mtop topology.mr1, g)
⊦ x + real./ y z =
if z = 0 then x + marker.unint (real./ y z) else real./ (x * z + y) z
⊦ real./ x y + z =
if y = 0 then marker.unint (real./ x y) + z else real./ (x + z * y) y
⊦ x < real./ u (fromNatural m) ⇔
if m = 0 then x < marker.unint (real./ u 0) else fromNatural m * x < u
⊦ x ≤ real./ u (fromNatural m) ⇔
if m = 0 then x ≤ marker.unint (real./ u 0) else fromNatural m * x ≤ u
⊦ real./ x (fromNatural n) < u ⇔
if n = 0 then marker.unint (real./ x 0) < u else x < fromNatural n * u
⊦ real./ x (fromNatural n) ≤ u ⇔
if n = 0 then marker.unint (real./ x 0) ≤ u else x ≤ fromNatural n * u
⊦ ∀x.
¬(transc.cos x = 0) ⇒
1 + transc.tan x ↑ arithmetic.BIT2 0 =
realax.inv (transc.cos x) ↑ arithmetic.BIT2 0
⊦ ∀y. ~1 < y ∧ y < 1 ⇒ 0 < transc.acs y ∧ transc.acs y < transc.pi
⊦ ∀y. ~1 ≤ y ∧ y ≤ 1 ⇒ 0 ≤ transc.acs y ∧ transc.acs y ≤ transc.pi
⊦ ∀f g.
(∃N. ∀n. n ≥ N ⇒ abs (f n) ≤ g n) ∧ seq.summable g ⇒
seq.summable (λk. abs (f k))
⊦ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒ ∀y. P y ⇒ y ≤ real.sup P
⊦ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒ ∀y. P y ⇒ y ≤ real.sup P
⊦ ∀f a b c.
a ≤ b ∧ integral.integrable (a, b) f ⇒
integral.integrable (a, b) (λx. c * f x)
⊦ (∀p. poly.poly_exp p 0 = 1 :: []) ∧
∀p n. poly.poly_exp p (suc n) = poly.poly_mul p (poly.poly_exp p n)
⊦ ∀x y.
¬(x = 0) ∧ ¬(y = 0) ⇒ realax.inv (x * y) = realax.inv x * realax.inv y
⊦ ∀y.
0 < y ⇒
∃x.
0 < x ∧ x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
y < transc.tan x
⊦ ∀y.
0 ≤ y ⇒
∃x.
0 ≤ x ∧ x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
transc.tan x = y
⊦ ∀x.
seq.sums
(λn.
real./ (~1 ↑ n)
(fromNatural (factorial (arithmetic.BIT2 0 * n))) *
x ↑ (arithmetic.BIT2 0 * n)) (transc.cos x)
⊦ ∀l n x.
lim.diffl (λx. x ↑ suc n * poly.poly l x)
(x ↑ n * poly.poly (poly.poly_diff_aux (suc n) l) x) x
⊦ ∀p q.
¬(poly.poly p = poly.poly []) ∧ ¬(poly.poly q = poly.poly []) ⇒
¬(poly.poly (poly.poly_mul p q) = poly.poly [])
⊦ ∀p.
poly.rsquarefree p ⇔
¬(poly.poly p = poly.poly []) ∧
∀a. poly.poly_order a p = 0 ∨ poly.poly_order a p = 1
⊦ ∀E g1 g2.
transc.gauge E g1 ∧ transc.gauge E g2 ⇒
transc.gauge E (λx. if g1 x < g2 x then g1 x else g2 x)
⊦ ∀f a b c.
a ≤ c ∧ c ≤ b ∧ integral.integrable (a, b) f ⇒
integral.integrable (a, c) f
⊦ ∀f a b c.
a ≤ c ∧ c ≤ b ∧ integral.integrable (a, b) f ⇒
integral.integrable (c, b) f
⊦ ∀g k x.
nets.tends x 0 (topology.mtop topology.mr1, g) ⇒
nets.tends (λn. k * x n) 0 (topology.mtop topology.mr1, g)
⊦ ∀g d.
nets.dorder g ⇒
nets.tends x x0 (topology.mtop d, g) ∧
nets.tends x x1 (topology.mtop d, g) ⇒ x0 = x1
⊦ (∀c. poly.## c [] = []) ∧
∀c h t. poly.## c (h :: t) = c * h :: poly.## c t
⊦ ∀n x y. ¬(n = 0) ∧ 0 ≤ x ∧ x < y ⇒ x ↑ n < y ↑ n
⊦ ∀y.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) < transc.atn y ∧
transc.atn y < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
transc.tan (transc.atn y) = y
⊦ ∀p q r.
poly.poly (poly.poly_mul p q) = poly.poly (poly.poly_mul p r) ⇔
poly.poly p = poly.poly [] ∨ poly.poly q = poly.poly r
⊦ ∀m.
topology.istopology
(λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. topology.dist m (x, y) < e ⇒ S' y)
⊦ ∀P.
pred_set.FINITE P ⇒
∀f'.
pred_set.INJ f' P (pred_set.IMAGE f' P) ⇒
∀f.
real_sigma.REAL_SUM_IMAGE f (pred_set.IMAGE f' P) =
real_sigma.REAL_SUM_IMAGE (f ∘ f') P
⊦ ∀f n p. real.sum (m, n) f + real.sum (m + n, p) f = real.sum (m, n + p) f
⊦ ∀f n.
seq.summable f ∧ (∀m. n ≤ m ⇒ 0 < f m) ⇒
real.sum (0, n) f < seq.suminf f
⊦ ∀f n.
seq.summable f ∧ (∀m. n ≤ m ⇒ 0 ≤ f m) ⇒
real.sum (0, n) f ≤ seq.suminf f
⊦ ∀p r. (∃y. ∀z. p z ⇒ y ≤ z) ∧ (∃x. p x ∧ x ≤ r) ⇒ real.inf p ≤ r
⊦ ∀f g x0 l.
lim.tends_real_real (λx. f x - g x) 0 x0 ∧ lim.tends_real_real g l x0 ⇒
lim.tends_real_real f l x0
⊦ (∀r. m ≤ r ∧ r < m + n ⇒ f r = 0) ⇒ real.sum (m, n) f = 0
⊦ ∀y. 1 ≤ y ⇒ ∃x. 0 ≤ x ∧ x ≤ y - 1 ∧ transc.exp x = y
⊦ ∀s f f'.
pred_set.FINITE s ∧ (∀x. bool.IN x s ⇒ f x = f' x) ⇒
real_sigma.REAL_SUM_IMAGE f s = real_sigma.REAL_SUM_IMAGE f' s
⊦ ∀P.
pred_set.FINITE P ⇒
∀f f'.
(∀x. bool.IN x P ⇒ f x ≤ f' x) ⇒
real_sigma.REAL_SUM_IMAGE f P ≤ real_sigma.REAL_SUM_IMAGE f' P
⊦ ∀P.
¬(P = pred_set.EMPTY) ∧ pred_set.FINITE P ⇒
real_sigma.REAL_SUM_IMAGE
(λs.
if bool.IN s P then realax.inv (fromNatural (pred_set.CARD P))
else 0) P = 1
⊦ ∀D p f.
transc.rsum (D, p) f =
real.sum (0, transc.dsize D) (λn. f (p n) * (D (suc n) - D n))
⊦ ∀f a b c i.
transc.Dint (a, b) f i ⇒ transc.Dint (a, b) (λx. c * f x) (c * i)
⊦ ∀g m x.
lim.diffl g m x ∧ 0 < g x ⇒
lim.diffl (λx. transc.ln (g x)) (realax.inv (g x) * m) x
⊦ ∀g x x0.
nets.tends x x0 (topology.mtop topology.mr1, g) ∧ ¬(x0 = 0) ⇒
nets.bounded (topology.mr1, g) (λn. realax.inv (x n))
⊦ ∀g.
nets.dorder g ⇒
∀x x0.
nets.tends x x0 (topology.mtop topology.mr1, g) ⇔
nets.tends (λn. ~x n) (~x0) (topology.mtop topology.mr1, g)
⊦ ∀f s s'.
pred_set.FINITE s ∧ pred_set.FINITE s' ⇒
real_sigma.REAL_SUM_IMAGE (λx. real_sigma.REAL_SUM_IMAGE (f x) s') s =
real_sigma.REAL_SUM_IMAGE (λx. real_sigma.REAL_SUM_IMAGE (λy. f y x) s)
s'
⊦ (∀x. poly.poly [] x = 0) ∧
∀h t x. poly.poly (h :: t) x = h + x * poly.poly t x
⊦ ∀x y. 0 < x ∧ 0 < y ⇒ ∃z. 0 < z ∧ z < x ∧ z < y
⊦ ∀a p q.
¬(poly.poly (poly.poly_mul p q) = poly.poly []) ⇒
poly.poly_order a (poly.poly_mul p q) =
poly.poly_order a p + poly.poly_order a q
⊦ ∀f x z.
seq.summable (λn. f n * x ↑ n) ∧ abs z < abs x ⇒
seq.summable (λn. f n * z ↑ n)
⊦ ∀g f.
nets.bounded (topology.mr1, g) f ⇔
∃k N. g N N ∧ ∀n. g n N ⇒ abs (f n) < k
⊦ ∀y.
transc.asn y =
select x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ≤ x ∧
x ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
transc.sin x = y
⊦ ∀y.
transc.atn y =
select x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) < x ∧
x < real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
transc.tan x = y
⊦ ∀x.
0 ≤ x ∧ transc.sin x = 0 ⇒
∃n.
even n ∧
x =
fromNatural n * real./ transc.pi (fromNatural (arithmetic.BIT2 0))
⊦ ∀p a.
¬(poly.poly (poly.diff p) = poly.poly []) ∧
¬(poly.poly_order a p = 0) ⇒
poly.poly_order a p = suc (poly.poly_order a (poly.diff p))
⊦ ∀f n k.
real.sum (0, n) (λr. f (r + k)) =
real.sum (0, n + k) f - real.sum (0, k) f
⊦ ∀g D p.
transc.fine g (D, p) ⇔
∀n. n < transc.dsize D ⇒ D (suc n) - D n < g (p n)
⊦ ∀f g l m x.
lim.diffl f l (g x) ∧ lim.diffl g m x ⇒
lim.diffl (λx. f (g x)) (l * m) x
⊦ ∀f g x.
lim.contl f x ∧ lim.contl g x ∧ ¬(g x = 0) ⇒
lim.contl (λx. real./ (f x) (g x)) x
⊦ real./ x (real./ y z) =
if y = 0 ∨ z = 0 then real./ x (marker.unint (real./ y z))
else real./ (x * z) y
⊦ poly.poly_add [] p2 = p2 ∧ poly.poly_add p1 [] = p1 ∧
poly.poly_add (h1 :: t1) (h2 :: t2) = h1 + h2 :: poly.poly_add t1 t2
⊦ (∀n. poly.poly_diff_aux n [] = []) ∧
∀n h t.
poly.poly_diff_aux n (h :: t) =
fromNatural n * h :: poly.poly_diff_aux (suc n) t
⊦ ∀n x y. 0 ≤ x ∧ 0 ≤ y ∧ y ↑ suc n = x ⇒ transc.root (suc n) x = y
⊦ ∀n x y. 0 ≤ x ∧ 0 ≤ y ∧ x ↑ suc n = y ↑ suc n ⇒ x = y
⊦ ∀a b c.
0 < a ∧ 0 < b ⇒
transc.rpow (real./ a b) c = real./ (transc.rpow a c) (transc.rpow b c)
⊦ ∀a b c.
0 < a ∧ 0 < b ⇒
transc.rpow (a * b) c = transc.rpow a c * transc.rpow b c
⊦ ∀x y d. 0 < d ∧ x - d < y ∧ y < x + d ⇔ abs (y - x) < d
⊦ ∀x z. ¬(x = 0) ∧ ¬(z = 0) ⇒ ∀y. real./ y z = real./ (x * y) (x * z)
⊦ ∀a p.
poly.poly p a = 0 ⇔ p = [] ∨ ∃q. p = poly.poly_mul (~a :: 1 :: []) q
⊦ ∀x.
~1 < x ∧ x < 1 ⇒
lim.diffl transc.asn
(realax.inv (transc.sqrt (1 - x ↑ arithmetic.BIT2 0))) x
⊦ ∀%%genvar%%1021 P'.
pred_set.FINITE %%genvar%%1021 ∧ pred_set.FINITE P' ∧
pred_set.DISJOINT %%genvar%%1021 P' ⇒
∀f.
real_sigma.REAL_SUM_IMAGE f (pred_set.UNION %%genvar%%1021 P') =
real_sigma.REAL_SUM_IMAGE f %%genvar%%1021 +
real_sigma.REAL_SUM_IMAGE f P'
⊦ ∀s s' f.
pred_set.FINITE s ∧ pred_set.FINITE s' ⇒
real_sigma.REAL_SUM_IMAGE (λx. real_sigma.REAL_SUM_IMAGE (f x) s') s =
real_sigma.REAL_SUM_IMAGE (λx. f (fst x) (snd x)) (pred_set.CROSS s s')
⊦ ∀D a b m n.
transc.division (a, b) D ∧ m < n ∧ n ≤ transc.dsize D ⇒ D m < D n
⊦ ∀f x z.
seq.summable (λn. f n * x ↑ n) ∧ abs z < abs x ⇒
seq.summable (λn. abs (f n) * z ↑ n)
⊦ ∀x x0. seq.--> x x0 ⇔ ∀e. 0 < e ⇒ ∃N. ∀n. n ≥ N ⇒ abs (x n - x0) < e
⊦ ∀f g m n.
real.sum (m, n) (λn. f n + g n) = real.sum (m, n) f + real.sum (m, n) g
⊦ ∀f g m n.
real.sum (m, n) (λn. f n - g n) = real.sum (m, n) f - real.sum (m, n) g
⊦ ∀f.
seq.summable f ⇔
∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ⇒ abs (real.sum (m, n) f) < e
⊦ ∀f g l x0.
(∀x. ¬(x = x0) ⇒ f x = g x) ⇒
(lim.tends_real_real f l x0 ⇔ lim.tends_real_real g l x0)
⊦ ∀x y.
¬(x = 0) ∧ ¬(y = 0) ⇒
realax.inv x - realax.inv y = real./ (y - x) (x * y)
⊦ ∀x.
0 ≤ x ∧ transc.cos x = 0 ⇒
∃n.
¬even n ∧
x =
fromNatural n * real./ transc.pi (fromNatural (arithmetic.BIT2 0))
⊦ ∀P. (∃n. P n) ∧ (∃M. ∀x. P x ⇒ x ≤ M) ⇔ ∃m. P m ∧ ∀x. P x ⇒ x ≤ m
⊦ ∀f g l m x.
lim.diffl f l x ∧ lim.diffl g m x ⇒ lim.diffl (λx. f x + g x) (l + m) x
⊦ ∀f g l m x.
lim.diffl f l x ∧ lim.diffl g m x ⇒ lim.diffl (λx. f x - g x) (l - m) x
⊦ ∀f g l m x.
lim.tends_real_real f l x ∧ lim.tends_real_real g m x ⇒
lim.tends_real_real (λx. f x * g x) (l * m) x
⊦ ∀f g l m x.
lim.tends_real_real f l x ∧ lim.tends_real_real g m x ⇒
lim.tends_real_real (λx. f x + g x) (l + m) x
⊦ ∀f g l m x.
lim.tends_real_real f l x ∧ lim.tends_real_real g m x ⇒
lim.tends_real_real (λx. f x - g x) (l - m) x
⊦ ∀a b f k1 k2.
a ≤ b ∧ transc.Dint (a, b) f k1 ∧ transc.Dint (a, b) f k2 ⇒ k1 = k2
⊦ ∀y.
0 < y ⇒
∀x. 0 ≤ x ⇒ ∃n. fromNatural n * y ≤ x ∧ x < fromNatural (suc n) * y
⊦ ∀x.
~1 < x ∧ x < 1 ⇒
lim.diffl transc.acs
(~realax.inv (transc.sqrt (1 - x ↑ arithmetic.BIT2 0))) x
⊦ ∀x.
seq.sums
(λn.
(let n ← n in
if even n then
real./ (~1 ↑ (n div arithmetic.BIT2 0))
(fromNatural (factorial n))
else 0) * x ↑ n) (transc.cos x)
⊦ ∀p a n.
poly.poly_divides (poly.poly_exp (~a :: 1 :: []) n) p ⇔
poly.poly p = poly.poly [] ∨ n ≤ poly.poly_order a p
⊦ ∀m.
topology.mtop m =
topology.topology
(λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. topology.dist m (x, y) < e ⇒ S' y)
⊦ ∀top x S'.
topology.limpt top x S' ⇔
∀N. topology.neigh top (N, x) ⇒ ∃y. ¬(x = y) ∧ S' y ∧ N y
⊦ ∀s.
pred_set.FINITE s ∧ ¬(s = pred_set.EMPTY) ⇒
∀f. (∀x. bool.IN x s ⇒ 0 < f x) ⇒ 0 < real_sigma.REAL_SUM_IMAGE f s
⊦ ∀f.
real_sigma.REAL_SUM_IMAGE f pred_set.EMPTY = 0 ∧
∀e s.
pred_set.FINITE s ⇒
real_sigma.REAL_SUM_IMAGE f (pred_set.INSERT e s) =
f e + real_sigma.REAL_SUM_IMAGE f (pred_set.DELETE s e)
⊦ ∀i N P. (∀x. P x ⇒ ∃n. n < N ∧ x = i n) ⇒ ∃a. ∀x. P x ⇒ x < a
⊦ ∀a b D.
transc.division (a, b) D ⇒
real.sum (0, transc.dsize D) (λn. D (suc n) - D n) - (b - a) = 0
⊦ ∀y. ~1 ≤ y ∧ y ≤ 1 ⇒ ∃!x. 0 ≤ x ∧ x ≤ transc.pi ∧ transc.cos x = y
⊦ ∀p.
¬(poly.poly p = poly.poly []) ⇒
∃i. ∀x. poly.poly p x = 0 ⇒ ∃n. n ≤ length p ∧ x = i n
⊦ ∀%%genvar%%1146.
pred_set.FINITE %%genvar%%1146 ⇒
∀f P'.
(∀x. ¬bool.IN x P' ⇒ f x = 0) ⇒
real_sigma.REAL_SUM_IMAGE f (pred_set.INTER %%genvar%%1146 P') =
real_sigma.REAL_SUM_IMAGE f %%genvar%%1146
⊦ ∀P.
pred_set.FINITE P ⇒
∀f.
(∀x. bool.IN x P ⇒ 0 ≤ f x) ⇒
∀x. bool.IN x P ⇒ f x ≤ real_sigma.REAL_SUM_IMAGE f P
⊦ ∀s.
pred_set.FINITE s ⇒
∀f f'.
(∀x. bool.IN x s ⇒ seq.--> (λn. f n x) (f' x)) ⇒
seq.--> (λn. real_sigma.REAL_SUM_IMAGE (f n) s)
(real_sigma.REAL_SUM_IMAGE f' s)
⊦ ∀f c N.
c < 1 ∧ (∀n. n ≥ N ⇒ abs (f (suc n)) ≤ c * abs (f n)) ⇒ seq.summable f
⊦ ∀D.
transc.dsize D =
select N. (∀n. n < N ⇒ D n < D (suc n)) ∧ ∀n. n ≥ N ⇒ D n = D N
⊦ ∀x.
transc.cos x =
seq.suminf
(λn.
(let n ← n in
if even n then
real./ (~1 ↑ (n div arithmetic.BIT2 0))
(fromNatural (factorial n))
else 0) * x ↑ n)
⊦ ∀p.
¬(poly.poly p = poly.poly []) ⇔
∃N i. ∀x. poly.poly p x = 0 ⇒ ∃n. n < N ∧ x = i n
⊦ ∀p.
¬(poly.poly p = poly.poly []) ⇒
∃N i. ∀x. poly.poly p x = 0 ⇒ ∃n. n < N ∧ x = i n
⊦ ∀%%genvar%%831 P f.
pred_set.FINITE %%genvar%%831 ∧ (∀x. bool.IN x %%genvar%%831 ⇒ P x) ⇒
real_sigma.REAL_SUM_IMAGE (λx. if P x then f x else 0) %%genvar%%831 =
real_sigma.REAL_SUM_IMAGE f %%genvar%%831
⊦ ∀f N. (∀n. n ≥ N ⇒ f n = 0) ⇒ ∀m n. m ≥ N ⇒ real.sum (m, n) f = 0
⊦ ∀x x0 y y0.
seq.--> x x0 ∧ seq.--> y y0 ∧ ¬(y0 = 0) ⇒
seq.--> (λn. real./ (x n) (y n)) (real./ x0 y0)
⊦ ∀f. seq.mono f ⇔ (∀m n. m ≤ n ⇒ f m ≤ f n) ∨ ∀m n. m ≤ n ⇒ f m ≥ f n
⊦ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇔ (∃x. P x) ∧ ∃z. ∀x. P x ⇒ x < z
⊦ ∀f g l m. seq.--> f l ∧ seq.--> g m ∧ (∃N. ∀n. n ≥ N ⇒ f n ≤ g n) ⇒ l ≤ m
⊦ ∀p x.
(∃r. p r) ∧ (∃z. ∀r. p r ⇒ r ≤ z) ∧ (∃r. p r ∧ x ≤ r) ⇒ x ≤ real.sup p
⊦ ∀P.
(∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∀y. (∃x. P x ∧ y < x) ⇔ y < real.sup P
⊦ ∀P.
(∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒
∀y. (∃x. P x ∧ y < x) ⇔ y < real.sup P
⊦ ∀f l x.
lim.diffl f l x ∧ ¬(f x = 0) ⇒
lim.diffl (λx. realax.inv (f x)) (~real./ l (f x ↑ arithmetic.BIT2 0))
x
⊦ ∀n x y.
0 ≤ x ∧ 0 ≤ y ⇒
transc.root (suc n) (real./ x y) =
real./ (transc.root (suc n) x) (transc.root (suc n) y)
⊦ ∀n x y.
0 ≤ x ∧ 0 ≤ y ⇒
transc.root (suc n) (x * y) =
transc.root (suc n) x * transc.root (suc n) y
⊦ ∀z x y. 0 ≤ z ∧ z ≤ 1 ⇒ min x y ≤ z * x + (1 - z) * y
⊦ ∀z x y. 0 ≤ z ∧ z ≤ 1 ⇒ z * x + (1 - z) * y ≤ max x y
⊦ ∀a b c.
0 < a ∧ 0 < c ∧ 0 < b ⇒ (transc.rpow a b < transc.rpow c b ⇔ a < c)
⊦ ∀a b c.
0 < a ∧ 0 < c ∧ 0 < b ⇒ (transc.rpow a b ≤ transc.rpow c b ⇔ a ≤ c)
⊦ ∀y.
~1 ≤ y ∧ y ≤ 1 ⇒
0 ≤ transc.acs y ∧ transc.acs y ≤ transc.pi ∧
transc.cos (transc.acs y) = y
⊦ ∀S' m.
topology.open (topology.mtop m) S' ⇔
∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. topology.dist m (x, y) < e ⇒ S' y
⊦ ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒ ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
⊦ ∀p.
(∃r. p r) ∧ (∃z. ∀r. p r ⇒ r ≤ z) ⇒ ∃!s. ∀y. (∃x. p x ∧ y < x) ⇔ y < s
⊦ ∀f a b c d.
a ≤ c ∧ c ≤ d ∧ d ≤ b ∧ integral.integrable (a, b) f ⇒
integral.integrable (c, d) f
⊦ ∀x1 x2 y1 y2. 0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 < x2 ∧ y1 < y2 ⇒ x1 * y1 < x2 * y2
⊦ ∀x1 x2 y1 y2. 0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≤ x2 ∧ y1 ≤ y2 ⇒ x1 * y1 ≤ x2 * y2
⊦ ∀x.
seq.sums
(λn.
real./ (~1 ↑ n)
(fromNatural (factorial (arithmetic.BIT2 0 * n + 1))) *
x ↑ (arithmetic.BIT2 0 * n + 1)) (transc.sin x)
⊦ ∀f a b c.
a ≤ b ∧ b ≤ c ∧ integral.integrable (a, b) f ∧
integral.integrable (b, c) f ⇒ integral.integrable (a, c) f
⊦ poly.normalize [] = [] ∧
∀h t.
poly.normalize (h :: t) =
if poly.normalize t = [] then if h = 0 then [] else h :: []
else h :: poly.normalize t
⊦ ∀a b c.
0 < a ∧ 0 < c ∧ ¬(0 = b) ∧ transc.rpow a b = transc.rpow c b ⇒ a = c
⊦ ∀a b c. 1 < a ∧ 0 < c ∧ 0 < b ∧ transc.rpow a b = transc.rpow a c ⇒ b = c
⊦ ∀x.
¬(x = 1) ⇒ ∀n. real.sum (0, n) (λn. x ↑ n) = real./ (x ↑ n - 1) (x - 1)
⊦ ∀x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ≤ x ∧
x ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ⇒
transc.cos x = transc.sqrt (1 - transc.sin x ↑ arithmetic.BIT2 0)
⊦ ∀x.
seq.sums
(λn.
(let n ← n in
if even n then 0
else
real./ (~1 ↑ (arithmetic.- n 1 div arithmetic.BIT2 0))
(fromNatural (factorial n))) * x ↑ n) (transc.sin x)
⊦ ∀f.
seq.cauchy f ⇔
∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ∧ n ≥ N ⇒ abs (f m - f n) < e
⊦ ∀f g a b.
a ≤ b ∧ integral.integrable (a, b) f ∧ integral.integrable (a, b) g ⇒
integral.integrable (a, b) (λx. f x + g x)
⊦ ∀f s1 s2.
pred_set.FINITE s1 ∧ pred_set.FINITE s2 ⇒
real_sigma.REAL_SUM_IMAGE (pair.UNCURRY (λx y. f (x, y)))
(pred_set.CROSS s1 s2) =
real_sigma.REAL_SUM_IMAGE (pair.UNCURRY (λy x. f (x, y)))
(pred_set.CROSS s2 s1)
⊦ ∀n a.
poly.poly (poly.diff (poly.poly_exp (~a :: 1 :: []) (suc n))) =
poly.poly
(poly.## (fromNatural (suc n)) (poly.poly_exp (~a :: 1 :: []) n))
⊦ ∀f a b i j.
a ≤ b ∧ transc.Dint (a, b) f i ∧ transc.Dint (a, b) (λx. abs (f x)) j ⇒
abs i ≤ j
⊦ ∀g.
nets.dorder g ⇒
∀x x0.
nets.tends x x0 (topology.mtop topology.mr1, g) ∧ ¬(x0 = 0) ⇒
nets.tends (λn. realax.inv (x n)) (realax.inv x0)
(topology.mtop topology.mr1, g)
⊦ ∀x.
transc.sin x =
seq.suminf
(λn.
(let n ← n in
if even n then 0
else
real./ (~1 ↑ (arithmetic.- n 1 div arithmetic.BIT2 0))
(fromNatural (factorial n))) * x ↑ n)
⊦ ∀y.
~1 < y ∧ y < 1 ⇒
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) < transc.asn y ∧
transc.asn y < real./ transc.pi (fromNatural (arithmetic.BIT2 0))
⊦ ∀y.
~1 ≤ y ∧ y ≤ 1 ⇒
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ≤ transc.asn y ∧
transc.asn y ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0))
⊦ ∀m g f.
nets.bounded (m, g) f ⇔
∃k x N. g N N ∧ ∀n. g n N ⇒ topology.dist m (f n, x) < k
⊦ ∀f k m n.
(∀p. m ≤ p ∧ p < m + n ⇒ f p ≤ k) ⇒
real.sum (m, n) f ≤ fromNatural n * k
⊦ ∀f c a b.
a ≤ b ∧ integral.integrable (a, b) f ⇒
integral.integral (a, b) (λx. c * f x) = c * integral.integral (a, b) f
⊦ ∀g1 g2 D p.
transc.fine (λx. if g1 x < g2 x then g1 x else g2 x) (D, p) ⇒
transc.fine g1 (D, p) ∧ transc.fine g2 (D, p)
⊦ ∀n x y.
x ↑ suc n - y ↑ suc n =
(x - y) * real.sum (0, suc n) (λp. x ↑ p * y ↑ arithmetic.- n p)
⊦ ∀a b d n.
transc.division (a, b) d ∧ d n < d (suc n) ∧
d (suc (suc n)) = d (suc n) ⇒ transc.dsize d = suc n
⊦ ∀m x y z.
nets.tendsto (m, x) y z ⇔
0 < topology.dist m (x, y) ∧
topology.dist m (x, y) ≤ topology.dist m (x, z)
⊦ ∀P.
pred_set.FINITE P ⇒
∀f p.
bool.IN p P ∧ (∀q. bool.IN q P ⇒ f p = f q) ⇒
real_sigma.REAL_SUM_IMAGE f P = fromNatural (pred_set.CARD P) * f p
⊦ ∀f s t.
pred_set.FINITE s ∧ pred_set.FINITE t ∧ pred_set.SUBSET s t ∧
(∀x. bool.IN x t ⇒ 0 ≤ f x) ⇒
real_sigma.REAL_SUM_IMAGE f s ≤ real_sigma.REAL_SUM_IMAGE f t
⊦ ∀p e.
0 < e ∧ (∃r. p r) ∧ (∃z. ∀r. p r ⇒ r ≤ z) ⇒
∃x. p x ∧ real.sup p ≤ x + e
⊦ ∀L.
topology.istopology L ⇔
L pred_set.EMPTY ∧ L pred_set.UNIV ∧
(∀a b. L a ∧ L b ⇒ L (topology.re_intersect a b)) ∧
∀P. pred_set.SUBSET P L ⇒ L (pred_set.BIGUNION P)
⊦ real./ (real./ x y) z =
if y = 0 then real./ (marker.unint (real./ x y)) z
else if z = 0 then marker.unint (real./ (real./ x y) z)
else real./ x (y * z)
⊦ ∀a b D p.
transc.tdiv (a, b) (D, p) ⇔
transc.division (a, b) D ∧ ∀n. D n ≤ p n ∧ p n ≤ D (suc n)
⊦ ∀m x S'.
topology.limpt (topology.mtop m) x S' ⇔
∀e. 0 < e ⇒ ∃y. ¬(x = y) ∧ S' y ∧ topology.dist m (x, y) < e
⊦ ∀f l x.
lim.diffl f l x ⇔
∃g. (∀z. f z - f x = g z * (z - x)) ∧ lim.contl g x ∧ g x = l
⊦ ∀g.
nets.dorder g ⇔
∀x y. g x x ∧ g y y ⇒ ∃z. g z z ∧ ∀w. g w z ⇒ g w x ∧ g w y
⊦ (∀n f. real.sum (n, 0) f = 0) ∧
∀n m f. real.sum (n, suc m) f = real.sum (n, m) f + f (n + m)
⊦ ∀n p.
(∀y. y < n ⇒ ∃!x. x < n ∧ p x = y) ⇒
∀f. real.sum (0, n) (λn. f (p n)) = real.sum (0, n) f
⊦ ∀p a b.
a < b ⇒
∃x.
a < x ∧ x < b ∧
poly.poly p b - poly.poly p a = (b - a) * poly.poly (poly.diff p) x
⊦ ∀d x x0.
nets.tends x x0 (topology.mtop d, (≥)) ⇔
∀e. 0 < e ⇒ ∃N. ∀n. n ≥ N ⇒ topology.dist d (x n, x0) < e
⊦ ∀f g l m x.
lim.diffl f l x ∧ lim.diffl g m x ⇒
lim.diffl (λx. f x * g x) (l * g x + m * f x) x
⊦ ∀f g l m x.
lim.tends_real_real f l x ∧ lim.tends_real_real g m x ∧ ¬(m = 0) ⇒
lim.tends_real_real (λx. real./ (f x) (g x)) (real./ l m) x
⊦ (∀l2. poly.poly_add [] l2 = l2) ∧
∀h t l2.
poly.poly_add (h :: t) l2 =
if l2 = [] then h :: t else h + head l2 :: poly.poly_add t (tail l2)
⊦ ∀n x y.
real.sum (0, suc n) (λp. x ↑ p * y ↑ arithmetic.- n p) =
real.sum (0, suc n) (λp. x ↑ arithmetic.- n p * y ↑ p)
⊦ ∀n p.
¬(poly.poly p = poly.poly []) ∧ length p = n ⇒
∃i. ∀x. poly.poly p x = 0 ⇒ ∃m. m ≤ n ∧ x = i m
⊦ ∀a b x. a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (x - y) < d ⇒ a ≤ y ∧ y ≤ b
⊦ ∀a b x. a < x ∧ x < b ⇒ ∃d. 0 < d ∧ ∀y. abs (y - x) ≤ d ⇒ a < y ∧ y < b
⊦ ∀x.
~transc.sin x =
seq.suminf
(λn.
~((let n ← n in
if even n then 0
else
real./ (~1 ↑ (arithmetic.- n 1 div arithmetic.BIT2 0))
(fromNatural (factorial n))) * x ↑ n))
⊦ ∀s l top g.
nets.tends s l (top, g) ⇔
∀N. topology.neigh top (N, l) ⇒ ∃n. g n n ∧ ∀m. g m n ⇒ N (s m)
⊦ ∀c x.
seq.summable (λn. powser.diffs c n * x ↑ n) ⇒
seq.sums (λn. fromNatural n * (c n * x ↑ arithmetic.- n 1))
(seq.suminf (λn. powser.diffs c n * x ↑ n))
⊦ ∀f g m n.
(∀p. m ≤ p ∧ p < m + n ⇒ f p = g p) ⇒
real.sum (m, n) f = real.sum (m, n) g
⊦ ∀f g m n.
(∀r. m ≤ r ∧ r < n + m ⇒ f r = g r) ⇒
real.sum (m, n) f = real.sum (m, n) g
⊦ ∀f g m n.
(∀r. m ≤ r ∧ r < n + m ⇒ f r ≤ g r) ⇒
real.sum (m, n) f ≤ real.sum (m, n) g
⊦ ∀d p a b.
transc.tdiv (a, b) (d, p) ⇒ ∀n. a ≤ d n ∧ d n ≤ b ∧ a ≤ p n ∧ p n ≤ b
⊦ ∀f x l.
lim.diffl f l x ∧ (∃d. 0 < d ∧ ∀y. abs (x - y) < d ⇒ f y = f x) ⇒ l = 0
⊦ ∀f x l.
lim.diffl f l x ∧ (∃d. 0 < d ∧ ∀y. abs (x - y) < d ⇒ f x ≤ f y) ⇒ l = 0
⊦ ∀f x l.
lim.diffl f l x ∧ (∃d. 0 < d ∧ ∀y. abs (x - y) < d ⇒ f y ≤ f x) ⇒ l = 0
⊦ ∀a b g.
a ≤ b ∧ transc.gauge (λx. a ≤ x ∧ x ≤ b) g ⇒
∃D p. transc.tdiv (a, b) (D, p) ∧ transc.fine g (D, p)
⊦ ∀g.
nets.dorder g ⇒
∀x y.
nets.bounded (topology.mr1, g) x ∧
nets.tends y 0 (topology.mtop topology.mr1, g) ⇒
nets.tends (λn. x n * y n) 0 (topology.mtop topology.mr1, g)
⊦ ∀diff n x.
x = 0 ∧ 0 < n ⇒
real.sum (0, n)
(λm. real./ (diff m 0) (fromNatural (factorial m)) * x ↑ m) =
diff 0 0
⊦ (∀l2. poly.poly_mul [] l2 = []) ∧
∀h t l2.
poly.poly_mul (h :: t) l2 =
if t = [] then poly.## h l2
else poly.poly_add (poly.## h l2) (0 :: poly.poly_mul t l2)
⊦ ∀a b d n.
transc.division (a, b) d ∧ d (suc n) = d n ∧
(∀i. i < n ⇒ d i < d (suc i)) ⇒ transc.dsize d = n
⊦ ∀a p q.
poly.poly_divides (a :: 1 :: []) (poly.poly_mul p q) ⇔
poly.poly_divides (a :: 1 :: []) p ∨ poly.poly_divides (a :: 1 :: []) q
⊦ ∀a p.
poly.poly_order a p =
select n.
poly.poly_divides (poly.poly_exp (~a :: 1 :: []) n) p ∧
¬poly.poly_divides (poly.poly_exp (~a :: 1 :: []) (suc n)) p
⊦ ∀p x.
(∃r. p r) ∧ (∃y. ∀z. p z ⇒ y ≤ z) ⇒
(real.inf p ≤ x ⇔ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x)
⊦ ∀p x.
(∃r. p r) ∧ (∃z. ∀r. p r ⇒ r ≤ z) ⇒
(x ≤ real.sup p ⇔ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y)
⊦ ∀P.
(∃x. P x ∧ 0 < x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
⊦ ∀f g a b i j.
transc.Dint (a, b) f i ∧ transc.Dint (a, b) g j ⇒
transc.Dint (a, b) (λx. f x + g x) (i + j)
⊦ ∀f g a b i j.
transc.Dint (a, b) f i ∧ transc.Dint (a, b) g j ⇒
transc.Dint (a, b) (λx. f x - g x) (i - j)
⊦ ∀f f' a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.diffl f (f' x) x) ⇒
transc.Dint (a, b) f' (f b - f a)
⊦ ∀g x x0.
nets.tends x x0 (topology.mtop topology.mr1, g) ∧ ¬(x0 = 0) ⇒
∃N. g N N ∧ ∀n. g n N ⇒ ¬(x n = 0)
⊦ ∀x n.
∃t.
abs t ≤ abs x ∧
transc.exp x =
real.sum (0, n) (λm. real./ (x ↑ m) (fromNatural (factorial m))) +
real./ (transc.exp t) (fromNatural (factorial n)) * x ↑ n
⊦ ∀f g a b i.
transc.Dint (a, b) f i ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ f x = g x) ⇒
transc.Dint (a, b) g i
⊦ poly.poly_mul [] p2 = [] ∧ poly.poly_mul (h1 :: []) p2 = poly.## h1 p2 ∧
poly.poly_mul (h1 :: k1 :: t1) p2 =
poly.poly_add (poly.## h1 p2) (0 :: poly.poly_mul (k1 :: t1) p2)
⊦ ∀p a.
poly.rsquarefree p ∧ poly.poly p a = 0 ⇒
∃q.
poly.poly p = poly.poly (poly.poly_mul (~a :: 1 :: []) q) ∧
¬(poly.poly q a = 0)
⊦ ∀d a b c.
transc.division (a, b) d ∧ a ≤ c ∧ c ≤ b ⇒
∃n. n ≤ transc.dsize d ∧ d n ≤ c ∧ c ≤ d (suc n)
⊦ ∀f a b.
(let x ← a in f x - real./ (f b - f a) (b - a) * x) =
let x ← b in f x - real./ (f b - f a) (b - a) * x
⊦ ∀a b c d.
¬(b = 0) ∧ ¬(d = 0) ⇒
real./ a b + real./ c d = real./ (a * d + b * c) (b * d)
⊦ ∀a b c d.
¬(b = 0) ∧ ¬(d = 0) ⇒
real./ a b - real./ c d = real./ (a * d - b * c) (b * d)
⊦ ∀y.
~1 ≤ y ∧ y ≤ 1 ⇒
∃!x.
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ≤ x ∧
x ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
transc.sin x = y
⊦ ∀L.
topology.open L pred_set.EMPTY ∧ topology.open L pred_set.UNIV ∧
(∀x y.
topology.open L x ∧ topology.open L y ⇒
topology.open L (topology.re_intersect x y)) ∧
∀P.
pred_set.SUBSET P (topology.open L) ⇒
topology.open L (pred_set.BIGUNION P)
⊦ ∀P s d.
(∀y. (∃x. (let x ← x in P (x + d)) ∧ y < x) ⇔ y < s) ⇒
∀y. (∃x. P x ∧ y < x) ⇔ y < s + d
⊦ ∀f a b c.
a ≤ b ∧ b ≤ c ∧ integral.integrable (a, c) f ⇒
integral.integral (a, c) f =
integral.integral (a, b) f + integral.integral (b, c) f
⊦ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∃M. ∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M
⊦ ∀f k' k.
0 < k ∧ (∀h. 0 < abs h ∧ abs h < k ⇒ abs (f h) ≤ k' * abs h) ⇒
lim.tends_real_real f 0 0
⊦ ∀n x y.
real.sum (0, suc n) (λp. x ↑ p * y ↑ arithmetic.- (suc n) p) =
y * real.sum (0, suc n) (λp. x ↑ p * y ↑ arithmetic.- n p)
⊦ ∀f n.
seq.summable f ∧
(∀d.
0 <
f (n + arithmetic.BIT2 0 * d) +
f (n + (arithmetic.BIT2 0 * d + 1))) ⇒
real.sum (0, n) f < seq.suminf f
⊦ ∀P.
(∀n f. P (n, 0) f) ∧ (∀n m f. P (n, m) f ⇒ P (n, suc m) f) ⇒
∀v v1 v2. P (v, v1) v2
⊦ ∀p a b.
a < b ∧ poly.poly p a < 0 ∧ poly.poly p b > 0 ⇒
∃x. a < x ∧ x < b ∧ poly.poly p x = 0
⊦ ∀p a b.
a < b ∧ poly.poly p a > 0 ∧ poly.poly p b < 0 ⇒
∃x. a < x ∧ x < b ∧ poly.poly p x = 0
⊦ ∀g.
nets.dorder g ⇒
∀x y.
nets.tends x 0 (topology.mtop topology.mr1, g) ∧
nets.tends y 0 (topology.mtop topology.mr1, g) ⇒
nets.tends (λn. x n + y n) 0 (topology.mtop topology.mr1, g)
⊦ ∀m.
topology.ismet m ⇔
(∀x y. m (x, y) = 0 ⇔ x = y) ∧ ∀x y z. m (y, z) ≤ m (x, y) + m (x, z)
⊦ ~real./ x y =
(if y = 0 then ~marker.unint (real./ x y) else real./ (~x) y) ∧
real./ x (~y) =
if y = 0 then marker.unint (real./ x y) else real./ (~x) y
⊦ ∀x.
transc.sin x = 0 ⇔
(∃n.
even n ∧
x =
fromNatural n *
real./ transc.pi (fromNatural (arithmetic.BIT2 0))) ∨
∃n.
even n ∧
x =
~(fromNatural n * real./ transc.pi (fromNatural (arithmetic.BIT2 0)))
⊦ ∀y.
~1 ≤ y ∧ y ≤ 1 ⇒
~real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ≤ transc.asn y ∧
transc.asn y ≤ real./ transc.pi (fromNatural (arithmetic.BIT2 0)) ∧
transc.sin (transc.asn y) = y
⊦ ∀p a.
¬(poly.poly p = poly.poly []) ⇒
∃!n.
poly.poly_divides (poly.poly_exp (~a :: 1 :: []) n) p ∧
¬poly.poly_divides (poly.poly_exp (~a :: 1 :: []) (suc n)) p
⊦ ∀f x l.
lim.diffl f l x ∧ l < 0 ⇒
∃d. 0 < d ∧ ∀h. 0 < h ∧ h < d ⇒ f x < f (x - h)
⊦ ∀f x l.
lim.diffl f l x ∧ 0 < l ⇒
∃d. 0 < d ∧ ∀h. 0 < h ∧ h < d ⇒ f x < f (x + h)
⊦ ∀x0 x y0 y.
x0 < y0 ∧
abs (x - x0) < real./ (y0 - x0) (fromNatural (arithmetic.BIT2 0)) ∧
abs (y - y0) < real./ (y0 - x0) (fromNatural (arithmetic.BIT2 0)) ⇒
x < y
⊦ ∀a b D.
transc.division (a, b) D ⇔
D 0 = a ∧ ∃N. (∀n. n < N ⇒ D n < D (suc n)) ∧ ∀n. n ≥ N ⇒ D n = b
⊦ ∀P.
(∀x. P x ⇒ realax.real_0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
⊦ ∀f a b c i j.
a ≤ b ∧ b ≤ c ∧ transc.Dint (a, b) f i ∧ transc.Dint (b, c) f j ⇒
transc.Dint (a, c) f (i + j)
⊦ ∀f g a b c.
(∀x. a ≤ x ∧ x ≤ b ∧ ¬(x = c) ⇒ f x = g x) ∧
integral.integrable (a, b) f ⇒ integral.integrable (a, b) g
⊦ ∀d g x x0.
nets.tends x x0 (topology.mtop d, g) ⇔
∀e. 0 < e ⇒ ∃n. g n n ∧ ∀m. g m n ⇒ topology.dist d (x m, x0) < e
⊦ ∀D a b.
transc.division (a, b) D ⇔
D 0 = a ∧ (∀n. n < transc.dsize D ⇒ D n < D (suc n)) ∧
∀n. n ≥ transc.dsize D ⇒ D n = b
⊦ ∀P.
(∀x. P x ⇒ 0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
⊦ ∀g.
nets.dorder g ⇒
∀x x0 y y0.
nets.tends x x0 (topology.mtop topology.mr1, g) ∧
nets.tends y y0 (topology.mtop topology.mr1, g) ⇒
nets.tends (λn. x n + y n) (x0 + y0) (topology.mtop topology.mr1, g)
⊦ ∀g.
nets.dorder g ⇒
∀x x0 y y0.
nets.tends x x0 (topology.mtop topology.mr1, g) ∧
nets.tends y y0 (topology.mtop topology.mr1, g) ⇒
nets.tends (λn. x n - y n) (x0 - y0) (topology.mtop topology.mr1, g)
⊦ ∀g.
nets.dorder g ⇒
∀x y x0 y0.
nets.tends x x0 (topology.mtop topology.mr1, g) ∧
nets.tends y y0 (topology.mtop topology.mr1, g) ⇒
nets.tends (λn. x n * y n) (x0 * y0) (topology.mtop topology.mr1, g)
⊦ ∀x.
transc.cos x = 0 ⇔
(∃n.
¬even n ∧
x =
fromNatural n *
real./ transc.pi (fromNatural (arithmetic.BIT2 0))) ∨
∃n.
¬even n ∧
x =
~(fromNatural n * real./ transc.pi (fromNatural (arithmetic.BIT2 0)))
⊦ ∀p a.
¬(poly.poly p = poly.poly []) ⇒
poly.poly_divides (poly.poly_exp (~a :: 1 :: []) (poly.poly_order a p))
p ∧
¬poly.poly_divides
(poly.poly_exp (~a :: 1 :: []) (suc (poly.poly_order a p))) p
⊦ ∀s gs n.
(∀m. m ≤ n ⇒ transc.gauge s (gs m)) ⇒
∃g.
transc.gauge s g ∧
∀d p. transc.fine g (d, p) ⇒ ∀m. m ≤ n ⇒ transc.fine (gs m) (d, p)
⊦ real.NUM_FLOOR (fromNatural n) = n ∧
real.NUM_FLOOR (~fromNatural n) = 0 ∧
(0 < m ⇒
real.NUM_FLOOR (real./ (fromNatural n) (fromNatural m)) = n div m) ∧
(0 < m ⇒ real.NUM_FLOOR (real./ (~fromNatural n) (fromNatural m)) = 0)
⊦ real./ x y * real./ u v =
if y = 0 then marker.unint (real./ x y) * real./ u v
else if v = 0 then real./ x y * marker.unint (real./ u v)
else real./ (x * u) (y * v)
⊦ ∀p a.
¬(poly.poly p = poly.poly []) ⇒
∃q.
poly.poly p =
poly.poly
(poly.poly_mul
(poly.poly_exp (~a :: 1 :: []) (poly.poly_order a p)) q) ∧
¬poly.poly_divides (~a :: 1 :: []) q
⊦ ∀%%genvar%%799.
pred_set.FINITE %%genvar%%799 ⇒
∀f.
(∀x. bool.IN x %%genvar%%799 ⇒ 0 ≤ f x) ∧
(∃x. bool.IN x %%genvar%%799 ∧ ¬(f x = 0)) ⇒
(¬(real_sigma.REAL_SUM_IMAGE f %%genvar%%799 = 0) ⇔
¬(%%genvar%%799 = pred_set.EMPTY))
⊦ ∀f a b.
(∀e.
0 < e ⇒
∃g.
(∀x. a ≤ x ∧ x ≤ b ⇒ abs (f x - g x) ≤ e) ∧
integral.integrable (a, b) g) ⇒ integral.integrable (a, b) f
⊦ ∀f g x d.
0 < d ∧ (∀z. abs (z - x) ≤ d ⇒ g (f z) = z) ∧
(∀z. abs (z - x) ≤ d ⇒ lim.contl f z) ⇒ lim.contl g (f x)
⊦ powser.diffs
(λn.
if even n then 0
else
real./ (~1 ↑ (arithmetic.- n 1 div arithmetic.BIT2 0))
(fromNatural (factorial n))) =
λn.
if even n then
real./ (~1 ↑ (n div arithmetic.BIT2 0)) (fromNatural (factorial n))
else 0
⊦ ∀x.
¬(transc.cos x = 0) ∧
¬(transc.cos (fromNatural (arithmetic.BIT2 0) * x) = 0) ⇒
transc.tan (fromNatural (arithmetic.BIT2 0) * x) =
real./ (fromNatural (arithmetic.BIT2 0) * transc.tan x)
(1 - transc.tan x ↑ arithmetic.BIT2 0)
⊦ ∀f a b.
a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ∧
(∀x. a < x ∧ x < b ⇒ lim.diffl f 0 x) ⇒ f b = f a
⊦ ∀f g a b c i.
(∀x. a ≤ x ∧ x ≤ b ∧ ¬(x = c) ⇒ f x = g x) ∧ transc.Dint (a, b) f i ⇒
transc.Dint (a, b) g i
⊦ ∀P.
pred_set.FINITE P ⇒
∀f.
real_sigma.REAL_SUM_IMAGE f P = 1 ∧
(∀x y. bool.IN x P ∧ bool.IN y P ⇒ f x = f y) ⇒
∀x. bool.IN x P ⇒ f x = realax.inv (fromNatural (pred_set.CARD P))
⊦ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∃x. a ≤ x ∧ x ≤ b ∧ integral.integral (a, b) f = f x * (b - a)
⊦ ∀f g a b i j.
transc.Dint (a, b) f i ∧ transc.Dint (a, b) g j ⇒
transc.Dint (a, b) (λx. m * f x + n * g x) (m * i + n * j)
⊦ ∀f g a b.
a ≤ b ∧ integral.integrable (a, b) f ∧ integral.integrable (a, b) g ⇒
integral.integral (a, b) (λx. f x + g x) =
integral.integral (a, b) f + integral.integral (a, b) g
⊦ ∀f g a b.
a ≤ b ∧ integral.integrable (a, b) f ∧ integral.integrable (a, b) g ⇒
integral.integral (a, b) (λx. f x - g x) =
integral.integral (a, b) f - integral.integral (a, b) g
⊦ ∀a b d p e f.
transc.tdiv (a, b) (d, p) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ abs (f x) ≤ e) ⇒
abs (transc.rsum (d, p) f) ≤ e * (b - a)
⊦ ∀p a n.
poly.poly_divides (poly.poly_exp (~a :: 1 :: []) n) p ∧
¬poly.poly_divides (poly.poly_exp (~a :: 1 :: []) (suc n)) p ⇔
n = poly.poly_order a p ∧ ¬(poly.poly p = poly.poly [])
⊦ ∀p a n.
¬(poly.poly p = poly.poly []) ∧
poly.poly_divides (poly.poly_exp (~a :: 1 :: []) n) p ∧
¬poly.poly_divides (poly.poly_exp (~a :: 1 :: []) (suc n)) p ⇒
n = poly.poly_order a p
⊦ powser.diffs
(λn.
if even n then
real./ (~1 ↑ (n div arithmetic.BIT2 0))
(fromNatural (factorial n))
else 0) =
λn.
~(let n ← n in
if even n then 0
else
real./ (~1 ↑ (arithmetic.- n 1 div arithmetic.BIT2 0))
(fromNatural (factorial n)))
⊦ ∀a d p.
length p = d ∧ ¬(poly.poly p = poly.poly []) ⇒
∃n.
poly.poly_divides (poly.poly_exp (~a :: 1 :: []) n) p ∧
¬poly.poly_divides (poly.poly_exp (~a :: 1 :: []) (suc n)) p
⊦ ∀x y.
(transc.sin (x + y) -
(transc.sin x * transc.cos y + transc.cos x * transc.sin y)) ↑
arithmetic.BIT2 0 +
(transc.cos (x + y) -
(transc.cos x * transc.cos y - transc.sin x * transc.sin y)) ↑
arithmetic.BIT2 0 = 0
⊦ (fromNatural n ≤ fromNatural m ⇔ n ≤ m) ∧
(~fromNatural n ≤ fromNatural m ⇔ ⊤) ∧
(fromNatural n ≤ ~fromNatural m ⇔ n = 0 ∧ m = 0) ∧
(~fromNatural n ≤ ~fromNatural m ⇔ m ≤ n)
⊦ (0 < real./ 1 (fromNatural (arithmetic.BIT2 0)) ∧
real./ 1 (fromNatural (arithmetic.BIT2 0)) < 1) ∧
0 ≤ real./ 1 (fromNatural (arithmetic.BIT2 0)) ∧
real./ 1 (fromNatural (arithmetic.BIT2 0)) ≤ 1
⊦ ∀f g a b i j.
a ≤ b ∧ transc.Dint (a, b) f i ∧ transc.Dint (a, b) g j ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ f x = g x) ⇒ i = j
⊦ ∀f g a b i j.
a ≤ b ∧ transc.Dint (a, b) f i ∧ transc.Dint (a, b) g j ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ g x) ⇒ i ≤ j
⊦ ∀f g a b s i.
pred_set.FINITE s ∧ (∀x. a ≤ x ∧ x ≤ b ∧ ¬bool.IN x s ⇒ f x = g x) ∧
transc.Dint (a, b) f i ⇒ transc.Dint (a, b) g i
⊦ ∀x y.
¬(transc.cos x = 0) ∧ ¬(transc.cos y = 0) ∧ ¬(transc.cos (x + y) = 0) ⇒
transc.tan (x + y) =
real./ (transc.tan x + transc.tan y) (1 - transc.tan x * transc.tan y)
⊦ ∀f g k.
0 < k ∧ seq.summable f ∧
(∀h. 0 < abs h ∧ abs h < k ⇒ ∀n. abs (g h n) ≤ f n * abs h) ⇒
lim.tends_real_real (λh. seq.suminf (g h)) 0 0
⊦ ∀f y0 x0.
lim.tends_real_real f y0 x0 ⇔
∀e.
0 < e ⇒
∃d.
0 < d ∧
∀x. 0 < abs (x - x0) ∧ abs (x - x0) < d ⇒ abs (f x - y0) < e
⊦ ∀g.
nets.dorder g ⇒
∀x x0 y y0.
nets.tends x x0 (topology.mtop topology.mr1, g) ∧
nets.tends y y0 (topology.mtop topology.mr1, g) ∧ ¬(y0 = 0) ⇒
nets.tends (λn. real./ (x n) (y n)) (real./ x0 y0)
(topology.mtop topology.mr1, g)
⊦ ∀f f' m n x.
(∀r. m ≤ r ∧ r < m + n ⇒ lim.diffl (λx. f r x) (f' r x) x) ⇒
lim.diffl (λx. real.sum (m, n) (λn. f n x))
(real.sum (m, n) (λr. f' r x)) x
⊦ real./ (real./ x y) (real./ u v) =
if u = 0 ∨ v = 0 then real./ (real./ x y) (marker.unint (real./ u v))
else if y = 0 then real./ (marker.unint (real./ x y)) (real./ u v)
else real./ (x * v) (y * u)
⊦ ∀m z h.
real.sum (0, m) (λp. (z + h) ↑ arithmetic.- m p * z ↑ p - z ↑ m) =
real.sum (0, m)
(λp. z ↑ p * ((z + h) ↑ arithmetic.- m p - z ↑ arithmetic.- m p))
⊦ ∀n c x.
real.sum (0, n) (λn. powser.diffs c n * x ↑ n) =
real.sum (0, n) (λn. fromNatural n * (c n * x ↑ arithmetic.- n 1)) +
fromNatural n * (c n * x ↑ arithmetic.- n 1)
⊦ ∀n c x.
real.sum (0, n) (λn. fromNatural n * (c n * x ↑ arithmetic.- n 1)) =
real.sum (0, n) (λn. powser.diffs c n * x ↑ n) -
fromNatural n * (c n * x ↑ arithmetic.- n 1)
⊦ ∀g.
nets.dorder g ⇒
∀x x0 y y0.
nets.tends x x0 (topology.mtop topology.mr1, g) ∧
nets.tends y y0 (topology.mtop topology.mr1, g) ∧
(∃N. g N N ∧ ∀n. g n N ⇒ x n ≤ y n) ⇒ x0 ≤ y0
⊦ ∀f a b y.
a ≤ b ∧ (f a ≤ y ∧ y ≤ f b) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∃x. a ≤ x ∧ x ≤ b ∧ f x = y
⊦ ∀f a b y.
a ≤ b ∧ (f b ≤ y ∧ y ≤ f a) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∃x. a ≤ x ∧ x ≤ b ∧ f x = y
⊦ ∀f g l m x.
lim.diffl f l x ∧ lim.diffl g m x ∧ ¬(g x = 0) ⇒
lim.diffl (λx. real./ (f x) (g x))
(real./ (l * g x - m * f x) (g x ↑ arithmetic.BIT2 0)) x
⊦ real./ x (fromNatural n) < real./ u (fromNatural m) ⇔
if n = 0 then marker.unint (real./ x 0) < real./ u (fromNatural m)
else if m = 0 then real./ x (fromNatural n) < marker.unint (real./ u 0)
else fromNatural m * x < fromNatural n * u
⊦ real./ x (fromNatural n) ≤ real./ u (fromNatural m) ⇔
if n = 0 then marker.unint (real./ x 0) ≤ real./ u (fromNatural m)
else if m = 0 then real./ x (fromNatural n) ≤ marker.unint (real./ u 0)
else fromNatural m * x ≤ fromNatural n * u
⊦ (fromNatural n < fromNatural m ⇔ n < m) ∧
(~fromNatural n < fromNatural m ⇔ ¬(n = 0) ∨ ¬(m = 0)) ∧
(fromNatural n < ~fromNatural m ⇔ ⊥) ∧
(~fromNatural n < ~fromNatural m ⇔ m < n)
⊦ ∀P a b.
(∃x. a ≤ x ∧ x ≤ b ∧ P x) ⇒
∃s. a ≤ s ∧ s ≤ b ∧ ∀y. y < s ⇔ ∃x. a ≤ x ∧ x ≤ b ∧ P x ∧ y < x
⊦ real./ x y = real./ u v ⇔
if y = 0 then marker.unint (real./ x y) = real./ u v
else if v = 0 then real./ x y = marker.unint (real./ u v)
else if y = v then x = u
else x * v = y * u
⊦ real.sum_tupled =
relation.WFREC
(select R. wellFounded R ∧ ∀f m n. R ((n, m), f) ((n, suc m), f))
(λsum_tupled a.
pair.pair_CASE a
(λv f.
pair.pair_CASE v
(λn v3.
arithmetic.num_CASE v3 (id 0)
(λm. id (sum_tupled ((n, m), f) + f (n + m))))))
⊦ fromNatural a * fromNatural b = fromNatural (a * b) ∧
~fromNatural a * fromNatural b = ~fromNatural (a * b) ∧
fromNatural a * ~fromNatural b = ~fromNatural (a * b) ∧
~fromNatural a * ~fromNatural b = fromNatural (a * b)
⊦ (fromNatural n = fromNatural m ⇔ n = m) ∧
(~fromNatural n = fromNatural m ⇔ n = 0 ∧ m = 0) ∧
(fromNatural n = ~fromNatural m ⇔ n = 0 ∧ m = 0) ∧
(~fromNatural n = ~fromNatural m ⇔ n = m)
⊦ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ M ≤ f x) ∧ ∃x. a ≤ x ∧ x ≤ b ∧ f x = M
⊦ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∃M. (∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M) ∧ ∃x. a ≤ x ∧ x ≤ b ∧ f x = M
⊦ ∀f g a b i j.
a ≤ b ∧ integral.integrable (a, b) f ∧ integral.integrable (a, b) g ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ g x) ⇒
integral.integral (a, b) f ≤ integral.integral (a, b) g
⊦ ∀g.
nets.dorder g ⇒
∀P Q.
(∃n. g n n ∧ ∀m. g m n ⇒ P m) ∧ (∃n. g n n ∧ ∀m. g m n ⇒ Q m) ⇒
∃n. g n n ∧ ∀m. g m n ⇒ P m ∧ Q m
⊦ ∀x n.
¬(x = 0) ∧ 0 < n ⇒
∃t.
0 < abs t ∧ abs t < abs x ∧
transc.exp x =
real.sum (0, n) (λm. real./ (x ↑ m) (fromNatural (factorial m))) +
real./ (transc.exp t) (fromNatural (factorial n)) * x ↑ n
⊦ ∀f a b.
a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ∧
(∀x. a < x ∧ x < b ⇒ lim.diffl f 0 x) ⇒ ∀x. a ≤ x ∧ x ≤ b ⇒ f x = f a
⊦ ∀f g x d.
0 < d ∧ (∀z. abs (z - x) ≤ d ⇒ g (f z) = z) ∧
(∀z. abs (z - x) ≤ d ⇒ lim.contl f z) ⇒
¬∀z. abs (z - x) ≤ d ⇒ f x ≤ f z
⊦ ∀f g x d.
0 < d ∧ (∀z. abs (z - x) ≤ d ⇒ g (f z) = z) ∧
(∀z. abs (z - x) ≤ d ⇒ lim.contl f z) ⇒
¬∀z. abs (z - x) ≤ d ⇒ f z ≤ f x
⊦ ∀f g l a x b.
a < x ∧ x < b ∧ (∀z. a < z ∧ z < b ⇒ g (f z) = z ∧ lim.contl f z) ∧
lim.diffl f l x ∧ ¬(l = 0) ⇒ lim.diffl g (realax.inv l) (f x)
⊦ real./ x y + real./ u v =
if y = 0 then marker.unint (real./ x y) + real./ u v
else if v = 0 then real./ x y + marker.unint (real./ u v)
else if y = v then real./ (x + u) v
else real./ (x * v + u * y) (y * v)
⊦ ∀a b c.
(∃D p. transc.tdiv (a, b) (D, p) ∧ transc.fine g (D, p)) ∧
(∃D2 p2. transc.tdiv (b, c) (D2, p2) ∧ transc.fine g (D2, p2)) ⇒
∃D p. transc.tdiv (a, c) (D, p) ∧ transc.fine g (D, p)
⊦ ∀f g.
(∀n. f (suc n) ≥ f n) ∧ (∀n. g (suc n) ≤ g n) ∧ (∀n. f n ≤ g n) ⇒
∃l m.
l ≤ m ∧ ((∀n. f n ≤ l) ∧ seq.--> f l) ∧ (∀n. m ≤ g n) ∧ seq.--> g m
⊦ ∀a b d p e f g.
transc.tdiv (a, b) (d, p) ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ abs (f x - g x) ≤ e) ⇒
abs (transc.rsum (d, p) f - transc.rsum (d, p) g) ≤ e * (b - a)
⊦ ∀f a b.
a < b ∧ f a = f b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ∧
(∀x. a < x ∧ x < b ⇒ lim.differentiable f x) ⇒
∃z. a < z ∧ z < b ∧ lim.diffl f 0 z
⊦ ∀f g l x d.
0 < d ∧ (∀z. abs (z - x) < d ⇒ g (f z) = z) ∧
(∀z. abs (z - x) < d ⇒ lim.contl f z) ∧ lim.diffl f l x ∧ ¬(l = 0) ⇒
lim.diffl g (realax.inv l) (f x)
⊦ ∀f g l x d.
0 < d ∧ (∀z. abs (z - x) ≤ d ⇒ g (f z) = z) ∧
(∀z. abs (z - x) ≤ d ⇒ lim.contl f z) ∧ lim.diffl f l x ∧ ¬(l = 0) ⇒
lim.diffl g (realax.inv l) (f x)
⊦ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∃M.
(∀x. a ≤ x ∧ x ≤ b ⇒ f x ≤ M) ∧
∀N. N < M ⇒ ∃x. a ≤ x ∧ x ≤ b ∧ N < f x
⊦ ∀c k' x.
seq.summable (λn. c n * k' ↑ n) ∧
seq.summable (λn. powser.diffs c n * k' ↑ n) ∧
seq.summable (λn. powser.diffs (powser.diffs c) n * k' ↑ n) ∧
abs x < abs k' ⇒
lim.diffl (λx. seq.suminf (λn. c n * x ↑ n))
(seq.suminf (λn. powser.diffs c n * x ↑ n)) x
⊦ ∀a b f k.
transc.Dint (a, b) f k ⇔
∀e.
0 < e ⇒
∃g.
transc.gauge (λx. a ≤ x ∧ x ≤ b) g ∧
∀D p.
transc.tdiv (a, b) (D, p) ∧ transc.fine g (D, p) ⇒
abs (transc.rsum (D, p) f - k) < e
⊦ ∀f g.
(∀n. f (suc n) ≥ f n) ∧ (∀n. g (suc n) ≤ g n) ∧ (∀n. f n ≤ g n) ∧
seq.--> (λn. f n - g n) 0 ⇒
∃l. ((∀n. f n ≤ l) ∧ seq.--> f l) ∧ (∀n. l ≤ g n) ∧ seq.--> g l
⊦ (∀n. intreal.INT_FLOOR (fromNatural n) = integer.int_of_num n) ∧
(∀n.
intreal.INT_FLOOR (~fromNatural n) =
integer.int_neg (integer.int_of_num n)) ∧
(∀n m.
0 < m ⇒
intreal.INT_FLOOR (real./ (fromNatural n) (fromNatural m)) =
integer.int_div (integer.int_of_num n) (integer.int_of_num m)) ∧
∀n m.
0 < m ⇒
intreal.INT_FLOOR (real./ (~fromNatural n) (fromNatural m)) =
integer.int_div (integer.int_neg (integer.int_of_num n))
(integer.int_of_num m)
⊦ ∀p q d e r s.
¬(poly.poly (poly.diff p) = poly.poly []) ∧
poly.poly p = poly.poly (poly.poly_mul q d) ∧
poly.poly (poly.diff p) = poly.poly (poly.poly_mul e d) ∧
poly.poly d =
poly.poly
(poly.poly_add (poly.poly_mul r p) (poly.poly_mul s (poly.diff p))) ⇒
∀a. poly.poly_order a q = if poly.poly_order a p = 0 then 0 else 1
⊦ ∀f diff.
diff 0 = f ∧ (∀m x. lim.diffl (diff m) (diff (suc m) x) x) ⇒
∀x n.
∃t.
abs t ≤ abs x ∧
f x =
real.sum (0, n)
(λm. real./ (diff m 0) (fromNatural (factorial m)) * x ↑ m) +
real./ (diff n t) (fromNatural (factorial n)) * x ↑ n
⊦ ∀f a b.
a < b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ∧
(∀x. a < x ∧ x < b ⇒ lim.differentiable f x) ⇒
∃l z. a < z ∧ z < b ∧ lim.diffl f l z ∧ f b - f a = (b - a) * l
⊦ ∀m1 m2 f x0 y0.
topology.limpt (topology.mtop m1) x0 pred_set.UNIV ⇒
(nets.tends f y0 (topology.mtop m2, nets.tendsto (m1, x0)) ⇔
∀e.
0 < e ⇒
∃d.
0 < d ∧
∀x.
0 < topology.dist m1 (x, x0) ∧ topology.dist m1 (x, x0) < d ⇒
topology.dist m2 (f x, y0) < e)
⊦ ∀m1 m2 f x0 y0.
topology.limpt (topology.mtop m1) x0 pred_set.UNIV ⇒
(nets.tends f y0 (topology.mtop m2, nets.tendsto (m1, x0)) ⇔
∀e.
0 < e ⇒
∃d.
0 < d ∧
∀x.
0 < topology.dist m1 (x, x0) ∧ topology.dist m1 (x, x0) ≤ d ⇒
topology.dist m2 (f x, y0) < e)
⊦ ∀p q d e r s.
¬(poly.poly (poly.diff p) = poly.poly []) ∧
poly.poly p = poly.poly (poly.poly_mul q d) ∧
poly.poly (poly.diff p) = poly.poly (poly.poly_mul e d) ∧
poly.poly d =
poly.poly
(poly.poly_add (poly.poly_mul r p) (poly.poly_mul s (poly.diff p))) ⇒
poly.rsquarefree q ∧ ∀a. poly.poly q a = 0 ⇔ poly.poly p a = 0
⊦ ∀z h n k'.
¬(h = 0) ∧ abs z ≤ k' ∧ abs (z + h) ≤ k' ⇒
abs
(real./ ((z + h) ↑ n - z ↑ n) h -
fromNatural n * z ↑ arithmetic.- n 1) ≤
fromNatural n *
(fromNatural (arithmetic.- n 1) *
(k' ↑ arithmetic.- n (arithmetic.BIT2 0) * abs h))
⊦ ∀P.
(∀a b c. a ≤ b ∧ b ≤ c ∧ P a b ∧ P b c ⇒ P a c) ∧
(∀x. ∃d. 0 < d ∧ ∀a b. a ≤ x ∧ x ≤ b ∧ b - a < d ⇒ P a b) ⇒
∀a b. a ≤ b ⇒ P a b
⊦ x ↑ 0 = 1 ∧ 0 ↑ bit1 n = 0 ∧ 0 ↑ arithmetic.BIT2 n = 0 ∧
fromNatural a ↑ n = fromNatural (a ↑ n) ∧
~fromNatural a ↑ n =
(if odd n then (~) else λx. x) (fromNatural (a ↑ n)) ∧
real./ x y ↑ n = real./ (x ↑ n) (y ↑ n)
⊦ fromNatural n + fromNatural m = fromNatural (n + m) ∧
~fromNatural n + fromNatural m =
(if n ≤ m then fromNatural (arithmetic.- m n)
else ~fromNatural (arithmetic.- n m)) ∧
fromNatural n + ~fromNatural m =
(if n < m then ~fromNatural (arithmetic.- m n)
else fromNatural (arithmetic.- n m)) ∧
~fromNatural n + ~fromNatural m = ~fromNatural (n + m)
⊦ (∀n f. real.sum (n, 0) f = 0) ∧
(∀n m f.
real.sum (n, bit1 m) f =
real.sum (n, arithmetic.- (bit1 m) 1) f +
f (n + arithmetic.- (bit1 m) 1)) ∧
∀n m f.
real.sum (n, arithmetic.BIT2 m) f =
real.sum (n, bit1 m) f + f (n + bit1 m)
⊦ ∀f g x d.
0 < d ∧ (∀z. abs (z - x) ≤ d ⇒ g (f z) = z) ∧
(∀z. abs (z - x) ≤ d ⇒ lim.contl f z) ⇒
∃e. 0 < e ∧ ∀y. abs (y - f x) ≤ e ⇒ ∃z. abs (z - x) ≤ d ∧ f z = y
⊦ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∀e.
0 < e ⇒
∃d.
0 < d ∧
∀x y.
a ≤ x ∧ x ≤ b ∧ a ≤ y ∧ y ≤ b ∧ abs (x - y) < d ⇒
abs (f x - f y) < e
⊦ ∀P.
(∀a b c. a ≤ b ∧ b ≤ c ∧ P (a, b) ∧ P (b, c) ⇒ P (a, c)) ∧
(∀x. ∃d. 0 < d ∧ ∀a b. a ≤ x ∧ x ≤ b ∧ b - a < d ⇒ P (a, b)) ⇒
∀a b. a ≤ b ⇒ P (a, b)
⊦ ∀f g f' g' a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.diffl f (f' x) x) ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ lim.diffl g (g' x) x) ⇒
transc.Dint (a, b) (λx. f' x * g x + f x * g' x)
(f b * g b - f a * g a)
⊦ ∀z h n.
¬(h = 0) ⇒
real./ ((z + h) ↑ n - z ↑ n) h - fromNatural n * z ↑ arithmetic.- n 1 =
h *
real.sum (0, arithmetic.- n 1)
(λp.
z ↑ p *
real.sum (0, arithmetic.- (arithmetic.- n 1) p)
(λq.
(z + h) ↑ q *
z ↑
arithmetic.-
(arithmetic.- (arithmetic.- n (arithmetic.BIT2 0)) p) q))
⊦ ∀f a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.contl f x) ⇒
∃L M.
L ≤ M ∧ (∀y. L ≤ y ∧ y ≤ M ⇒ ∃x. a ≤ x ∧ x ≤ b ∧ f x = y) ∧
∀x. a ≤ x ∧ x ≤ b ⇒ L ≤ f x ∧ f x ≤ M
⊦ ∀a b c D1 p1 D2 p2.
transc.tdiv (a, b) (D1, p1) ∧ transc.fine g (D1, p1) ∧
transc.tdiv (b, c) (D2, p2) ∧ transc.fine g (D2, p2) ⇒
∃D p.
transc.tdiv (a, c) (D, p) ∧ transc.fine g (D, p) ∧
∀f.
transc.rsum (D, p) f =
transc.rsum (D1, p1) f + transc.rsum (D2, p2) f
⊦ ∀f a b.
integral.integrable (a, b) f ⇔
∀e.
0 < e ⇒
∃g.
transc.gauge (λx. a ≤ x ∧ x ≤ b) g ∧
∀d1 p1 d2 p2.
transc.tdiv (a, b) (d1, p1) ∧ transc.fine g (d1, p1) ∧
transc.tdiv (a, b) (d2, p2) ∧ transc.fine g (d2, p2) ⇒
abs (transc.rsum (d1, p1) f - transc.rsum (d2, p2) f) < e
⊦ ∀f diff.
diff 0 = f ∧ (∀m x. lim.diffl (diff m) (diff (suc m) x) x) ⇒
∀x n.
¬(x = 0) ∧ 0 < n ⇒
∃t.
0 < abs t ∧ abs t < abs x ∧
f x =
real.sum (0, n)
(λm. real./ (diff m 0) (fromNatural (factorial m)) * x ↑ m) +
real./ (diff n t) (fromNatural (factorial n)) * x ↑ n
⊦ intreal.INT_FLOOR (fromNatural n) = integer.int_of_num n ∧
intreal.INT_FLOOR (~fromNatural n) =
integer.int_neg (integer.int_of_num n) ∧
intreal.INT_FLOOR (real./ (fromNatural n) (fromNatural (bit1 m))) =
integer.int_div (integer.int_of_num n) (integer.int_of_num (bit1 m)) ∧
intreal.INT_FLOOR
(real./ (fromNatural n) (fromNatural (arithmetic.BIT2 m))) =
integer.int_div (integer.int_of_num n)
(integer.int_of_num (arithmetic.BIT2 m)) ∧
intreal.INT_FLOOR (real./ (~fromNatural n) (fromNatural (bit1 m))) =
integer.int_div (integer.int_neg (integer.int_of_num n))
(integer.int_of_num (bit1 m)) ∧
intreal.INT_FLOOR
(real./ (~fromNatural n) (fromNatural (arithmetic.BIT2 m))) =
integer.int_div (integer.int_neg (integer.int_of_num n))
(integer.int_of_num (arithmetic.BIT2 m))
⊦ ∀f diff h n.
h < 0 ∧ 0 < n ∧ diff 0 = f ∧
(∀m t. m < n ∧ h ≤ t ∧ t ≤ 0 ⇒ lim.diffl (diff m) (diff (suc m) t) t) ⇒
∃t.
h < t ∧ t < 0 ∧
f h =
real.sum (0, n)
(λm. real./ (diff m 0) (fromNatural (factorial m)) * h ↑ m) +
real./ (diff n t) (fromNatural (factorial n)) * h ↑ n
⊦ ∀f diff h n.
0 < h ∧ 0 < n ∧ diff 0 = f ∧
(∀m t. m < n ∧ 0 ≤ t ∧ t ≤ h ⇒ lim.diffl (diff m) (diff (suc m) t) t) ⇒
∃t.
0 < t ∧ t < h ∧
f h =
real.sum (0, n)
(λm. real./ (diff m 0) (fromNatural (factorial m)) * h ↑ m) +
real./ (diff n t) (fromNatural (factorial n)) * h ↑ n
⊦ ∀f a b c.
a ≤ c ∧ c ≤ b ∧ integral.integrable (a, b) f ⇒
∃i.
∀e.
0 < e ⇒
∃g.
transc.gauge (λx. a ≤ x ∧ x ≤ b) g ∧
∀d1 p1 d2 p2.
transc.tdiv (a, c) (d1, p1) ∧ transc.fine g (d1, p1) ∧
transc.tdiv (c, b) (d2, p2) ∧ transc.fine g (d2, p2) ⇒
abs (transc.rsum (d1, p1) f + transc.rsum (d2, p2) f - i) < e
⊦ ∀f g f' g' a b.
a ≤ b ∧ (∀x. a ≤ x ∧ x ≤ b ⇒ lim.diffl f (f' x) x) ∧
(∀x. a ≤ x ∧ x ≤ b ⇒ lim.diffl g (g' x) x) ∧
integral.integrable (a, b) (λx. f' x * g x) ∧
integral.integrable (a, b) (λx. f x * g' x) ⇒
integral.integral (a, b) (λx. f x * g' x) =
f b * g b - f a * g a - integral.integral (a, b) (λx. f' x * g x)
⊦ (0 < real./ 1 3 ∧ real./ 1 3 < 1 ∧
0 < real./ (fromNatural (arithmetic.BIT2 0)) 3 ∧
real./ (fromNatural (arithmetic.BIT2 0)) 3 < 1) ∧ 0 ≤ real./ 1 3 ∧
real./ 1 3 ≤ 1 ∧ 0 ≤ real./ (fromNatural (arithmetic.BIT2 0)) 3 ∧
real./ (fromNatural (arithmetic.BIT2 0)) 3 ≤ 1
⊦ ∀a b c g d1 p1 d2 p2.
transc.tdiv (a, b) (d1, p1) ∧ transc.fine g (d1, p1) ∧
transc.tdiv (b, c) (d2, p2) ∧ transc.fine g (d2, p2) ⇒
transc.tdiv (a, c)
((λn.
if n < transc.dsize d1 then d1 n
else d2 (arithmetic.- n (transc.dsize d1))),
(λn.
if n < transc.dsize d1 then p1 n
else p2 (arithmetic.- n (transc.dsize d1)))) ∧
transc.fine g
((λn.
if n < transc.dsize d1 then d1 n
else d2 (arithmetic.- n (transc.dsize d1))),
(λn.
if n < transc.dsize d1 then p1 n
else p2 (arithmetic.- n (transc.dsize d1)))) ∧
∀f.
transc.rsum
((λn.
if n < transc.dsize d1 then d1 n
else d2 (arithmetic.- n (transc.dsize d1))),
(λn.
if n < transc.dsize d1 then p1 n
else p2 (arithmetic.- n (transc.dsize d1)))) f =
transc.rsum (d1, p1) f + transc.rsum (d2, p2) f
⊦ (lim.diffl f l x ∧ ¬(f x = 0) ⇒
lim.diffl (λx. realax.inv (f x)) (~real./ l (f x ↑ arithmetic.BIT2 0))
x) ∧
(lim.diffl f l x ∧ lim.diffl g m x ∧ ¬(g x = 0) ⇒
lim.diffl (λx. real./ (f x) (g x))
(real./ (l * g x - m * f x) (g x ↑ arithmetic.BIT2 0)) x) ∧
(lim.diffl f l x ∧ lim.diffl g m x ⇒
lim.diffl (λx. f x + g x) (l + m) x) ∧
(lim.diffl f l x ∧ lim.diffl g m x ⇒
lim.diffl (λx. f x * g x) (l * g x + m * f x) x) ∧
(lim.diffl f l x ∧ lim.diffl g m x ⇒
lim.diffl (λx. f x - g x) (l - m) x) ∧
(lim.diffl f l x ⇒ lim.diffl (λx. ~f x) (~l) x) ∧
(lim.diffl g m x ⇒
lim.diffl (λx. g x ↑ n) (fromNatural n * g x ↑ arithmetic.- n 1 * m)
x) ∧
(lim.diffl g m x ⇒
lim.diffl (λx. transc.exp (g x)) (transc.exp (g x) * m) x) ∧
(lim.diffl g m x ⇒
lim.diffl (λx. transc.sin (g x)) (transc.cos (g x) * m) x) ∧
(lim.diffl g m x ⇒
lim.diffl (λx. transc.cos (g x)) (~transc.sin (g x) * m) x)
External Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- List
- HOL4
- integer
- integer.int
- integer
- Number
- Natural
- natural
- Real
- real
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∃!
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- []
- all
- head
- length
- map
- tail
- Pair
- ,
- fst
- snd
- Bool
- Function
- flip
- id
- ∘
- Combinator
- Combinator.s
- HOL4
- arithmetic
- arithmetic.-
- arithmetic.num_CASE
- arithmetic.BIT2
- arithmetic.DIV2
- bool
- bool.IN
- bool.LET
- bool.TYPE_DEFINITION
- integer
- integer.int_add
- integer.int_div
- integer.int_le
- integer.int_lt
- integer.int_mul
- integer.int_neg
- integer.int_of_num
- integer.int_sub
- integer.LEAST_INT
- integer.Num
- marker
- marker.unint
- marker.Abbrev
- numeral
- numeral.exactlog
- numeral.iDUB
- numeral.iSUB
- numeral.iZ
- numeral.iiSUC
- numeral.internal_mult
- numeral.onecount
- numeral.texp_help
- pair
- pair.pair_CASE
- pair.UNCURRY
- pred_set
- pred_set.count
- pred_set.BIGUNION
- pred_set.CARD
- pred_set.CHOICE
- pred_set.COMPL
- pred_set.CROSS
- pred_set.DELETE
- pred_set.DIFF
- pred_set.DISJOINT
- pred_set.EMPTY
- pred_set.FINITE
- pred_set.GSPEC
- pred_set.IMAGE
- pred_set.INJ
- pred_set.INSERT
- pred_set.INTER
- pred_set.ITSET
- pred_set.REST
- pred_set.SUBSET
- pred_set.UNION
- pred_set.UNIV
- prim_rec
- prim_rec.PRE
- relation
- relation.inv_image
- relation.RESTRICT
- relation.WFREC
- while
- while.LEAST
- arithmetic
- Number
- Natural
- *
- +
- <
- ≤
- >
- ≥
- ↑
- bit1
- div
- even
- factorial
- mod
- odd
- suc
- zero
- Real
- *
- +
- -
- /
- <
- ≤
- >
- ≥
- ↑
- ~
- abs
- fromNatural
- inv
- max
- min
- Natural
- Relation
- wellFounded
Assumptions
⊦ ⊤
⊦ pred_set.FINITE pred_set.EMPTY
⊦ wellFounded (<)
⊦ ¬pred_set.FINITE pred_set.UNIV
⊦ pred_set.EMPTY = λx. ⊥
⊦ pred_set.UNIV = λx. ⊤
⊦ pred_set.CARD pred_set.EMPTY = 0
⊦ pred_set.count 0 = pred_set.EMPTY
⊦ ∀x. x = x
⊦ ∀t. ⊥ ⇒ t
⊦ ∀n. pred_set.FINITE (pred_set.count n)
⊦ ∀n. 0 ≤ n
⊦ ∀m. m ≤ m
⊦ ∀x. x ≤ x
⊦ ∀s. pred_set.SUBSET s pred_set.UNIV
⊦ ∀s. pred_set.SUBSET s s
⊦ bool.IN = λx f. f x
⊦ 1 = suc 0
⊦ arithmetic.DIV2 (bit1 x) = x
⊦ ¬¬p ⇒ p
⊦ ∀x. ¬bool.IN x pred_set.EMPTY
⊦ ∀x. id x = x
⊦ ∀x. marker.unint x = x
⊦ ∀t. t ∨ ¬t
⊦ ∀x. marker.Abbrev x ⇔ x
⊦ ∀n. ¬(n < n)
⊦ ∀n. 0 < factorial n
⊦ ∀n. 0 < suc n
⊦ ∀m. m ≤ suc m
⊦ (¬) = λt. t ⇒ ⊥
⊦ (∃) = λP. P ((select) P)
⊦ ∀t. (∀x. t) ⇔ t
⊦ ∀t. (∃x. t) ⇔ t
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λP. P = λx. ⊤
⊦ arithmetic.BIT2 0 = suc 1
⊦ integer.int_neg (integer.int_of_num 0) = integer.int_of_num 0
⊦ ¬(p ⇒ q) ⇒ p
⊦ ∀x. x = x ⇔ ⊤
⊦ ∀x. pred_set.DELETE pred_set.EMPTY x = pred_set.EMPTY
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀x. integer.int_neg (integer.int_neg x) = x
⊦ ∀n. ¬(0 = suc n)
⊦ ∀n. ¬(suc n = 0)
⊦ ∀n. ¬(suc n = n)
⊦ ∀n. ¬(suc n ≤ 0)
⊦ ∀n. even (arithmetic.BIT2 0 * n)
⊦ ∀n. integer.Num (integer.int_of_num n) = n
⊦ ∀c. arithmetic.- c c = 0
⊦ ∀f. pred_set.IMAGE f pred_set.EMPTY = pred_set.EMPTY
⊦ flip = λf x y. f y x
⊦ ¬(p ⇒ q) ⇒ ¬q
⊦ ¬(p ∨ q) ⇒ ¬p
⊦ ¬(p ∨ q) ⇒ ¬q
⊦ ∀t1 t2. (let x ← t2 in t1) = t1
⊦ ∀A. A ⇒ ¬A ⇒ ⊥
⊦ ∀t. ¬t ⇒ t ⇒ ⊥
⊦ ∀t. (t ⇒ ⊥) ⇒ ¬t
⊦ ∀x. integer.int_add x (integer.int_of_num 0) = x
⊦ ∀x. integer.int_sub x (integer.int_of_num 0) = x
⊦ ∀n. odd (suc (arithmetic.BIT2 0 * n))
⊦ ∀n. even n ⇔ ¬odd n
⊦ ∀n. odd n ⇔ ¬even n
⊦ ∀m. m * 1 = m
⊦ ∀x. 0 + x = x
⊦ Combinator.s = λf g x. f x (g x)
⊦ ∀m n. m ≤ m + n
⊦ ∀n m. arithmetic.- n m ≤ n
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. t ⇒ ⊥ ⇔ t ⇔ ⊥
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀x. integer.int_mul (integer.int_of_num 0) x = integer.int_of_num 0
⊦ ∀x. integer.int_sub (integer.int_of_num 0) x = integer.int_neg x
⊦ ∀x. integer.int_mul (integer.int_of_num 1) x = x
⊦ ∀m. prim_rec.PRE m = arithmetic.- m 1
⊦ ∀m. suc m = m + 1
⊦ ∀n. suc n = 1 + n
⊦ ∀n. n ≤ 0 ⇔ n = 0
⊦ ∀m. 0 = m ∨ 0 < m
⊦ ∀m. arithmetic.- (suc m) 1 = m
⊦ ∀x. x ↑ 0 = 1
⊦ ∀x. ~x + x = 0
⊦ ∀x. 1 * x = x
⊦ ∀s.
pred_set.DISJOINT pred_set.EMPTY s ∧ pred_set.DISJOINT s pred_set.EMPTY
⊦ ∀x. (fst x, snd x) = x
⊦ ∀x y. fst (x, y) = x
⊦ ∀x y. snd (x, y) = y
⊦ ∀h t. head (h :: t) = h
⊦ ∀h t. tail (h :: t) = t
⊦ ∀x s. ¬(pred_set.INSERT x s = pred_set.EMPTY)
⊦ ∀b t. (if b then t else t) = t
⊦ ∀m n. m < m + suc n
⊦ ∀a1 a0. ¬(a0 :: a1 = [])
⊦ ∀f x. bool.LET f x = f x
⊦ ∀P x. P x ⇒ P ((select) P)
⊦ ∀P x. bool.IN x P ⇔ P x
⊦ pair.pair_CASE (x, y) f = f x y
⊦ ∀n. pred_set.count (suc n) = pred_set.INSERT n (pred_set.count n)
⊦ ∀n. ¬(n = 0) ⇔ 0 < n
⊦ ∀l. length l = 0 ⇔ l = []
⊦ ∀x. ∃q r. x = (q, r)
⊦ (∀%%genvar%%2721. P %%genvar%%2721) ⇔ P ⊤ ∧ P ⊥
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀x s. pred_set.FINITE (pred_set.INSERT x s) ⇔ pred_set.FINITE s
⊦ ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1
⊦ ∀A B. A ∨ B ⇔ B ∨ A
⊦ ∀y x. integer.int_add x y = integer.int_add y x
⊦ ∀x y. integer.int_add (integer.int_sub x y) y = x
⊦ ∀m n. m > n ⇔ n < m
⊦ ∀n m. n ≥ m ⇔ m ≤ n
⊦ ∀m n. m * n = n * m
⊦ ∀m n. m + n = n + m
⊦ ∀m n. m < n ∨ n ≤ m
⊦ ∀m n. m ≤ n ∨ n ≤ m
⊦ ∀a c. arithmetic.- (a + c) c = a
⊦ ∀x y. x > y ⇔ y < x
⊦ ∀x y. x ≥ y ⇔ y ≤ x
⊦ ∀x y. x * y = y * x
⊦ ∀x y. x + y = y + x
⊦ ∀x y. x ≤ y ∨ y ≤ x
⊦ ∀s t. pred_set.DISJOINT s t ⇔ pred_set.DISJOINT t s
⊦ ∀s t. pred_set.UNION s t = pred_set.UNION t s
⊦ ∀s. pred_set.FINITE s ⇒ ∀f. pred_set.FINITE (pred_set.IMAGE f s)
⊦ ∀s. pred_set.FINITE s ⇒ ∀t. pred_set.FINITE (pred_set.DIFF s t)
⊦ ∀s. pred_set.FINITE s ⇒ ∀t. pred_set.FINITE (pred_set.INTER s t)
⊦ ∀R f. wellFounded R ⇒ wellFounded (relation.inv_image R f)
⊦ (¬A ⇒ ⊥) ⇒ (A ⇒ ⊥) ⇒ ⊥
⊦ ∀n. bit1 n = n + (n + suc 0)
⊦ ∀n. 0 < n ⇒ 0 div n = 0
⊦ ∀f g. f ∘ g = λx. f (g x)
⊦ ∀x s. pred_set.COMPL s x ⇔ ¬bool.IN x s
⊦ ∀A B. A ⇒ B ⇔ ¬A ∨ B
⊦ ∀x y. integer.int_le x y ⇔ ¬integer.int_lt y x
⊦ ∀x y. integer.int_sub x y = integer.int_add x (integer.int_neg y)
⊦ ∀x y. ¬integer.int_le x y ⇔ integer.int_lt y x
⊦ ∀x y. integer.int_neg (integer.int_sub x y) = integer.int_sub y x
⊦ ∀x y. integer.int_sub x (integer.int_neg y) = integer.int_add x y
⊦ ∀m n. m < n ⇔ suc m ≤ n
⊦ ∀m n. m < n ⇒ m < suc n
⊦ ∀m n. m < n ⇒ suc m ≤ n
⊦ ∀m n. ¬(m < n) ⇔ n ≤ m
⊦ ∀m n. ¬(m ≤ n) ⇔ n < m
⊦ ∀m n. bool.IN m (pred_set.count n) ⇔ m < n
⊦ ∀m n. suc m ≤ n ⇒ m < n
⊦ ∀m. m = 0 ∨ ∃n. m = suc n
⊦ ∀x y. x < y ⇔ ¬(y ≤ x)
⊦ ∀x y. x - y = x + ~y
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ ∀x.
integer.int_le (integer.int_of_num 0) (integer.int_neg x) ⇔
integer.int_le x (integer.int_of_num 0)
⊦ ∀x.
integer.int_lt (integer.int_of_num 0) (integer.int_neg x) ⇔
integer.int_lt x (integer.int_of_num 0)
⊦ ∀i.
integer.int_of_num (integer.Num i) = i ⇔
integer.int_le (integer.int_of_num 0) i
⊦ ∀n. arithmetic.BIT2 n = n + (n + suc (suc 0))
⊦ ∀P. ¬(∀x. P x) ⇔ ∃x. ¬P x
⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ prim_rec.PRE 0 = 0 ∧ ∀m. prim_rec.PRE (suc m) = m
⊦ ∀x y.
integer.int_neg (integer.int_mul x y) =
integer.int_mul x (integer.int_neg y)
⊦ ∀x y.
integer.int_neg (integer.int_mul x y) =
integer.int_mul (integer.int_neg x) y
⊦ ∀x y. integer.int_neg x = integer.int_neg y ⇔ x = y
⊦ ∀x y.
integer.int_le (integer.int_neg x) (integer.int_neg y) ⇔
integer.int_le y x
⊦ ∀m n. ¬(m < n ∧ n < suc m)
⊦ ∀r n. r < n ⇒ r div n = 0
⊦ ∀n k. k < n ⇒ k mod n = k
⊦ ∀m n. ¬(m ≤ n) ⇔ suc n ≤ m
⊦ ∀m n. suc (m + n) = m + suc n
⊦ ∀m n. suc (m + n) = suc n + m
⊦ ∀n m. ¬(suc n ≤ m) ⇔ m ≤ n
⊦ ∀m n. integer.int_of_num m = integer.int_of_num n ⇔ m = n
⊦ ∀m n. suc m = suc n ⇔ m = n
⊦ ∀m n. fromNatural m = fromNatural n ⇔ m = n
⊦ ∀m n.
integer.int_le (integer.int_of_num m) (integer.int_of_num n) ⇔ m ≤ n
⊦ ∀m n.
integer.int_lt (integer.int_of_num m) (integer.int_of_num n) ⇔ m < n
⊦ ∀m n. suc m < suc n ⇔ m < n
⊦ ∀n m. suc n ≤ suc m ⇔ n ≤ m
⊦ ∀m n. arithmetic.- m n = 0 ⇔ m ≤ n
⊦ ∀n m. arithmetic.- (suc n) (suc m) = arithmetic.- n m
⊦ ∀n. even n ⇔ ∃m. n = arithmetic.BIT2 0 * m
⊦ ∀s t. pred_set.DISJOINT s t ⇔ pred_set.INTER s t = pred_set.EMPTY
⊦ ∀s. pred_set.FINITE s ⇒ ∀t. pred_set.SUBSET t s ⇒ pred_set.FINITE t
⊦ ∀m. arithmetic.- 0 m = 0 ∧ arithmetic.- m 0 = m
⊦ ∀x. abs x = if 0 ≤ x then x else ~x
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀f. id ∘ f = f ∧ f ∘ id = f
⊦ ∀s. pred_set.FINITE s ⇒ (pred_set.CARD s = 0 ⇔ s = pred_set.EMPTY)
⊦ ∀P.
pred_set.CROSS P pred_set.EMPTY = pred_set.EMPTY ∧
pred_set.CROSS pred_set.EMPTY P = pred_set.EMPTY
⊦ ∀x s. ¬bool.IN x s ⇔ pred_set.DELETE s x = s
⊦ ∀x y.
integer.int_neg (integer.int_add x y) =
integer.int_add (integer.int_neg x) (integer.int_neg y)
⊦ ∀x y.
integer.int_le y (integer.int_add x y) ⇔
integer.int_le (integer.int_of_num 0) x
⊦ ∀m n. ¬(n = 0) ⇒ m < m + n
⊦ ∀m n.
integer.int_add (integer.int_of_num m) (integer.int_of_num n) =
integer.int_of_num (m + n)
⊦ ∀m n. fromNatural m + fromNatural n = fromNatural (m + n)
⊦ ∀n. odd n ⇔ ∃m. n = suc (arithmetic.BIT2 0 * m)
⊦ ∀x n. x ↑ suc n = x * x ↑ n
⊦ ∀x y. max x y = if x ≤ y then y else x
⊦ ∀x y. min x y = if x ≤ y then x else y
⊦ ∀s t.
pred_set.FINITE (pred_set.UNION s t) ⇔
pred_set.FINITE s ∧ pred_set.FINITE t
⊦ ∀P Q.
pred_set.FINITE P ∧ pred_set.FINITE Q ⇒
pred_set.FINITE (pred_set.CROSS P Q)
⊦ ∀R f. relation.inv_image R f = λx y. R (f x) (f y)
⊦ ∀m n. m ≤ n ⇔ ∃p. n = m + p
⊦ ∀n m. n < m ⇒ ∀p. n < m + p
⊦ ∀m n. m ≤ n ⇒ ∃k. m = arithmetic.- n k
⊦ ∀m n. m ≤ n ⇒ ∃p. n = m + p
⊦ ∀f g. f = g ⇔ ∀x. f x = g x
⊦ ∀f v. (∀x. x = v ⇒ f x) ⇔ f v
⊦ ∀P a. (∃x. x = a ∧ P x) ⇔ P a
⊦ ∀f x y. pair.UNCURRY f (x, y) = f x y
⊦ (∨) = λt1 t2. ∀t. (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t
⊦ (even 0 ⇔ ⊤) ∧ ∀n. even (suc n) ⇔ ¬even n
⊦ (odd 0 ⇔ ⊥) ∧ ∀n. odd (suc n) ⇔ ¬odd n
⊦ ∀t1 t2. (t1 ⇔ t2) ⇔ (t1 ⇒ t2) ∧ (t2 ⇒ t1)
⊦ ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)
⊦ ∀x y.
x = y ⇔ integer.int_of_num 0 = integer.int_add y (integer.int_neg x)
⊦ ∀x y.
integer.int_le x y ⇔
integer.int_le (integer.int_of_num 0)
(integer.int_add y (integer.int_neg x))
⊦ ∀x y.
integer.int_lt x y ⇔
integer.int_le (integer.int_add x (integer.int_of_num 1)) y
⊦ ∀x y. integer.int_le x y ∧ integer.int_le y x ⇔ x = y
⊦ ∀m n. m = n ⇔ m ≤ n ∧ n ≤ m
⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n
⊦ ∀m n. n ≤ m ⇒ arithmetic.- m n + n = m
⊦ ∀m n. m = n ∨ m < n ∨ n < m
⊦ ∀n m. n ≤ m ∧ m ≤ n ⇒ n = m
⊦ ∀n. 0 < n ⇒ ∀k. k * n mod n = 0
⊦ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y
⊦ ∀s t. pred_set.SUBSET s t ∧ pred_set.SUBSET t s ⇒ s = t
⊦ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)
⊦ (∀n. P (integer.int_of_num n)) ⇔
∀x. integer.int_le (integer.int_of_num 0) x ⇒ P x
⊦ (∀s. pred_set.INTER pred_set.EMPTY s = pred_set.EMPTY) ∧
∀s. pred_set.INTER s pred_set.EMPTY = pred_set.EMPTY
⊦ (∀s. pred_set.UNION pred_set.EMPTY s = s) ∧
∀s. pred_set.UNION s pred_set.EMPTY = s
⊦ ¬(¬A ∨ B) ⇒ ⊥ ⇔ A ⇒ ¬B ⇒ ⊥
⊦ ∀x s. bool.IN x s ⇒ ∀f. bool.IN (f x) (pred_set.IMAGE f s)
⊦ ∀P. (∀x y. P x y) ⇔ ∀y x. P x y
⊦ ∀f v. pred_set.GSPEC f v ⇔ ∃x. (v, ⊤) = f x
⊦ ∀P Q. (∀x. P ⇒ Q x) ⇔ P ⇒ ∀x. Q x
⊦ ∀P Q. (∀x. P ∨ Q x) ⇔ P ∨ ∀x. Q x
⊦ ∀Q P. (∀x. P x ∨ Q) ⇔ (∀x. P x) ∨ Q
⊦ ∀P Q. (∃x. P ∧ Q x) ⇔ P ∧ ∃x. Q x
⊦ ∀P Q. P ∧ (∀x. Q x) ⇔ ∀x. P ∧ Q x
⊦ ∀P Q. P ∨ (∃x. Q x) ⇔ ∃x. P ∨ Q x
⊦ ∀m n. m < suc n ⇔ m = n ∨ m < n
⊦ ∀m n. m < suc n ⇒ m = n ∨ m < n
⊦ ∀P Q. (∀x. P x ⇒ Q) ⇔ (∃x. P x) ⇒ Q
⊦ ∀P Q. (∃x. P x ∧ Q) ⇔ (∃x. P x) ∧ Q
⊦ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q
⊦ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q
⊦ ¬(A ∨ B) ⇒ ⊥ ⇔ (A ⇒ ⊥) ⇒ ¬B ⇒ ⊥
⊦ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∧ z ⇒ y ∧ w
⊦ (y ⇒ x) ∧ (z ⇒ w) ⇒ (x ⇒ z) ⇒ y ⇒ w
⊦ ∀x y z. x = y ∧ y = z ⇒ x = z
⊦ ∀x y s.
pred_set.INSERT x (pred_set.INSERT y s) =
pred_set.INSERT y (pred_set.INSERT x s)
⊦ ∀x sos. pred_set.BIGUNION sos x ⇔ ∃s. bool.IN x s ∧ bool.IN s sos
⊦ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3
⊦ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3
⊦ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C
⊦ ∀z y x.
integer.int_add x (integer.int_add y z) =
integer.int_add (integer.int_add x y) z
⊦ ∀x y z. integer.int_add x y = integer.int_add x z ⇔ y = z
⊦ ∀x y z. integer.int_le x y ∧ integer.int_le y z ⇒ integer.int_le x z
⊦ ∀m n p. m ≤ n ⇒ m * p ≤ n * p
⊦ ∀m n p. m < arithmetic.- n p ⇔ m + p < n
⊦ ∀m n p. m ≥ arithmetic.- n p ⇔ m + p ≥ n
⊦ ∀m n p. arithmetic.- m n ≤ p ⇔ m ≤ n + p
⊦ ∀m n p. m + (n + p) = m + n + p
⊦ ∀m n p. m + p = n + p ⇔ m = n
⊦ ∀m n p. m + p < n + p ⇔ m < n
⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p
⊦ ∀m n p. m < n ∧ n < p ⇒ m < p
⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p
⊦ ∀m n p. m ≤ n ∧ n < p ⇒ m < p
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀x y z. y ≤ z ⇒ x + y ≤ x + z
⊦ ∀x y z. x * (y * z) = x * y * z
⊦ ∀x y z. x + (y + z) = x + y + z
⊦ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
⊦ ∀x. ¬(x = 0) ⇒ inv x * x = 1
⊦ ∀P x. (∀y. P y ⇔ y = x) ⇒ (select) P = x
⊦ ∀s t u. pred_set.SUBSET s t ∧ pred_set.SUBSET t u ⇒ pred_set.SUBSET s u
⊦ ∀s t. s = t ⇔ ∀x. bool.IN x s ⇔ bool.IN x t
⊦ ∀s t. pred_set.SUBSET s t ⇔ ∀x. bool.IN x s ⇒ bool.IN x t
⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x)
⊦ ∀f v. bool.IN v (pred_set.GSPEC f) ⇔ ∃x. (v, ⊤) = f x
⊦ (∀x. P x ⇒ Q x) ⇒ (∀x. P x) ⇒ ∀x. Q x
⊦ (∀x. P x ⇒ Q x) ⇒ (∃x. P x) ⇒ ∃x. Q x
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1 ∧ (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (t1 ⇔ t2) ⇔ t1 ∧ t2 ∨ ¬t1 ∧ ¬t2
⊦ ∀n m. arithmetic.- n m = if m < n then numeral.iSUB ⊤ n m else 0
⊦ ∀m n. 0 < n ⇒ (m = prim_rec.PRE n ⇔ suc m = n)
⊦ ∀m n. arithmetic.- m n = m ⇔ m = 0 ∨ n = 0
⊦ ∀m n. m * n = 0 ⇔ m = 0 ∨ n = 0
⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0
⊦ ∀m n. ¬(m < n) ∧ ¬(m = n) ⇒ n < m
⊦ length [] = 0 ∧ ∀h t. length (h :: t) = suc (length t)
⊦ ∀x y z.
x = integer.int_add y z ⇔ integer.int_add x (integer.int_neg y) = z
⊦ ∀x y z.
integer.int_le x (integer.int_add y z) ⇔
integer.int_le (integer.int_add x (integer.int_neg z)) y
⊦ ∀m n. n < m ⇒ ∃p. m = n + (p + 1)
⊦ ∀f x s.
pred_set.IMAGE f (pred_set.INSERT x s) =
pred_set.INSERT (f x) (pred_set.IMAGE f s)
⊦ ∀P. P 0 ∧ (∀n. P n ⇒ P (suc n)) ⇒ ∀n. P n
⊦ 0 < n ⇒ (k mod n = 0 ⇔ ∃d. k = d * n)
⊦ factorial 0 = 1 ∧ ∀n. factorial (suc n) = suc n * factorial n
⊦ (∀t. ¬¬t ⇔ t) ∧ (¬⊤ ⇔ ⊥) ∧ (¬⊥ ⇔ ⊤)
⊦ ∀m n. ¬(m = n) ⇔ suc m ≤ n ∨ suc n ≤ m
⊦ ∀x y. ¬(y = 0) ⇒ x / y = x * inv y
⊦ integer.int_of_num 0 = integer.int_add c x ⇒
(integer.int_le (integer.int_of_num 0) (integer.int_add c y) ⇔
integer.int_le x y)
⊦ ∀x y s. bool.IN x (pred_set.INSERT y s) ⇔ x = y ∨ bool.IN x s
⊦ ∀A B C. A ∨ B ∧ C ⇔ (A ∨ B) ∧ (A ∨ C)
⊦ ∀A B C. (B ∨ C) ∧ A ⇔ B ∧ A ∨ C ∧ A
⊦ ∀A B C. B ∧ C ∨ A ⇔ (B ∨ A) ∧ (C ∨ A)
⊦ ∀x y z.
integer.int_mul (integer.int_add x y) z =
integer.int_add (integer.int_mul x z) (integer.int_mul y z)
⊦ ∀m n p. p * arithmetic.- m n = arithmetic.- (p * m) (p * n)
⊦ ∀m n p. p * (m + n) = p * m + p * n
⊦ ∀m n p. (m + n) * p = m * p + n * p
⊦ ∀n r. r < n ⇒ ∀q. (q * n + r) div n = q
⊦ ∀n. 0 < n ⇒ n div n = 1 ∧ n mod n = 0
⊦ ∀x y z. x * (y + z) = x * y + x * z
⊦ ∀f.
(∀s. pred_set.INJ f pred_set.EMPTY s) ∧
∀s. pred_set.INJ f s pred_set.EMPTY ⇔ s = pred_set.EMPTY
⊦ ∀s t x. bool.IN x (pred_set.INTER s t) ⇔ bool.IN x s ∧ bool.IN x t
⊦ ∀s t x. bool.IN x (pred_set.UNION s t) ⇔ bool.IN x s ∨ bool.IN x t
⊦ ∀P. integer.LEAST_INT P = select i. P i ∧ ∀j. integer.int_lt j i ⇒ ¬P j
⊦ (∃!) = λP. (∃) P ∧ ∀x y. P x ∧ P y ⇒ x = y
⊦ ∀b f g x. (if b then f else g) x = if b then f x else g x
⊦ ∀n m.
¬(m = 0) ⇒
integer.int_div (integer.int_of_num n) (integer.int_of_num m) =
integer.int_of_num (n div m)
⊦ ∀f b x y. f (if b then x else y) = if b then f x else f y
⊦ ∀f R y z. R y z ⇒ relation.RESTRICT f R z y = f y
⊦ ∀P Q. (∃x. P x) ∧ (∀x. P x ⇒ Q x) ⇒ Q ((select) P)
⊦ ∀x s t.
pred_set.DISJOINT (pred_set.INSERT x s) t ⇔
pred_set.DISJOINT s t ∧ ¬bool.IN x t
⊦ ∀s x y. bool.IN x (pred_set.DELETE s y) ⇔ bool.IN x s ∧ ¬(x = y)
⊦ ∀s t x. bool.IN x (pred_set.DIFF s t) ⇔ bool.IN x s ∧ ¬bool.IN x t
⊦ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x
⊦ ∀P Q. (∃x. P x ∨ Q x) ⇔ (∃x. P x) ∨ ∃x. Q x
⊦ ∀s. s = pred_set.EMPTY ∨ ∃x t. s = pred_set.INSERT x t ∧ ¬bool.IN x t
⊦ ∀e f. ∃!fn1. fn1 0 = e ∧ ∀n. fn1 (suc n) = f (fn1 n) n
⊦ ∀e f. ∃fn. fn 0 = e ∧ ∀n. fn (suc n) = f n (fn n)
⊦ ∀x y.
integer.int_le (integer.int_of_num 0) x ∧
integer.int_le (integer.int_of_num 0) y ⇒
integer.int_le (integer.int_of_num 0) (integer.int_add x y)
⊦ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
⊦ ∀P. (∃n. P n) ⇒ ∃n. P n ∧ ∀m. m < n ⇒ ¬P m
⊦ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h :: t)) ⇒ ∀l. P l
⊦ pred_set.SUBSET s t ⇒
pred_set.UNION s (pred_set.DIFF t s) = t ∧
pred_set.UNION (pred_set.DIFF t s) s = t
⊦ integer.int_of_num 0 = integer.int_add c x ⇒
(integer.int_le (integer.int_of_num 0)
(integer.int_add (integer.int_neg c) y) ⇔
integer.int_le (integer.int_neg x) y)
⊦ integer.int_le (integer.int_of_num 0) (integer.int_add c x) ⇒
integer.int_le x y ⇒
(integer.int_le (integer.int_of_num 0) (integer.int_add c y) ⇔ ⊤)
⊦ integer.int_le (integer.int_of_num 0) (integer.int_add c x) ⇒
integer.int_lt x y ⇒ (integer.int_of_num 0 = integer.int_add c y ⇔ ⊥)
⊦ (∀t1 t2. (if ⊤ then t1 else t2) = t1) ∧
∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀m n p. m ≤ arithmetic.- n p ⇔ m + p ≤ n ∨ m ≤ 0
⊦ ∀m n p. arithmetic.- m n < p ⇔ m < n + p ∧ 0 < p
⊦ ∀b c.
c ≤ b ⇒ ∀a. arithmetic.- a (arithmetic.- b c) = arithmetic.- (a + c) b
⊦ ∀P Q x.
bool.IN x (pred_set.CROSS P Q) ⇔ bool.IN (fst x) P ∧ bool.IN (snd x) Q
⊦ ∀p. (∃n. p n) ⇒ p (while.LEAST p) ∧ ∀n. n < while.LEAST p ⇒ ¬p n
⊦ (∀n. 0 + n = n) ∧ ∀m n. suc m + n = suc (m + n)
⊦ ∀y s f. bool.IN y (pred_set.IMAGE f s) ⇔ ∃x. y = f x ∧ bool.IN x s
⊦ ∀s.
pred_set.FINITE s ⇒
∀x.
pred_set.CARD (pred_set.INSERT x s) =
if bool.IN x s then pred_set.CARD s else suc (pred_set.CARD s)
⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b
⊦ ∀a0 a1 a0' a1'. a0 :: a1 = a0' :: a1' ⇔ a0 = a0' ∧ a1 = a1'
⊦ (∃!x. P x) ⇔ (∃x. P x) ∧ ∀x y. P x ∧ P y ⇒ x = y
⊦ integer.int_le (integer.int_of_num 0) (integer.int_add c x) ⇒
integer.int_lt x (integer.int_neg y) ⇒
(integer.int_of_num 0 = integer.int_add (integer.int_neg c) y ⇔ ⊥)
⊦ integer.int_le (integer.int_of_num 0) (integer.int_add c x) ⇒
integer.int_lt y (integer.int_neg x) ⇒
(integer.int_le (integer.int_of_num 0)
(integer.int_add (integer.int_neg c) y) ⇔ ⊥)
⊦ ∀n.
numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n) ∧
numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n) ∧
numeral.iDUB 0 = 0
⊦ (∀n. n ↑ 0 = 1) ∧ ∀m n. m ↑ suc n = m * m ↑ n
⊦ (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)
⊦ (p ⇔ q ∨ r) ⇔ (p ∨ ¬q) ∧ (p ∨ ¬r) ∧ (q ∨ r ∨ ¬p)
⊦ integer.int_le (integer.int_of_num 0) (integer.int_add c x) ⇒
(integer.int_le (integer.int_of_num 0)
(integer.int_add (integer.int_neg c) (integer.int_neg x)) ⇔
integer.int_of_num 0 = integer.int_add c x)
⊦ ∀x s t.
pred_set.INTER (pred_set.INSERT x s) t =
if bool.IN x t then pred_set.INSERT x (pred_set.INTER s t)
else pred_set.INTER s t
⊦ ∀x s t.
pred_set.UNION (pred_set.INSERT x s) t =
if bool.IN x t then pred_set.UNION s t
else pred_set.INSERT x (pred_set.UNION s t)
⊦ ∀f0 f1. ∃fn. fn [] = f0 ∧ ∀a0 a1. fn (a0 :: a1) = f1 a0 a1 (fn a1)
⊦ ∀x y z. 0 < z ⇒ (x < y div z ⇔ (x + 1) * z ≤ y)
⊦ ∀R. wellFounded R ⇒ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x
⊦ (∀v f. arithmetic.num_CASE 0 v f = v) ∧
∀n v f. arithmetic.num_CASE (suc n) v f = f n
⊦ ∀x x' y y'. (x ⇔ x') ∧ (x' ⇒ (y ⇔ y')) ⇒ (x ⇒ y ⇔ x' ⇒ y')
⊦ ∀n k q. (∃r. k = q * n + r ∧ r < n) ⇒ k div n = q
⊦ ∀f.
(∀x y. f x = f y ⇔ x = y) ⇒
∀s. pred_set.FINITE (pred_set.IMAGE f s) ⇔ pred_set.FINITE s
⊦ (p ⇔ q ∧ r) ⇔ (p ∨ ¬q ∨ ¬r) ∧ (q ∨ ¬p) ∧ (r ∨ ¬p)
⊦ ∀m n p. m = arithmetic.- n p ⇔ m + p = n ∨ m ≤ 0 ∧ n ≤ p
⊦ P (arithmetic.- a b) ⇔ ∀d. (b = a + d ⇒ P 0) ∧ (a = b + d ⇒ P d)
⊦ ∀A B. (¬(A ∧ B) ⇔ ¬A ∨ ¬B) ∧ (¬(A ∨ B) ⇔ ¬A ∧ ¬B)
⊦ ∀n. 0 < n ⇒ ∀k. k = (k div n) * n + k mod n ∧ k mod n < n
⊦ ∀M R f.
f = relation.WFREC R M ⇒ wellFounded R ⇒
∀x. f x = M (relation.RESTRICT f R x) x
⊦ (∀f. map f [] = []) ∧ ∀f h t. map f (h :: t) = f h :: map f t
⊦ (∀P. all P [] ⇔ ⊤) ∧ ∀P h t. all P (h :: t) ⇔ P h ∧ all P t
⊦ (∀m. arithmetic.- 0 m = 0) ∧
∀m n.
arithmetic.- (suc m) n = if m < n then 0 else suc (arithmetic.- m n)
⊦ ∀n.
even 0 ∧ even (arithmetic.BIT2 n) ∧ ¬even (bit1 n) ∧ ¬odd 0 ∧
¬odd (arithmetic.BIT2 n) ∧ odd (bit1 n)
⊦ ∀s f b.
pred_set.FINITE s ⇒
pred_set.ITSET f s b =
if s = pred_set.EMPTY then b
else pred_set.ITSET f (pred_set.REST s) (f (pred_set.CHOICE s) b)
⊦ (∀n. n ≤ 0 ⇔ n = 0) ∧ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n
⊦ bool.TYPE_DEFINITION =
λP rep.
(∀x' x''. rep x' = rep x'' ⇒ x' = x'') ∧ ∀x. P x ⇔ ∃x'. x = rep x'
⊦ ∀t. ((⊤ ⇔ t) ⇔ t) ∧ ((t ⇔ ⊤) ⇔ t) ∧ ((⊥ ⇔ t) ⇔ ¬t) ∧ ((t ⇔ ⊥) ⇔ ¬t)
⊦ ∀P.
(∃rep. bool.TYPE_DEFINITION P rep) ⇒
∃rep abs. (∀a. abs (rep a) = a) ∧ ∀r. P r ⇔ rep (abs r) = r
⊦ (m ≤ m * n ⇔ m = 0 ∨ 0 < n) ∧ (m ≤ n * m ⇔ m = 0 ∨ 0 < n)
⊦ ∀Q P.
(∃n. P n) ∧ (∀n. (∀m. m < n ⇒ ¬P m) ∧ P n ⇒ Q n) ⇒ Q (while.LEAST P)
⊦ numeral.texp_help 0 acc = arithmetic.BIT2 acc ∧
numeral.texp_help (bit1 n) acc =
numeral.texp_help (prim_rec.PRE (bit1 n)) (bit1 acc) ∧
numeral.texp_help (arithmetic.BIT2 n) acc =
numeral.texp_help (bit1 n) (bit1 acc)
⊦ ∀p.
(∃n. p = integer.int_of_num n ∧ ¬(n = 0)) ∨
(∃n. p = integer.int_neg (integer.int_of_num n) ∧ ¬(n = 0)) ∨
p = integer.int_of_num 0
⊦ numeral.exactlog 0 = 0 ∧ (∀n. numeral.exactlog (bit1 n) = 0) ∧
∀n.
numeral.exactlog (arithmetic.BIT2 n) =
bool.LET (λx. if x = 0 then 0 else bit1 x) (numeral.onecount n 0)
⊦ (∀x. numeral.onecount 0 x = x) ∧
(∀n x. numeral.onecount (bit1 n) x = numeral.onecount n (suc x)) ∧
∀n x. numeral.onecount (arithmetic.BIT2 n) x = 0
⊦ ∀P.
P pred_set.EMPTY ∧
(∀s.
pred_set.FINITE s ∧ P s ⇒
∀e. ¬bool.IN e s ⇒ P (pred_set.INSERT e s)) ⇒
∀s. pred_set.FINITE s ⇒ P s
⊦ ∀t. (⊤ ∧ t ⇔ t) ∧ (t ∧ ⊤ ⇔ t) ∧ (⊥ ∧ t ⇔ ⊥) ∧ (t ∧ ⊥ ⇔ ⊥) ∧ (t ∧ t ⇔ t)
⊦ ∀t. (⊤ ∨ t ⇔ ⊤) ∧ (t ∨ ⊤ ⇔ ⊤) ∧ (⊥ ∨ t ⇔ t) ∧ (t ∨ ⊥ ⇔ t) ∧ (t ∨ t ⇔ t)
⊦ factorial 0 = 1 ∧
(∀n. factorial (bit1 n) = bit1 n * factorial (prim_rec.PRE (bit1 n))) ∧
∀n.
factorial (arithmetic.BIT2 n) = arithmetic.BIT2 n * factorial (bit1 n)
⊦ 0 + m = m ∧ m + 0 = m ∧ suc m + n = suc (m + n) ∧ m + suc n = suc (m + n)
⊦ ∀t. (⊤ ⇒ t ⇔ t) ∧ (t ⇒ ⊤ ⇔ ⊤) ∧ (⊥ ⇒ t ⇔ ⊤) ∧ (t ⇒ t ⇔ ⊤) ∧ (t ⇒ ⊥ ⇔ ¬t)
⊦ ∀P Q x x' y y'.
(P ⇔ Q) ∧ (Q ⇒ x = x') ∧ (¬Q ⇒ y = y') ⇒
(if P then x else y) = if Q then x' else y'
⊦ (p ⇔ q ⇔ r) ⇔ (p ∨ q ∨ r) ∧ (p ∨ ¬r ∨ ¬q) ∧ (q ∨ ¬r ∨ ¬p) ∧ (r ∨ ¬q ∨ ¬p)
⊦ ∀f g.
(∀n. g (suc n) = f n (suc n)) ⇔
(∀n. g (bit1 n) = f (arithmetic.- (bit1 n) 1) (bit1 n)) ∧
∀n. g (arithmetic.BIT2 n) = f (bit1 n) (arithmetic.BIT2 n)
⊦ ∀p.
(∃x. p x) ∧ (∃m. ∀x. p x ⇒ x ≤ m) ⇒
∃s. (∀x. p x ⇒ x ≤ s) ∧ ∀m. (∀x. p x ⇒ x ≤ m) ⇒ s ≤ m
⊦ ∀n m.
numeral.internal_mult 0 n = 0 ∧ numeral.internal_mult n 0 = 0 ∧
numeral.internal_mult (bit1 n) m =
numeral.iZ (numeral.iDUB (numeral.internal_mult n m) + m) ∧
numeral.internal_mult (arithmetic.BIT2 n) m =
numeral.iDUB (numeral.iZ (numeral.internal_mult n m + m))
⊦ ∀n m.
0 * n = 0 ∧ n * 0 = 0 ∧
bit1 n * m = numeral.iZ (numeral.iDUB (n * m) + m) ∧
arithmetic.BIT2 n * m = numeral.iDUB (numeral.iZ (n * m + m))
⊦ ∀f s t.
pred_set.INJ f s t ⇔
(∀x. bool.IN x s ⇒ bool.IN (f x) t) ∧
∀x y. bool.IN x s ∧ bool.IN y s ⇒ f x = f y ⇒ x = y
⊦ ∀f e s b.
(∀x y z. f x (f y z) = f y (f x z)) ∧ pred_set.FINITE s ⇒
pred_set.ITSET f (pred_set.INSERT e s) b =
f e (pred_set.ITSET f (pred_set.DELETE s e) b)
⊦ prim_rec.PRE 0 = 0 ∧ prim_rec.PRE 1 = 0 ∧
(∀n.
prim_rec.PRE (bit1 (bit1 n)) =
arithmetic.BIT2 (prim_rec.PRE (bit1 n))) ∧
(∀n.
prim_rec.PRE (bit1 (arithmetic.BIT2 n)) = arithmetic.BIT2 (bit1 n)) ∧
∀n. prim_rec.PRE (arithmetic.BIT2 n) = bit1 n
⊦ (p ⇔ if q then r else s) ⇔
(p ∨ q ∨ ¬s) ∧ (p ∨ ¬r ∨ ¬q) ∧ (p ∨ ¬r ∨ ¬s) ∧ (¬q ∨ r ∨ ¬p) ∧
(q ∨ s ∨ ¬p)
⊦ ∀m n.
0 * m = 0 ∧ m * 0 = 0 ∧ 1 * m = m ∧ m * 1 = m ∧ suc m * n = m * n + n ∧
m * suc n = m + m * n
⊦ ∀n m.
(integer.int_lt (integer.int_of_num n) (integer.int_of_num m) ⇔
n < m) ∧
(integer.int_lt (integer.int_neg (integer.int_of_num n))
(integer.int_neg (integer.int_of_num m)) ⇔ m < n) ∧
(integer.int_lt (integer.int_neg (integer.int_of_num n))
(integer.int_of_num m) ⇔ ¬(n = 0) ∨ ¬(m = 0)) ∧
(integer.int_lt (integer.int_of_num n)
(integer.int_neg (integer.int_of_num m)) ⇔ ⊥)
⊦ (∀m n. integer.int_of_num m = integer.int_of_num n ⇔ m = n) ∧
(∀x y. integer.int_neg x = integer.int_neg y ⇔ x = y) ∧
∀n m.
(integer.int_of_num n = integer.int_neg (integer.int_of_num m) ⇔
n = 0 ∧ m = 0) ∧
(integer.int_neg (integer.int_of_num n) = integer.int_of_num m ⇔
n = 0 ∧ m = 0)
⊦ ∀n m.
(0 ≤ n ⇔ ⊤) ∧ (bit1 n ≤ 0 ⇔ ⊥) ∧ (arithmetic.BIT2 n ≤ 0 ⇔ ⊥) ∧
(bit1 n ≤ bit1 m ⇔ n ≤ m) ∧ (bit1 n ≤ arithmetic.BIT2 m ⇔ n ≤ m) ∧
(arithmetic.BIT2 n ≤ bit1 m ⇔ ¬(m ≤ n)) ∧
(arithmetic.BIT2 n ≤ arithmetic.BIT2 m ⇔ n ≤ m)
⊦ ∀n m.
(0 < bit1 n ⇔ ⊤) ∧ (0 < arithmetic.BIT2 n ⇔ ⊤) ∧ (n < 0 ⇔ ⊥) ∧
(bit1 n < bit1 m ⇔ n < m) ∧
(arithmetic.BIT2 n < arithmetic.BIT2 m ⇔ n < m) ∧
(bit1 n < arithmetic.BIT2 m ⇔ ¬(m < n)) ∧
(arithmetic.BIT2 n < bit1 m ⇔ n < m)
⊦ ∀n m.
(0 = bit1 n ⇔ ⊥) ∧ (bit1 n = 0 ⇔ ⊥) ∧ (0 = arithmetic.BIT2 n ⇔ ⊥) ∧
(arithmetic.BIT2 n = 0 ⇔ ⊥) ∧ (bit1 n = arithmetic.BIT2 m ⇔ ⊥) ∧
(arithmetic.BIT2 n = bit1 m ⇔ ⊥) ∧ (bit1 n = bit1 m ⇔ n = m) ∧
(arithmetic.BIT2 n = arithmetic.BIT2 m ⇔ n = m)
⊦ ∀m n p.
integer.int_mul p (integer.int_of_num 0) = integer.int_of_num 0 ∧
integer.int_mul (integer.int_of_num 0) p = integer.int_of_num 0 ∧
integer.int_mul (integer.int_of_num m) (integer.int_of_num n) =
integer.int_of_num (m * n) ∧
integer.int_mul (integer.int_neg (integer.int_of_num m))
(integer.int_of_num n) =
integer.int_neg (integer.int_of_num (m * n)) ∧
integer.int_mul (integer.int_of_num m)
(integer.int_neg (integer.int_of_num n)) =
integer.int_neg (integer.int_of_num (m * n)) ∧
integer.int_mul (integer.int_neg (integer.int_of_num m))
(integer.int_neg (integer.int_of_num n)) = integer.int_of_num (m * n)
⊦ ∀i j.
¬(j = integer.int_of_num 0) ⇒
integer.int_div i j =
if integer.int_lt (integer.int_of_num 0) j then
if integer.int_le (integer.int_of_num 0) i then
integer.int_of_num (integer.Num i div integer.Num j)
else
integer.int_add
(integer.int_neg
(integer.int_of_num
(integer.Num (integer.int_neg i) div integer.Num j)))
(if integer.Num (integer.int_neg i) mod integer.Num j = 0 then
integer.int_of_num 0
else integer.int_neg (integer.int_of_num 1))
else if integer.int_le (integer.int_of_num 0) i then
integer.int_add
(integer.int_neg
(integer.int_of_num
(integer.Num i div integer.Num (integer.int_neg j))))
(if integer.Num i mod integer.Num (integer.int_neg j) = 0 then
integer.int_of_num 0
else integer.int_neg (integer.int_of_num 1))
else
integer.int_of_num
(integer.Num (integer.int_neg i) div
integer.Num (integer.int_neg j))
⊦ ∀p n m.
integer.int_add (integer.int_of_num 0) p = p ∧
integer.int_add p (integer.int_of_num 0) = p ∧
integer.int_neg (integer.int_of_num 0) = integer.int_of_num 0 ∧
integer.int_neg (integer.int_neg p) = p ∧
integer.int_add (integer.int_of_num n) (integer.int_of_num m) =
integer.int_of_num (numeral.iZ (n + m)) ∧
integer.int_add (integer.int_of_num n)
(integer.int_neg (integer.int_of_num m)) =
(if m ≤ n then integer.int_of_num (arithmetic.- n m)
else integer.int_neg (integer.int_of_num (arithmetic.- m n))) ∧
integer.int_add (integer.int_neg (integer.int_of_num n))
(integer.int_of_num m) =
(if n ≤ m then integer.int_of_num (arithmetic.- m n)
else integer.int_neg (integer.int_of_num (arithmetic.- n m))) ∧
integer.int_add (integer.int_neg (integer.int_of_num n))
(integer.int_neg (integer.int_of_num m)) =
integer.int_neg (integer.int_of_num (numeral.iZ (n + m)))
⊦ 0 * n = 0 ∧ n * 0 = 0 ∧
bit1 x * bit1 y = numeral.internal_mult (bit1 x) (bit1 y) ∧
bit1 x * arithmetic.BIT2 y =
bool.LET
(λn.
if odd n then
numeral.texp_help (arithmetic.DIV2 n) (prim_rec.PRE (bit1 x))
else numeral.internal_mult (bit1 x) (arithmetic.BIT2 y))
(numeral.exactlog (arithmetic.BIT2 y)) ∧
arithmetic.BIT2 x * bit1 y =
bool.LET
(λm.
if odd m then
numeral.texp_help (arithmetic.DIV2 m) (prim_rec.PRE (bit1 y))
else numeral.internal_mult (arithmetic.BIT2 x) (bit1 y))
(numeral.exactlog (arithmetic.BIT2 x)) ∧
arithmetic.BIT2 x * arithmetic.BIT2 y =
bool.LET
(λm.
bool.LET
(λn.
if odd m then
numeral.texp_help (arithmetic.DIV2 m)
(prim_rec.PRE (arithmetic.BIT2 y))
else if odd n then
numeral.texp_help (arithmetic.DIV2 n)
(prim_rec.PRE (arithmetic.BIT2 x))
else
numeral.internal_mult (arithmetic.BIT2 x)
(arithmetic.BIT2 y))
(numeral.exactlog (arithmetic.BIT2 y)))
(numeral.exactlog (arithmetic.BIT2 x))
⊦ ∀n m.
(integer.int_lt (integer.int_of_num 0) (integer.int_of_num (bit1 n)) ⇔
⊤) ∧
(integer.int_lt (integer.int_of_num 0)
(integer.int_of_num (arithmetic.BIT2 n)) ⇔ ⊤) ∧
(integer.int_lt (integer.int_of_num 0) (integer.int_of_num 0) ⇔ ⊥) ∧
(integer.int_lt (integer.int_of_num 0)
(integer.int_neg (integer.int_of_num n)) ⇔ ⊥) ∧
(integer.int_lt (integer.int_of_num n) (integer.int_of_num 0) ⇔ ⊥) ∧
(integer.int_lt (integer.int_neg (integer.int_of_num (bit1 n)))
(integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_lt
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
(integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_lt (integer.int_of_num n) (integer.int_of_num m) ⇔
n < m) ∧
(integer.int_lt (integer.int_neg (integer.int_of_num (bit1 n)))
(integer.int_of_num m) ⇔ ⊤) ∧
(integer.int_lt
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
(integer.int_of_num m) ⇔ ⊤) ∧
(integer.int_lt (integer.int_of_num n)
(integer.int_neg (integer.int_of_num m)) ⇔ ⊥) ∧
(integer.int_lt (integer.int_neg (integer.int_of_num n))
(integer.int_neg (integer.int_of_num m)) ⇔ m < n)
⊦ ∀n m.
(integer.int_le (integer.int_of_num 0) (integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_le (integer.int_of_num 0) (integer.int_of_num n) ⇔ ⊤) ∧
(integer.int_le (integer.int_of_num 0)
(integer.int_neg (integer.int_of_num (bit1 n))) ⇔ ⊥) ∧
(integer.int_le (integer.int_of_num 0)
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) ⇔ ⊥) ∧
(integer.int_le (integer.int_of_num (bit1 n)) (integer.int_of_num 0) ⇔
⊥) ∧
(integer.int_le (integer.int_of_num (arithmetic.BIT2 n))
(integer.int_of_num 0) ⇔ ⊥) ∧
(integer.int_le (integer.int_neg (integer.int_of_num (bit1 n)))
(integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_le
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
(integer.int_of_num 0) ⇔ ⊤) ∧
(integer.int_le (integer.int_of_num n) (integer.int_of_num m) ⇔
n ≤ m) ∧
(integer.int_le (integer.int_of_num n)
(integer.int_neg (integer.int_of_num (bit1 m))) ⇔ ⊥) ∧
(integer.int_le (integer.int_of_num n)
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 m))) ⇔ ⊥) ∧
(integer.int_le (integer.int_neg (integer.int_of_num n))
(integer.int_of_num m) ⇔ ⊤) ∧
(integer.int_le (integer.int_neg (integer.int_of_num n))
(integer.int_neg (integer.int_of_num m)) ⇔ m ≤ n)
⊦ ∀b n m.
numeral.iSUB b 0 x = 0 ∧ numeral.iSUB ⊤ n 0 = n ∧
numeral.iSUB ⊥ (bit1 n) 0 = numeral.iDUB n ∧
numeral.iSUB ⊤ (bit1 n) (bit1 m) = numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (bit1 n) (bit1 m) = bit1 (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊤ (bit1 n) (arithmetic.BIT2 m) =
bit1 (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊥ (bit1 n) (arithmetic.BIT2 m) =
numeral.iDUB (numeral.iSUB ⊥ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) 0 = bit1 n ∧
numeral.iSUB ⊤ (arithmetic.BIT2 n) (bit1 m) =
bit1 (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) (bit1 m) =
numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊤ (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
numeral.iDUB (numeral.iSUB ⊤ n m) ∧
numeral.iSUB ⊥ (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
bit1 (numeral.iSUB ⊥ n m)
⊦ ∀n m.
(integer.int_of_num 0 = integer.int_of_num 0 ⇔ ⊤) ∧
(integer.int_of_num 0 = integer.int_of_num (bit1 n) ⇔ ⊥) ∧
(integer.int_of_num 0 = integer.int_of_num (arithmetic.BIT2 n) ⇔ ⊥) ∧
(integer.int_of_num 0 = integer.int_neg (integer.int_of_num (bit1 n)) ⇔
⊥) ∧
(integer.int_of_num 0 =
integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)) ⇔ ⊥) ∧
(integer.int_of_num (bit1 n) = integer.int_of_num 0 ⇔ ⊥) ∧
(integer.int_of_num (arithmetic.BIT2 n) = integer.int_of_num 0 ⇔ ⊥) ∧
(integer.int_neg (integer.int_of_num (bit1 n)) = integer.int_of_num 0 ⇔
⊥) ∧
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)) =
integer.int_of_num 0 ⇔ ⊥) ∧
(integer.int_of_num n = integer.int_of_num m ⇔ n = m) ∧
(integer.int_of_num (bit1 n) = integer.int_neg (integer.int_of_num m) ⇔
⊥) ∧
(integer.int_of_num (arithmetic.BIT2 n) =
integer.int_neg (integer.int_of_num m) ⇔ ⊥) ∧
(integer.int_neg (integer.int_of_num (bit1 n)) = integer.int_of_num m ⇔
⊥) ∧
(integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)) =
integer.int_of_num m ⇔ ⊥) ∧
(integer.int_neg (integer.int_of_num n) =
integer.int_neg (integer.int_of_num m) ⇔ n = m)
⊦ ∀n m.
numeral.iZ (0 + n) = n ∧ numeral.iZ (n + 0) = n ∧
numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m)) ∧
numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m)) ∧
numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m)) ∧
numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
arithmetic.BIT2 (suc (n + m)) ∧ suc (0 + n) = suc n ∧
suc (n + 0) = suc n ∧ suc (bit1 n + bit1 m) = bit1 (suc (n + m)) ∧
suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m)) ∧
suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m)) ∧
suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (0 + n) = numeral.iiSUC n ∧
numeral.iiSUC (n + 0) = numeral.iiSUC n ∧
numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m)) ∧
numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
bit1 (numeral.iiSUC (n + m)) ∧
numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
arithmetic.BIT2 (numeral.iiSUC (n + m))
⊦ (∀n. 0 + n = n) ∧ (∀n. n + 0 = n) ∧ (∀n m. n + m = numeral.iZ (n + m)) ∧
(∀n. 0 * n = 0) ∧ (∀n. n * 0 = 0) ∧ (∀n m. n * m = n * m) ∧
(∀n. arithmetic.- 0 n = 0) ∧ (∀n. arithmetic.- n 0 = n) ∧
(∀n m. arithmetic.- n m = arithmetic.- n m) ∧ (∀n. 0 ↑ bit1 n = 0) ∧
(∀n. 0 ↑ arithmetic.BIT2 n = 0) ∧ (∀n. n ↑ 0 = 1) ∧
(∀n m. n ↑ m = n ↑ m) ∧ suc 0 = 1 ∧ (∀n. suc n = suc n) ∧
prim_rec.PRE 0 = 0 ∧ (∀n. prim_rec.PRE n = prim_rec.PRE n) ∧
(∀n. n = 0 ⇔ n = 0) ∧ (∀n. 0 = n ⇔ n = 0) ∧ (∀n m. n = m ⇔ n = m) ∧
(∀n. n < 0 ⇔ ⊥) ∧ (∀n. 0 < n ⇔ 0 < n) ∧ (∀n m. n < m ⇔ n < m) ∧
(∀n. 0 > n ⇔ ⊥) ∧ (∀n. n > 0 ⇔ 0 < n) ∧ (∀n m. n > m ⇔ m < n) ∧
(∀n. 0 ≤ n ⇔ ⊤) ∧ (∀n. n ≤ 0 ⇔ n ≤ 0) ∧ (∀n m. n ≤ m ⇔ n ≤ m) ∧
(∀n. n ≥ 0 ⇔ ⊤) ∧ (∀n. 0 ≥ n ⇔ n = 0) ∧ (∀n m. n ≥ m ⇔ m ≤ n) ∧
(∀n. odd n ⇔ odd n) ∧ (∀n. even n ⇔ even n) ∧ ¬odd 0 ∧ even 0