Theory "real"

Parents realax

Signature

Constant	Type
sup	:(real -> bool) -> real
sumc	:num -> num -> (num -> real) -> real
sum	:num # num -> (num -> real) -> real
real_sub	:real -> real -> real
real_of_num	:num -> real
real_lte	:real -> real -> bool
real_gt	:real -> real -> bool
real_ge	:real -> real -> bool
pow	:real -> num -> real
pos	:real -> real
min	:real -> real -> real
max	:real -> real -> real
inf	:(real -> bool) -> real
abs	:real -> real
NUM_FLOOR	:real -> num
NUM_CEILING	:real -> num
/	:real -> real -> real

Definitions

real_of_num

|- (0 = real_0) /\ !n. & (SUC n) = & n + real_1

real_sub

|- !x y. x - y = x + ~y

real_lte

|- !x y. x <= y = ~(y < x)

real_gt

|- !x y. x > y = y < x

real_ge

|- !x y. x >= y = y <= x

real_div

|- !x y. x / y = x * inv y

abs

|- !x. abs x = (if 0 <= x then x else ~x)

pow

|- (!x. x pow 0 = 1) /\ !x n. x pow SUC n = x * x pow n

sup

|- !P. sup P = @s. !y. (?x. P x /\ y < x) = y < s

sumc

|- (!n f. sumc n 0 f = 0) /\ !n m f. sumc n (SUC m) f = sumc n m f + f (n + m)

SUM_DEF

|- !m n f. sum (m,n) f = sumc m n f

pos_def

|- !x. pos x = (if 0 <= x then x else 0)

min_def

|- !x y. min x y = (if x <= y then x else y)

max_def

|- !x y. max x y = (if x <= y then y else x)

inf_def

|- !p. inf p = ~sup (\r. p ~r)

NUM_FLOOR_def

|- !x. flr x = LEAST n. & (n + 1) > x

NUM_CEILING_def

|- !x. clg x = LEAST n. x <= & n

Theorems

REAL_0

|- real_0 = 0

REAL_1

|- real_1 = 1

REAL_10

|- ~(1 = 0)

REAL_ADD_SYM

|- !x y. x + y = y + x

REAL_ADD_COMM

|- !x y. x + y = y + x

REAL_ADD_ASSOC

|- !x y z. x + (y + z) = x + y + z

REAL_ADD_LID

|- !x. 0 + x = x

REAL_ADD_LINV

|- !x. ~x + x = 0

REAL_LDISTRIB

|- !x y z. x * (y + z) = x * y + x * z

REAL_LT_TOTAL

|- !x y. (x = y) \/ x < y \/ y < x

REAL_LT_REFL

|- !x. ~(x < x)

REAL_LT_TRANS

|- !x y z. x < y /\ y < z ==> x < z

REAL_LT_IADD

|- !x y z. y < z ==> x + y < x + z

REAL_SUP_ALLPOS

|- !P.
     (!x. P x ==> 0 < x) /\ (?x. P x) /\ (?z. !x. P x ==> x < z) ==>
     ?s. !y. (?x. P x /\ y < x) = y < s

REAL_MUL_SYM

|- !x y. x * y = y * x

REAL_MUL_COMM

|- !x y. x * y = y * x

REAL_MUL_ASSOC

|- !x y z. x * (y * z) = x * y * z

REAL_MUL_LID

|- !x. 1 * x = x

REAL_MUL_LINV

|- !x. ~(x = 0) ==> (inv x * x = 1)

REAL_LT_MUL

|- !x y. 0 < x /\ 0 < y ==> 0 < x * y

REAL_INV_0

|- inv 0 = 0

REAL_ADD_RID

|- !x. x + 0 = x

REAL_ADD_RINV

|- !x. x + ~x = 0

REAL_MUL_RID

|- !x. x * 1 = x

REAL_MUL_RINV

|- !x. ~(x = 0) ==> (x * inv x = 1)

REAL_RDISTRIB

|- !x y z. (x + y) * z = x * z + y * z

REAL_EQ_LADD

|- !x y z. (x + y = x + z) = (y = z)

REAL_EQ_RADD

|- !x y z. (x + z = y + z) = (x = y)

REAL_ADD_LID_UNIQ

|- !x y. (x + y = y) = (x = 0)

REAL_ADD_RID_UNIQ

|- !x y. (x + y = x) = (y = 0)

REAL_LNEG_UNIQ

|- !x y. (x + y = 0) = (x = ~y)

REAL_RNEG_UNIQ

|- !x y. (x + y = 0) = (y = ~x)

REAL_NEG_ADD

|- !x y. ~(x + y) = ~x + ~y

REAL_MUL_LZERO

|- !x. 0 * x = 0

REAL_MUL_RZERO

|- !x. x * 0 = 0

REAL_NEG_LMUL

|- !x y. ~(x * y) = ~x * y

REAL_NEG_RMUL

|- !x y. ~(x * y) = x * ~y

REAL_NEGNEG

|- !x. ~ ~x = x

REAL_NEG_MUL2

|- !x y. ~x * ~y = x * y

REAL_ENTIRE

|- !x y. (x * y = 0) = (x = 0) \/ (y = 0)

REAL_LT_LADD

|- !x y z. x + y < x + z = y < z

REAL_LT_RADD

|- !x y z. x + z < y + z = x < y

REAL_NOT_LT

|- !x y. ~(x < y) = y <= x

REAL_LT_ANTISYM

|- !x y. ~(x < y /\ y < x)

REAL_LT_GT

|- !x y. x < y ==> ~(y < x)

REAL_NOT_LE

|- !x y. ~(x <= y) = y < x

REAL_LE_TOTAL

|- !x y. x <= y \/ y <= x

REAL_LET_TOTAL

|- !x y. x <= y \/ y < x

