Package hol-real: HOL real theories

Information

namehol-real
version1.0
descriptionHOL real theories
authorHOL developers <hol-developers@lists.sourceforge.net>
licenseMIT
checksumb8657facefcd305d7a12b54217d75adf953105aa
requiresbase
hol-base
hol-integer
showData.Bool
Data.List
Data.Pair
Function
HOL4
Number.Natural
Number.Real
Relation

Files

Defined Type Operators

Defined Constants

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

%%genvar%%688 y.
    %%genvar%%688 = y %%genvar%%688 < y y < %%genvar%%688

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

External Constants

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