Theory: real

Parents

• realax

Types

Constants

• real_lte  :real -> real -> bool
• /  :real -> real -> real
• abs  :real -> real
• real_sub  :real -> real -> real
• pow  :real -> num -> real
• sum  :num # num -> (num -> real) -> real
• sup  :(real -> bool) -> real
• real_ge  :real -> real -> bool
• real_gt  :real -> real -> bool
• real_of_num  :num -> real
• sumc  :num -> num -> (num -> real) -> real

Definitions

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

real_div

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

real_ge

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

real_gt

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

real_lte

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

real_of_num

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

real_sub

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

SUM_DEF

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

sumc

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

sup

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

Theorems

ABS_0

|- abs 0 = 0

ABS_1

|- abs 1 = 1

ABS_ABS

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

ABS_BETWEEN

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

ABS_BETWEEN1

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

ABS_BETWEEN2

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

ABS_BOUND

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

ABS_BOUNDS

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

ABS_CASES

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

ABS_CIRCLE

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

ABS_DIV

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

ABS_INV

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

ABS_LE

|- !x. x <= abs x

ABS_LT_MUL2

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

ABS_MUL

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

ABS_N

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

ABS_NEG

|- !x. abs ~x = abs x

ABS_NZ

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

ABS_POS

|- !x. 0 <= abs x

ABS_POW2

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

ABS_REFL

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

ABS_SIGN

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

ABS_SIGN2

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

ABS_STILLNZ

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

ABS_SUB

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

ABS_SUB_ABS

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

ABS_SUM

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

ABS_TRIANGLE

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

ABS_ZERO

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

POW_0

|- !n. 0 pow SUC n = 0

POW_1

|- !x. x pow 1 = x

POW_2

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

POW_2_LE1

|- !n. 1 <= 2 pow n

POW_2_LT

|- !n. & n < 2 pow n

POW_ABS

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

POW_ADD

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

POW_EQ

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

POW_INV

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

POW_LE

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

POW_LT

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

POW_M1

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

POW_MINUS1

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

POW_MUL

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

POW_NZ

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

POW_ONE

|- !n. 1 pow n = 1

POW_PLUS1

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

POW_POS

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

POW_POS_LT

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

POW_ZERO

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

POW_ZERO_EQ

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

REAL

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

REAL_0

|- real_0 = 0

REAL_1

|- real_1 = 1

REAL_10

|- ~(1 = 0)

REAL_ABS_0

|- abs 0 = 0

REAL_ABS_MUL

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

REAL_ABS_POS

|- !x. 0 <= abs x

REAL_ABS_TRIANGLE

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

REAL_ADD

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

REAL_ADD2_SUB2

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

REAL_ADD_ASSOC

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

REAL_ADD_LDISTRIB

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

REAL_ADD_LID

|- !x. 0 + x = x

REAL_ADD_LID_UNIQ

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

REAL_ADD_LINV

|- !x. ~x + x = 0

REAL_ADD_RDISTRIB

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

REAL_ADD_RID

|- !x. x + 0 = x

REAL_ADD_RID_UNIQ

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

REAL_ADD_RINV

|- !x. x + ~x = 0

REAL_ADD_SUB

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

REAL_ADD_SUB2

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

REAL_ADD_SYM

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

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

REAL_DIFFSQ

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

REAL_DIV_LMUL

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

REAL_DIV_LZERO

|- !x. 0 / x = 0

REAL_DIV_MUL2

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

REAL_DIV_REFL

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

REAL_DIV_RMUL

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

REAL_DOUBLE

|- !x. x + 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_ENTIRE

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

REAL_EQ_IMP_LE

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

REAL_EQ_LADD

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

REAL_EQ_LMUL

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

REAL_EQ_LMUL2

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

REAL_EQ_LMUL_IMP

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

REAL_EQ_MUL_LCANCEL

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

REAL_EQ_NEG

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

REAL_EQ_RADD

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

REAL_EQ_RMUL

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

REAL_EQ_RMUL_IMP

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

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_FACT_NZ

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

REAL_HALF_DOUBLE

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

REAL_INJ

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

REAL_INV1

|- inv 1 = 1

REAL_INV_0

|- inv 0 = 0

REAL_INV_1OVER

|- !x. inv x = 1 / x

REAL_INV_EQ_0

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

REAL_INV_INV

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

REAL_INV_LT1

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

REAL_INV_MUL

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

REAL_INV_NZ

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

REAL_INV_POS

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

REAL_INVINV

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

REAL_LDISTRIB

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

REAL_LE

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

REAL_LE1_POW2

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

REAL_LE_01

|- 0 <= 1

REAL_LE_ADD

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

REAL_LE_ADD2

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

REAL_LE_ADDL

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

REAL_LE_ADDR

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

REAL_LE_ANTISYM

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

REAL_LE_DIV

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

REAL_LE_DOUBLE

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

REAL_LE_INV

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

REAL_LE_INV_EQ

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

REAL_LE_LADD

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

REAL_LE_LADD_IMP

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

REAL_LE_LDIV

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

REAL_LE_LMUL

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

REAL_LE_LMUL_IMP

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

REAL_LE_LNEG

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

REAL_LE_LT

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

REAL_LE_MUL

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

REAL_LE_MUL2

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

REAL_LE_NEG

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

REAL_LE_NEG2

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

REAL_LE_NEGL

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

REAL_LE_NEGR

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

REAL_LE_NEGTOTAL

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

REAL_LE_POW2