REAL_LTE_TOTAL

|- !x y. x < y \/ y <= x

REAL_LE_REFL

|- !x. x <= x

REAL_LE_LT

|- !x y. x <= y = x < y \/ (x = y)

REAL_LT_LE

|- !x y. x < y = x <= y /\ ~(x = y)

REAL_LT_IMP_LE

|- !x y. x < y ==> x <= y

REAL_LTE_TRANS

|- !x y z. x < y /\ y <= z ==> x < z

REAL_LET_TRANS

|- !x y z. x <= y /\ y < z ==> x < z

REAL_LE_TRANS

|- !x y z. x <= y /\ y <= z ==> x <= z

REAL_LE_ANTISYM

|- !x y. x <= y /\ y <= x = (x = y)

REAL_LET_ANTISYM

|- !x y. ~(x < y /\ y <= x)

REAL_LTE_ANTSYM

|- !x y. ~(x <= y /\ y < x)

REAL_NEG_LT0

|- !x. ~x < 0 = 0 < x

REAL_NEG_GT0

|- !x. 0 < ~x = x < 0

REAL_NEG_LE0

|- !x. ~x <= 0 = 0 <= x

REAL_NEG_GE0

|- !x. 0 <= ~x = x <= 0

REAL_LT_NEGTOTAL

|- !x. (x = 0) \/ 0 < x \/ 0 < ~x

REAL_LE_NEGTOTAL

|- !x. 0 <= x \/ 0 <= ~x

REAL_LE_MUL

|- !x y. 0 <= x /\ 0 <= y ==> 0 <= x * y

REAL_LE_SQUARE

|- !x. 0 <= x * x

REAL_LE_01

|- 0 <= 1

REAL_LT_01

|- 0 < 1

REAL_LE_LADD

|- !x y z. x + y <= x + z = y <= z

REAL_LE_RADD

|- !x y z. x + z <= y + z = x <= y

REAL_LT_ADD2

|- !w x y z. w < x /\ y < z ==> w + y < x + z

REAL_LE_ADD2

|- !w x y z. w <= x /\ y <= z ==> w + y <= x + z

REAL_LE_ADD

|- !x y. 0 <= x /\ 0 <= y ==> 0 <= x + y

REAL_LT_ADD

|- !x y. 0 < x /\ 0 < y ==> 0 < x + y

REAL_LT_ADDNEG

|- !x y z. y < x + ~z = y + z < x

REAL_LT_ADDNEG2

|- !x y z. x + ~y < z = x < z + y

REAL_LT_ADD1

|- !x y. x <= y ==> x < y + 1

REAL_SUB_ADD

|- !x y. x - y + y = x

REAL_SUB_ADD2

|- !x y. y + (x - y) = x

REAL_SUB_REFL

|- !x. x - x = 0

REAL_SUB_0

|- !x y. (x - y = 0) = (x = y)

REAL_LE_DOUBLE

|- !x. 0 <= x + x = 0 <= x

REAL_LE_NEGL

|- !x. ~x <= x = 0 <= x

REAL_LE_NEGR

|- !x. x <= ~x = x <= 0

REAL_NEG_EQ0

|- !x. (~x = 0) = (x = 0)

REAL_NEG_0

|- ~0 = 0

REAL_NEG_SUB

|- !x y. ~(x - y) = y - x

REAL_SUB_LT

|- !x y. 0 < x - y = y < x

REAL_SUB_LE

|- !x y. 0 <= x - y = y <= x

REAL_ADD_SUB

|- !x y. x + y - x = y

REAL_EQ_LMUL

|- !x y z. (x * y = x * z) = (x = 0) \/ (y = z)

REAL_EQ_RMUL

|- !x y z. (x * z = y * z) = (z = 0) \/ (x = y)

REAL_SUB_LDISTRIB

|- !x y z. x * (y - z) = x * y - x * z

REAL_SUB_RDISTRIB

|- !x y z. (x - y) * z = x * z - y * z

REAL_NEG_EQ

|- !x y. (~x = y) = (x = ~y)

REAL_NEG_MINUS1

|- !x. ~x = ~1 * x

REAL_INV_NZ

|- !x. ~(x = 0) ==> ~(inv x = 0)

REAL_INVINV

|- !x. ~(x = 0) ==> (inv (inv x) = x)

REAL_LT_IMP_NE

|- !x y. x < y ==> ~(x = y)

REAL_INV_POS

|- !x. 0 < x ==> 0 < inv x

REAL_LT_LMUL_0

|- !x y. 0 < x ==> (0 < x * y = 0 < y)

REAL_LT_RMUL_0

|- !x y. 0 < y ==> (0 < x * y = 0 < x)

REAL_LT_LMUL

|- !x y z. 0 < x ==> (x * y < x * z = y < z)

REAL_LT_RMUL

|- !x y z. 0 < z ==> (x * z < y * z = x < y)

REAL_LT_RMUL_IMP

|- !x y z. x < y /\ 0 < z ==> x * z < y * z

REAL_LT_LMUL_IMP

|- !x y z. y < z /\ 0 < x ==> x * y < x * z

REAL_LINV_UNIQ

|- !x y. (x * y = 1) ==> (x = inv y)

REAL_RINV_UNIQ

|- !x y. (x * y = 1) ==> (y = inv x)

REAL_INV_INV

|- !x. inv (inv x) = x

REAL_INV_EQ_0

|- !x. (inv x = 0) = (x = 0)

REAL_NEG_INV

|- !x. ~(x = 0) ==> (~inv x = inv ~x)

REAL_INV_1OVER

|- !x. inv x = 1 / x

REAL_LT_INV_EQ

|- !x. 0 < inv x = 0 < x

REAL_LE_INV_EQ

|- !x. 0 <= inv x = 0 <= x

REAL_LE_INV

|- !x. 0 <= x ==> 0 <= inv x

REAL_LE_ADDR

|- !x y. x <= x + y = 0 <= y

REAL_LE_ADDL

|- !x y. y <= x + y = 0 <= x

REAL_LT_ADDR

|- !x y. x < x + y = 0 < y

REAL_LT_ADDL

|- !x y. y < x + y = 0 < x

REAL

|- !n. & (SUC n) = & n + 1

REAL_POS

|- !n. 0 <= & n

REAL_LE

|- !m n. & m <= & n = m <= n

REAL_LT

|- !m n. & m < & n = m < n

REAL_INJ

|- !m n. (& m = & n) = (m = n)

REAL_ADD

|- !m n. & m + & n = & (m + n)

REAL_MUL

|- !m n. & m * & n = & (m * n)

REAL_INV1

|- inv 1 = 1

REAL_OVER1

|- !x. x / 1 = x

REAL_DIV_REFL

|- !x. ~(x = 0) ==> (x / x = 1)

REAL_DIV_LZERO

|- !x. 0 / x = 0

REAL_LT_NZ

|- !n. ~(& n = 0) = 0 < & n

REAL_NZ_IMP_LT

|- !n. ~(n = 0) ==> 0 < & n

REAL_LT_RDIV_0

|- !y z. 0 < z ==> (0 < y / z = 0 < y)

REAL_LT_RDIV

|- !x y z. 0 < z ==> (x / z < y / z = x < y)

REAL_LT_FRACTION_0

|- !n d. ~(n = 0) ==> (0 < d / & n = 0 < d)

REAL_LT_MULTIPLE

|- !n d. 1 < n ==> (d < & n * d = 0 < d)

REAL_LT_FRACTION

|- !n d. 1 < n ==> (d / & n < d = 0 < d)

REAL_LT_HALF1

|- !d. 0 < d / 2 = 0 < d

REAL_LT_HALF2

|- !d. d / 2 < d = 0 < d

REAL_DOUBLE

|- !x. x + x = 2 * x

REAL_DIV_LMUL

|- !x y. ~(y = 0) ==> (y * (x / y) = x)

REAL_DIV_RMUL

|- !x y. ~(y = 0) ==> (x / y * y = x)

REAL_HALF_DOUBLE

|- !x. x / 2 + x / 2 = x

REAL_DOWN

|- !x. 0 < x ==> ?y. 0 < y /\ y < x

REAL_DOWN2

|- !x y. 0 < x /\ 0 < y ==> ?z. 0 < z /\ z < x /\ z < y

REAL_SUB_SUB

|- !x y. x - y - x = ~y

REAL_LT_ADD_SUB

|- !x y z. x + y < z = x < z - y

REAL_LT_SUB_RADD

|- !x y z. x - y < z = x < z + y

REAL_LT_SUB_LADD

|- !x y z. x < y - z = x + z < y

REAL_LE_SUB_LADD

|- !x y z. x <= y - z = x + z <= y

REAL_LE_SUB_RADD

|- !x y z. x - y <= z = x <= z + y

REAL_LT_NEG

|- !x y. ~x < ~y = y < x

REAL_LE_NEG

|- !x y. ~x <= ~y = y <= x

REAL_ADD2_SUB2

|- !a b c d. a + b - (c + d) = a - c + (b - d)

REAL_SUB_LZERO

|- !x. 0 - x = ~x

REAL_SUB_RZERO

|- !x. x - 0 = x

REAL_LET_ADD2

|- !w x y z. w <= x /\ y < z ==> w + y < x + z

REAL_LTE_ADD2

|- !w x y z. w < x /\ y <= z ==> w + y < x + z

REAL_LET_ADD

|- !x y. 0 <= x /\ 0 < y ==> 0 < x + y

REAL_LTE_ADD

|- !x y. 0 < x /\ 0 <= y ==> 0 < x + y

REAL_LT_MUL2

|- !x1 x2 y1 y2.
     0 <= x1 /\ 0 <= y1 /\ x1 < x2 /\ y1 < y2 ==> x1 * y1 < x2 * y2

REAL_LT_INV

|- !x y. 0 < x /\ x < y ==> inv y < inv x

REAL_SUB_LNEG

|- !x y. ~x - y = ~(x + y)

REAL_SUB_RNEG

|- !x y. x - ~y = x + y

REAL_SUB_NEG2

|- !x y. ~x - ~y = y - x

REAL_SUB_TRIANGLE

|- !a b c. a - b + (b - c) = a - c

REAL_EQ_SUB_LADD

|- !x y z. (x = y - z) = (x + z = y)

REAL_EQ_SUB_RADD

|- !x y z. (x - y = z) = (x = z + y)

REAL_INV_MUL

|- !x y. ~(x = 0) /\ ~(y = 0) ==> (inv (x * y) = inv x * inv y)

REAL_LE_LMUL

|- !x y z. 0 < x ==> (x * y <= x * z = y <= z)

REAL_LE_RMUL

|- !x y z. 0 < z ==> (x * z <= y * z = x <= y)

REAL_SUB_INV2

|- !x y. ~(x = 0) /\ ~(y = 0) ==> (inv x - inv y = (y - x) / (x * y))

REAL_SUB_SUB2

|- !x y. x - (x - y) = y

REAL_ADD_SUB2

|- !x y. x - (x + y) = ~y

REAL_MEAN

|- !x y. x < y ==> ?z. x < z /\ z < y

REAL_EQ_LMUL2

|- !x y z. ~(x = 0) ==> ((y = z) = (x * y = x * z))

REAL_LE_MUL2

|- !x1 x2 y1 y2.
     0 <= x1 /\ 0 <= y1 /\ x1 <= x2 /\ y1 <= y2 ==> x1 * y1 <= x2 * y2