|- !x. 0 <= x pow 2

REAL_LE_RADD

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

REAL_LE_RDIV

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

REAL_LE_REFL

|- !x. x <= x

REAL_LE_RMUL

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

REAL_LE_RMUL_IMP

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

REAL_LE_RNEG

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

REAL_LE_SQUARE

|- !x. 0 <= x * x

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_LE_TOTAL

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

REAL_LE_TRANS

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

REAL_LET_ADD

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

REAL_LET_ADD2

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

REAL_LET_ANTISYM

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

REAL_LET_TOTAL

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

REAL_LET_TRANS

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

REAL_LINV_UNIQ

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

REAL_LNEG_UNIQ

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

real_lt

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

REAL_LT1_POW2

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

REAL_LT_01

|- 0 < 1

REAL_LT_1

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

REAL_LT_ADD

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

REAL_LT_ADD1

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

REAL_LT_ADD2

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

REAL_LT_ADD_SUB

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

REAL_LT_ADDL

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

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_ADDR

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

REAL_LT_ANTISYM

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

REAL_LT_DIV

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

REAL_LT_FRACTION

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

REAL_LT_FRACTION_0

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

REAL_LT_GT

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

REAL_LT_HALF1

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

REAL_LT_HALF2

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

REAL_LT_IADD

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

REAL_LT_IMP_LE

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

REAL_LT_IMP_NE

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

REAL_LT_INV

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

REAL_LT_INV_EQ

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

REAL_LT_LADD

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

REAL_LT_LE

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

REAL_LT_LMUL

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

REAL_LT_LMUL_0

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

REAL_LT_LMUL_IMP

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

REAL_LT_MUL

|- !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_MULTIPLE

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

REAL_LT_NEG

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

REAL_LT_NEGTOTAL

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

REAL_LT_NZ

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

REAL_LT_RADD

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

REAL_LT_RDIV

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

REAL_LT_RDIV_0

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

REAL_LT_REFL

|- !x. ~(x < x)

REAL_LT_RMUL

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

REAL_LT_RMUL_0

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

REAL_LT_RMUL_IMP

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

REAL_LT_SUB_LADD

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

REAL_LT_SUB_RADD

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

REAL_LT_TOTAL

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

REAL_LT_TRANS

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

REAL_LTE_ADD

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

REAL_LTE_ADD2

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

REAL_LTE_ANTSYM

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

REAL_LTE_TOTAL

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

REAL_LTE_TRANS

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

REAL_MEAN

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

REAL_MIDDLE1

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

REAL_MIDDLE2

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

REAL_MUL

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

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_MUL_LNEG

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

REAL_MUL_LZERO

|- !x. 0 * x = 0

REAL_MUL_RID

|- !x. x * 1 = x

REAL_MUL_RINV

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

REAL_MUL_RNEG

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

REAL_MUL_RZERO

|- !x. x * 0 = 0

REAL_MUL_SYM

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

REAL_NEG_0

|- ~0 = 0

REAL_NEG_ADD

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

REAL_NEG_EQ

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

REAL_NEG_EQ0

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

REAL_NEG_GE0

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

REAL_NEG_GT0

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

REAL_NEG_INV

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

REAL_NEG_LE0

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

REAL_NEG_LMUL

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

REAL_NEG_LT0

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

REAL_NEG_MINUS1

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

REAL_NEG_MUL2

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

REAL_NEG_NEG

|- !x. ~~x = x

REAL_NEG_RMUL

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

REAL_NEG_SUB

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

REAL_NEGNEG

|- !x. ~~x = x

REAL_NOT_LE

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

REAL_NOT_LT

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

REAL_NZ_IMP_LT

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

REAL_OF_NUM_ADD

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

REAL_OF_NUM_EQ

|- !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_OVER1

|- !x. x / 1 = x

REAL_POASQ

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

REAL_POS

|- !n. 0 <= & n

REAL_POS_NZ

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

REAL_POW2_ABS

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

REAL_POW_LT

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

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_RDISTRIB

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

REAL_RINV_UNIQ

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

REAL_RNEG_UNIQ

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

REAL_SUB_0

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

REAL_SUB_ABS

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

REAL_SUB_ADD

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

REAL_SUB_ADD2

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

REAL_SUB_INV2

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

REAL_SUB_LDISTRIB

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

REAL_SUB_LE

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

REAL_SUB_LNEG

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

REAL_SUB_LT

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

REAL_SUB_LZERO

|- !x. 0 - x = ~x

REAL_SUB_NEG2

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

REAL_SUB_RDISTRIB

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

REAL_SUB_REFL

|- !x. x - x = 0

REAL_SUB_RNEG

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

REAL_SUB_RZERO

|- !x. x - 0 = x

REAL_SUB_SUB

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

REAL_SUB_SUB2

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

REAL_SUB_TRIANGLE

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

REAL_SUMSQ

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

REAL_SUP

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

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_SUP_EXISTS

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

REAL_SUP_LE

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

REAL_SUP_SOMEPOS

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

REAL_SUP_UBOUND

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

REAL_SUP_UBOUND_LE

|- !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

sum

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

SUM_0

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

SUM_1

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

SUM_2

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

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_ADD

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

SUM_BOUND

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

SUM_CANCEL

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

SUM_CMUL

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

SUM_DIFF

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

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_GROUP

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

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_NEG

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

SUM_NSUB

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

SUM_OFFSET

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

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_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_REINDEX

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

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_TWO

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

SUM_ZERO

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

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