REAL_LE_LDIV

|- !x y z. 0 < x /\ y <= z * x ==> y / x <= z

REAL_LE_RDIV

|- !x y z. 0 < x /\ y * x <= z ==> y <= z / x

REAL_LT_DIV

|- !x y. 0 < x /\ 0 < y ==> 0 < x / y

REAL_LE_DIV

|- !x y. 0 <= x /\ 0 <= y ==> 0 <= x / y

REAL_LT_1

|- !x y. 0 <= x /\ x < y ==> x / y < 1

REAL_LE_LMUL_IMP

|- !x y z. 0 <= x /\ y <= z ==> x * y <= x * z

REAL_LE_RMUL_IMP

|- !x y z. 0 <= x /\ y <= z ==> y * x <= z * x

REAL_EQ_IMP_LE

|- !x y. (x = y) ==> x <= y

REAL_INV_LT1

|- !x. 0 < x /\ x < 1 ==> 1 < inv x

REAL_POS_NZ

|- !x. 0 < x ==> ~(x = 0)

REAL_EQ_RMUL_IMP

|- !x y z. ~(z = 0) /\ (x * z = y * z) ==> (x = y)

REAL_EQ_LMUL_IMP

|- !x y z. ~(x = 0) /\ (x * y = x * z) ==> (y = z)

REAL_FACT_NZ

|- !n. ~(& (FACT n) = 0)

REAL_DIFFSQ

|- !x y. (x + y) * (x - y) = x * x - y * y

REAL_POASQ

|- !x. 0 < x * x = ~(x = 0)

REAL_SUMSQ

|- !x y. (x * x + y * y = 0) = (x = 0) /\ (y = 0)

REAL_EQ_NEG

|- !x y. (~x = ~y) = (x = y)

REAL_DIV_MUL2

|- !x z. ~(x = 0) /\ ~(z = 0) ==> !y. y / z = x * y / (x * z)

REAL_MIDDLE1

|- !a b. a <= b ==> a <= (a + b) / 2

REAL_MIDDLE2

|- !a b. a <= b ==> (a + b) / 2 <= b

ABS_ZERO

|- !x. (abs x = 0) = (x = 0)

ABS_0

|- abs 0 = 0

ABS_1

|- abs 1 = 1

ABS_NEG

|- !x. abs ~x = abs x

ABS_TRIANGLE

|- !x y. abs (x + y) <= abs x + abs y

ABS_POS

|- !x. 0 <= abs x

ABS_MUL

|- !x y. abs (x * y) = abs x * abs y

ABS_LT_MUL2

|- !w x y z. abs w < y /\ abs x < z ==> abs (w * x) < y * z

ABS_SUB

|- !x y. abs (x - y) = abs (y - x)

ABS_NZ

|- !x. ~(x = 0) = 0 < abs x

ABS_INV

|- !x. ~(x = 0) ==> (abs (inv x) = inv (abs x))

ABS_ABS

|- !x. abs (abs x) = abs x

ABS_LE

|- !x. x <= abs x

ABS_REFL

|- !x. (abs x = x) = 0 <= x

ABS_N

|- !n. abs (& n) = & n

ABS_BETWEEN

|- !x y d. 0 < d /\ x - d < y /\ y < x + d = abs (y - x) < d

ABS_BOUND

|- !x y d. abs (x - y) < d ==> y < x + d

ABS_STILLNZ

|- !x y. abs (x - y) < abs y ==> ~(x = 0)

ABS_CASES

|- !x. (x = 0) \/ 0 < abs x

ABS_BETWEEN1

|- !x y z. x < z /\ abs (y - x) < z - x ==> y < z

ABS_SIGN

|- !x y. abs (x - y) < y ==> 0 < x

ABS_SIGN2

|- !x y. abs (x - y) < ~y ==> x < 0

ABS_DIV

|- !y. ~(y = 0) ==> !x. abs (x / y) = abs x / abs y

ABS_CIRCLE

|- !x y h. abs h < abs y - abs x ==> abs (x + h) < abs y

REAL_SUB_ABS

|- !x y. abs x - abs y <= abs (x - y)

ABS_SUB_ABS

|- !x y. abs (abs x - abs y) <= abs (x - y)

ABS_BETWEEN2

|- !x0 x y0 y.
     x0 < y0 /\ abs (x - x0) < (y0 - x0) / 2 /\
     abs (y - y0) < (y0 - x0) / 2 ==>
     x < y

ABS_BOUNDS

|- !x k. abs x <= k = ~k <= x /\ x <= k

POW_0

|- !n. 0 pow SUC n = 0

POW_NZ

|- !c n. ~(c = 0) ==> ~(c pow n = 0)

POW_INV

|- !c. ~(c = 0) ==> !n. inv (c pow n) = inv c pow n

POW_ABS

|- !c n. abs c pow n = abs (c pow n)

POW_PLUS1

|- !e. 0 < e ==> !n. 1 + & n * e <= (1 + e) pow n

POW_ADD

|- !c m n. c pow (m + n) = c pow m * c pow n

POW_1

|- !x. x pow 1 = x

POW_2

|- !x. x pow 2 = x * x

POW_ONE

|- !n. 1 pow n = 1

POW_POS

|- !x. 0 <= x ==> !n. 0 <= x pow n

POW_LE

|- !n x y. 0 <= x /\ x <= y ==> x pow n <= y pow n

POW_M1

|- !n. abs (~1 pow n) = 1

POW_MUL

|- !n x y. (x * y) pow n = x pow n * y pow n

REAL_LE_POW2

|- !x. 0 <= x pow 2

ABS_POW2

|- !x. abs (x pow 2) = x pow 2

REAL_POW2_ABS

|- !x. abs x pow 2 = x pow 2

REAL_LE1_POW2

|- !x. 1 <= x ==> 1 <= x pow 2

REAL_LT1_POW2

|- !x. 1 < x ==> 1 < x pow 2

POW_POS_LT

|- !x n. 0 < x ==> 0 < x pow SUC n

POW_2_LE1

|- !n. 1 <= 2 pow n

POW_2_LT

|- !n. & n < 2 pow n

POW_MINUS1

|- !n. ~1 pow (2 * n) = 1

POW_LT

|- !n x y. 0 <= x /\ x < y ==> x pow SUC n < y pow SUC n

REAL_POW_LT

|- !x n. 0 < x ==> 0 < x pow n

POW_EQ

|- !n x y. 0 <= x /\ 0 <= y /\ (x pow SUC n = y pow SUC n) ==> (x = y)

POW_ZERO

|- !n x. (x pow n = 0) ==> (x = 0)

POW_ZERO_EQ

|- !n x. (x pow SUC n = 0) = (x = 0)

REAL_POW_LT2

|- !n x y. ~(n = 0) /\ 0 <= x /\ x < y ==> x pow n < y pow n

REAL_POW_MONO_LT

|- !m n x. 1 < x /\ m < n ==> x pow m < x pow n

REAL_POW_POW

|- !x m n. (x pow m) pow n = x pow (m * n)

REAL_SUP_SOMEPOS

|- !P.
     (?x. P x /\ 0 < x) /\ (?z. !x. P x ==> x < z) ==>
     ?s. !y. (?x. P x /\ y < x) = y < s

SUP_LEMMA1

|- !P s d.
     (!y. (?x. (\x. P (x + d)) x /\ y < x) = y < s) ==>
     !y. (?x. P x /\ y < x) = y < s + d

SUP_LEMMA2

|- !P. (?x. P x) ==> ?d x. (\x. P (x + d)) x /\ 0 < x

SUP_LEMMA3

|- !d. (?z. !x. P x ==> x < z) ==> ?z. !x. (\x. P (x + d)) x ==> x < z

REAL_SUP_EXISTS

|- !P.
     (?x. P x) /\ (?z. !x. P x ==> x < z) ==>
     ?s. !y. (?x. P x /\ y < x) = y < s

REAL_SUP

|- !P.
     (?x. P x) /\ (?z. !x. P x ==> x < z) ==>
     !y. (?x. P x /\ y < x) = y < sup P

REAL_SUP_UBOUND

|- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> !y. P y ==> y <= sup P

SETOK_LE_LT

|- !P.
     (?x. P x) /\ (?z. !x. P x ==> x <= z) =
     (?x. P x) /\ ?z. !x. P x ==> x < z

REAL_SUP_LE

|- !P.
     (?x. P x) /\ (?z. !x. P x ==> x <= z) ==>
     !y. (?x. P x /\ y < x) = y < sup P

REAL_SUP_UBOUND_LE

|- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> !y. P y ==> y <= sup P

REAL_ARCH

|- !x. 0 < x ==> !y. ?n. y < & n * x

REAL_ARCH_LEAST

|- !y. 0 < y ==> !x. 0 <= x ==> ?n. & n * y <= x /\ x < & (SUC n) * y

sum

|- !f n m. (sum (n,0) f = 0) /\ (sum (n,SUC m) f = sum (n,m) f + f (n + m))

SUM_TWO

|- !f n p. sum (0,n) f + sum (n,p) f = sum (0,n + p) f

SUM_DIFF

|- !f m n. sum (m,n) f = sum (0,m + n) f - sum (0,m) f

ABS_SUM

|- !f m n. abs (sum (m,n) f) <= sum (m,n) (\n. abs (f n))

SUM_LE

|- !f g m n.
     (!r. m <= r /\ r < n + m ==> f r <= g r) ==> sum (m,n) f <= sum (m,n) g

SUM_EQ

|- !f g m n.
     (!r. m <= r /\ r < n + m ==> (f r = g r)) ==> (sum (m,n) f = sum (m,n) g)

SUM_POS

|- !f. (!n. 0 <= f n) ==> !m n. 0 <= sum (m,n) f

SUM_POS_GEN

|- !f m. (!n. m <= n ==> 0 <= f n) ==> !n. 0 <= sum (m,n) f

SUM_ABS

|- !f m n. abs (sum (m,n) (\m. abs (f m))) = sum (m,n) (\m. abs (f m))

SUM_ABS_LE

|- !f m n. abs (sum (m,n) f) <= sum (m,n) (\n. abs (f n))

SUM_ZERO

|- !f N. (!n. n >= N ==> (f n = 0)) ==> !m n. m >= N ==> (sum (m,n) f = 0)

SUM_ADD

|- !f g m n. sum (m,n) (\n. f n + g n) = sum (m,n) f + sum (m,n) g

SUM_CMUL

|- !f c m n. sum (m,n) (\n. c * f n) = c * sum (m,n) f

SUM_NEG

|- !f n d. sum (n,d) (\n. ~f n) = ~sum (n,d) f

SUM_SUB

|- !f g m n. sum (m,n) (\n. f n - g n) = sum (m,n) f - sum (m,n) g

SUM_SUBST

|- !f g m n.
     (!p. m <= p /\ p < m + n ==> (f p = g p)) ==> (sum (m,n) f = sum (m,n) g)

SUM_NSUB

|- !n f c. sum (0,n) f - & n * c = sum (0,n) (\p. f p - c)

SUM_BOUND

|- !f k m n. (!p. m <= p /\ p < m + n ==> f p <= k) ==> sum (m,n) f <= & n * k

SUM_GROUP

|- !n k f. sum (0,n) (\m. sum (m * k,k) f) = sum (0,n * k) f

SUM_1

|- !f n. sum (n,1) f = f n

SUM_2

|- !f n. sum (n,2) f = f n + f (n + 1)

SUM_OFFSET

|- !f n k. sum (0,n) (\m. f (m + k)) = sum (0,n + k) f - sum (0,k) f

SUM_REINDEX

|- !f m k n. sum (m + k,n) f = sum (m,n) (\r. f (r + k))

SUM_0

|- !m n. sum (m,n) (\r. 0) = 0

SUM_PERMUTE_0

|- !n p.
     (!y. y < n ==> ?!x. x < n /\ (p x = y)) ==>
     !f. sum (0,n) (\n. f (p n)) = sum (0,n) f

SUM_CANCEL

|- !f n d. sum (n,d) (\n. f (SUC n) - f n) = f (n + d) - f n

REAL_MUL_RNEG

|- !x y. x * ~y = ~(x * y)

REAL_MUL_LNEG

|- !x y. ~x * y = ~(x * y)

real_lt

|- !y x. x < y = ~(y <= x)

REAL_LE_LADD_IMP

|- !x y z. y <= z ==> x + y <= x + z

REAL_LE_LNEG

|- !x y. ~x <= y = 0 <= x + y

REAL_LE_NEG2

|- !x y. ~x <= ~y = y <= x

REAL_NEG_NEG

|- !x. ~ ~x = x

REAL_LE_RNEG

|- !x y. x <= ~y = x + y <= 0

REAL_POW_INV

|- !x n. inv x pow n = inv (x pow n)

REAL_POW_DIV

|- !x y n. (x / y) pow n = x pow n / y pow n

REAL_POW_ADD

|- !x m n. x pow (m + n) = x pow m * x pow n

REAL_LE_RDIV_EQ

|- !x y z. 0 < z ==> (x <= y / z = x * z <= y)

REAL_LE_LDIV_EQ

|- !x y z. 0 < z ==> (x / z <= y = x <= y * z)

REAL_LT_RDIV_EQ

|- !x y z. 0 < z ==> (x < y / z = x * z < y)

REAL_LT_LDIV_EQ

|- !x y z. 0 < z ==> (x / z < y = x < y * z)

REAL_EQ_RDIV_EQ

|- !x y z. 0 < z ==> ((x = y / z) = (x * z = y))

REAL_EQ_LDIV_EQ

|- !x y z. 0 < z ==> ((x / z = y) = (x = y * z))

REAL_OF_NUM_POW

|- !x n. & x pow n = & (x ** n)

REAL_ADD_LDISTRIB

|- !x y z. x * (y + z) = x * y + x * z

REAL_ADD_RDISTRIB

|- !x y z. (x + y) * z = x * z + y * z

REAL_OF_NUM_ADD

|- !m n. & m + & n = & (m + n)

REAL_OF_NUM_LE

|- !m n. & m <= & n = m <= n

REAL_OF_NUM_MUL

|- !m n. & m * & n = & (m * n)

REAL_OF_NUM_SUC

|- !n. & n + 1 = & (SUC n)

REAL_OF_NUM_EQ

|- !m n. (& m = & n) = (m = n)

REAL_EQ_MUL_LCANCEL

|- !x y z. (x * y = x * z) = (x = 0) \/ (y = z)

REAL_ABS_0

|- abs 0 = 0

REAL_ABS_TRIANGLE

|- !x y. abs (x + y) <= abs x + abs y

REAL_ABS_MUL

|- !x y. abs (x * y) = abs x * abs y

REAL_ABS_POS

|- !x. 0 <= abs x

REAL_LE_EPSILON

|- !x y. (!e. 0 < e ==> x <= y + e) ==> x <= y

REAL_BIGNUM

|- !r. ?n. r < & n

REAL_INV_LT_ANTIMONO

|- !x y. 0 < x /\ 0 < y ==> (inv x < inv y = y < x)

REAL_INV_INJ

|- !x y. (inv x = inv y) = (x = y)

REAL_DIV_RMUL_CANCEL

|- !c a b. ~(c = 0) ==> (a * c / (b * c) = a / b)

REAL_DIV_LMUL_CANCEL

|- !c a b. ~(c = 0) ==> (c * a / (c * b) = a / b)

REAL_DIV_ADD

|- !x y z. y / x + z / x = (y + z) / x

REAL_ADD_RAT

|- !a b c d.
     ~(b = 0) /\ ~(d = 0) ==> (a / b + c / d = (a * d + b * c) / (b * d))

REAL_SUB_RAT

|- !a b c d.
     ~(b = 0) /\ ~(d = 0) ==> (a / b - c / d = (a * d - b * c) / (b * d))

REAL_SUB

|- !m n. & m - & n = (if m - n = 0 then ~ & (n - m) else & (m - n))

REAL_POS_POS

|- !x. 0 <= pos x

REAL_POS_ID

|- !x. 0 <= x ==> (pos x = x)

REAL_POS_INFLATE

|- !x. x <= pos x

REAL_POS_MONO

|- !x y. x <= y ==> pos x <= pos y

REAL_POS_EQ_ZERO

|- !x. (pos x = 0) = x <= 0

REAL_POS_LE_ZERO

|- !x. pos x <= 0 = x <= 0

REAL_MIN_REFL

|- !x. min x x = x

REAL_LE_MIN

|- !z x y. z <= min x y = z <= x /\ z <= y

REAL_MIN_LE

|- !z x y. min x y <= z = x <= z \/ y <= z

REAL_MIN_LE1

|- !x y. min x y <= x

REAL_MIN_LE2

|- !x y. min x y <= y

REAL_MIN_ALT

|- !x y. (x <= y ==> (min x y = x)) /\ (y <= x ==> (min x y = y))

REAL_MIN_LE_LIN

|- !z x y. 0 <= z /\ z <= 1 ==> min x y <= z * x + (1 - z) * y

REAL_MIN_ADD

|- !z x y. min (x + z) (y + z) = min x y + z

REAL_MIN_SUB

|- !z x y. min (x - z) (y - z) = min x y - z

REAL_IMP_MIN_LE2

|- !x1 x2 y1 y2. x1 <= y1 /\ x2 <= y2 ==> min x1 x2 <= min y1 y2

REAL_MAX_REFL

|- !x. max x x = x

REAL_LE_MAX

|- !z x y. z <= max x y = z <= x \/ z <= y

REAL_LE_MAX1

|- !x y. x <= max x y

REAL_LE_MAX2

|- !x y. y <= max x y

REAL_MAX_LE

|- !z x y. max x y <= z = x <= z /\ y <= z

REAL_MAX_ALT

|- !x y. (x <= y ==> (max x y = y)) /\ (y <= x ==> (max x y = x))

REAL_MAX_MIN

|- !x y. max x y = ~min (~x) ~y

REAL_MIN_MAX

|- !x y. min x y = ~max (~x) ~y

REAL_LIN_LE_MAX

|- !z x y. 0 <= z /\ z <= 1 ==> z * x + (1 - z) * y <= max x y

REAL_MAX_ADD

|- !z x y. max (x + z) (y + z) = max x y + z

REAL_MAX_SUB

|- !z x y. max (x - z) (y - z) = max x y - z

REAL_IMP_MAX_LE2

|- !x1 x2 y1 y2. x1 <= y1 /\ x2 <= y2 ==> max x1 x2 <= max y1 y2

REAL_SUP_EXISTS_UNIQUE

|- !p.
     (?x. p x) /\ (?z. !x. p x ==> x <= z) ==>
     ?!s. !y. (?x. p x /\ y < x) = y < s

REAL_SUP_MAX

|- !p z. p z /\ (!x. p x ==> x <= z) ==> (sup p = z)

REAL_IMP_SUP_LE

|- !p x. (?r. p r) /\ (!r. p r ==> r <= x) ==> sup p <= x

REAL_IMP_LE_SUP

|- !p x.
     (?r. p r) /\ (?z. !r. p r ==> r <= z) /\ (?r. p r /\ x <= r) ==>
     x <= sup p

REAL_INF_MIN

|- !p z. p z /\ (!x. p x ==> z <= x) ==> (inf p = z)

REAL_IMP_LE_INF

|- !p r. (?x. p x) /\ (!x. p x ==> r <= x) ==> r <= inf p

REAL_IMP_INF_LE

|- !p r. (?z. !x. p x ==> z <= x) /\ (?x. p x /\ x <= r) ==> inf p <= r

REAL_INF_LT

|- !p z. (?x. p x) /\ inf p < z ==> ?x. p x /\ x < z

REAL_INF_CLOSE

|- !p e. (?x. p x) /\ 0 < e ==> ?x. p x /\ x < inf p + e

SUP_EPSILON

|- !p e.
     0 < e /\ (?x. p x) /\ (?z. !x. p x ==> x <= z) ==>
     ?x. p x /\ sup p <= x + e

REAL_LE_SUP

|- !p x.
     (?y. p y) /\ (?y. !z. p z ==> z <= y) ==>
     (x <= sup p = !y. (!z. p z ==> z <= y) ==> x <= y)

REAL_INF_LE

|- !p x.
     (?y. p y) /\ (?y. !z. p z ==> y <= z) ==>
     (inf p <= x = !y. (!z. p z ==> y <= z) ==> y <= x)

REAL_SUP_CONST

|- !x. sup (\r. r = x) = x

REAL_MUL_SUB2_CANCEL

|- !z x y. x * y + (z - x) * y = z * y

REAL_MUL_SUB1_CANCEL

|- !z x y. y * x + y * (z - x) = y * z

REAL_NEG_HALF

|- !x. x - x / 2 = x / 2

REAL_NEG_THIRD

|- !x. x - x / 3 = 2 * x / 3

REAL_DIV_DENOM_CANCEL

|- !x y z. ~(x = 0) ==> (y / x / (z / x) = y / z)

REAL_DIV_DENOM_CANCEL2

|- !y z. y / 2 / (z / 2) = y / z

REAL_DIV_DENOM_CANCEL3

|- !y z. y / 3 / (z / 3) = y / z

REAL_DIV_INNER_CANCEL

|- !x y z. ~(x = 0) ==> (y / x * (x / z) = y / z)

REAL_DIV_INNER_CANCEL2

|- !y z. y / 2 * (2 / z) = y / z

REAL_DIV_INNER_CANCEL3

|- !y z. y / 3 * (3 / z) = y / z

REAL_DIV_OUTER_CANCEL

|- !x y z. ~(x = 0) ==> (x / y * (z / x) = z / y)

REAL_DIV_OUTER_CANCEL2

|- !y z. 2 / y * (z / 2) = z / y

REAL_DIV_OUTER_CANCEL3

|- !y z. 3 / y * (z / 3) = z / y

REAL_DIV_REFL2

|- 2 / 2 = 1

REAL_DIV_REFL3

|- 3 / 3 = 1

REAL_HALF_BETWEEN

|- (0 < 1 / 2 /\ 1 / 2 < 1) /\ 0 <= 1 / 2 /\ 1 / 2 <= 1

REAL_THIRDS_BETWEEN

|- (0 < 1 / 3 /\ 1 / 3 < 1 /\ 0 < 2 / 3 /\ 2 / 3 < 1) /\ 0 <= 1 / 3 /\
   1 / 3 <= 1 /\ 0 <= 2 / 3 /\ 2 / 3 <= 1

REAL_LE_SUB_CANCEL2

|- !x y z. x - z <= y - z = x <= y

REAL_ADD_SUB_ALT

|- !x y. x + y - y = x

add_rat

|- x / y + u / v =
   (if y = 0 then
      unint (x / y) + u / v
    else
      (if v = 0 then
         x / y + unint (u / v)
       else
         (if y = v then (x + u) / v else (x * v + u * y) / (y * v))))

add_ratl

|- x / y + z = (if y = 0 then unint (x / y) + z else (x + z * y) / y)

add_ratr

|- x + y / z = (if z = 0 then x + unint (y / z) else (x * z + y) / z)

add_ints

|- (& n + & m = & (n + m)) /\
   (~ & n + & m = (if n <= m then & (m - n) else ~ & (n - m))) /\
   (& n + ~ & m = (if n < m then ~ & (m - n) else & (n - m))) /\
   (~ & n + ~ & m = ~ & (n + m))

mult_rat

|- x / y * (u / v) =
   (if y = 0 then
      unint (x / y) * (u / v)
    else
      (if v = 0 then x / y * unint (u / v) else x * u / (y * v)))

mult_ratl

|- x / y * z = (if y = 0 then unint (x / y) * z else x * z / y)

mult_ratr

|- x * (y / z) = (if z = 0 then x * unint (y / z) else x * y / z)

mult_ints

|- (& a * & b = & (a * b)) /\ (~ & a * & b = ~ & (a * b)) /\
   (& a * ~ & b = ~ & (a * b)) /\ (~ & a * ~ & b = & (a * b))

pow_rat

|- (x pow 0 = 1) /\ (0 pow NUMERAL (BIT1 n) = 0) /\
   (0 pow NUMERAL (BIT2 n) = 0) /\
   (& (NUMERAL a) pow NUMERAL n = & (NUMERAL a ** NUMERAL n)) /\
   (~ & (NUMERAL a) pow NUMERAL n =
    (if ODD (NUMERAL n) then $~ else (\x. x)) (& (NUMERAL a ** NUMERAL n))) /\
   ((x / y) pow n = x pow n / y pow n)

neg_rat

|- (~(x / y) = (if y = 0 then ~unint (x / y) else ~x / y)) /\
   (x / ~y = (if y = 0 then unint (x / y) else ~x / y))

eq_rat

|- (x / y = u / v) =
   (if y = 0 then
      unint (x / y) = u / v
    else
      (if v = 0 then
         x / y = unint (u / v)
       else
         (if y = v then x = u else x * v = y * u)))

eq_ratl

|- (x / y = z) = (if y = 0 then unint (x / y) = z else x = y * z)

eq_ratr

|- (z = x / y) = (if y = 0 then z = unint (x / y) else y * z = x)

eq_ints

|- ((& n = & m) = (n = m)) /\ ((~ & n = & m) = (n = 0) /\ (m = 0)) /\
   ((& n = ~ & m) = (n = 0) /\ (m = 0)) /\ ((~ & n = ~ & m) = (n = m))

div_ratr

|- x / (y / z) = (if (y = 0) \/ (z = 0) then x / unint (y / z) else x * z / y)

div_ratl

|- x / y / z =
   (if y = 0 then
      unint (x / y) / z
    else
      (if z = 0 then unint (x / y / z) else x / (y * z)))

div_rat

|- x / y / (u / v) =
   (if (u = 0) \/ (v = 0) then
      x / y / unint (u / v)
    else
      (if y = 0 then unint (x / y) / (u / v) else x * v / (y * u)))

le_rat

|- x / & n <= u / & m =
   (if n = 0 then
      unint (x / 0) <= u / & m
    else
      (if m = 0 then x / & n <= unint (u / 0) else & m * x <= & n * u))

le_ratl

|- x / & n <= u = (if n = 0 then unint (x / 0) <= u else x <= & n * u)

le_ratr

|- x <= u / & m = (if m = 0 then x <= unint (u / 0) else & m * x <= u)

le_int

|- (& n <= & m = n <= m) /\ (~ & n <= & m = T) /\
   (& n <= ~ & m = (n = 0) /\ (m = 0)) /\ (~ & n <= ~ & m = m <= n)

lt_rat

|- x / & n < u / & m =
   (if n = 0 then
      unint (x / 0) < u / & m
    else
      (if m = 0 then x / & n < unint (u / 0) else & m * x < & n * u))

lt_ratl

|- x / & n < u = (if n = 0 then unint (x / 0) < u else x < & n * u)

lt_ratr

|- x < u / & m = (if m = 0 then x < unint (u / 0) else & m * x < u)

lt_int

|- (& n < & m = n < m) /\ (~ & n < & m = ~(n = 0) \/ ~(m = 0)) /\
   (& n < ~ & m = F) /\ (~ & n < ~ & m = m < n)

NUM_FLOOR_LE

|- 0 <= x ==> & (flr x) <= x

NUM_FLOOR_LE2

|- 0 <= y ==> (x <= flr y = & x <= y)

NUM_FLOOR_LET

|- flr x <= y = x < & y + 1

NUM_FLOOR_DIV

|- 0 <= x /\ 0 < y ==> & (flr (x / y)) * y <= x

NUM_FLOOR_DIV_LOWERBOUND

|- 0 <= x /\ 0 < y ==> x < & (flr (x / y) + 1) * y

NUM_FLOOR_EQNS

|- (flr (& n) = n) /\ (0 < m ==> (flr (& n / & m) = n DIV m))

NUM_FLOOR_LOWER_BOUND

|- x < & n = flr (x + 1) <= n

NUM_FLOOR_upper_bound

|- & n <= x = n < flr (x + 1)

LE_NUM_CEILING

|- !x. x <= & (clg x)

NUM_CEILING_LE

|- !x n. x <= & n ==> clg x <= n