The Theory %real%

Parents

orders

dyadic

Children

analysis

Constants

Is__Rep	( ) SET BOOL
$<_R	BOOL
$_R	BOOL
$>_R	BOOL
$_R	BOOL
Sup	SET
1_R
0_R
$+_R
~_R
$-_R

Abs_R
$*_R
$/_R
$/_N
$^-¹
$^_N

$^_Z
Float

Aliases

<	$<_R : BOOL
	$_R : BOOL
>	$>_R : BOOL
	$_R : BOOL
+	$+_R :
~	~_R :
-	$-_R :
Abs	Abs_R :
*	$*_R :
/	$/_R :
/	$/_N :
^	$^_N :
^	$^_Z :

Types

Fixity

Left Infix 305:

-_R

Left Infix 315:

/_N

/_R

Right Infix 210:

<_R

>_R

Right Infix 300:

+_R

Right Infix 310:

*_R

Right Infix 320:

^_N

^_Z

Postfix 320:

^-¹

Definitions

Is__Rep	a Is__Rep a a Cuts (Universe, $dy_less)
_def	f TypeDefn Is__Rep f
<_R	ConstSpec ( <_R' StrictLinearOrder (Universe, <_R') UnboundedBelow (Universe, <_R') UnboundedAbove (Universe, <_R') Complete (Universe, <_R') ( ( a b <_R' ( a) ( b) a dy_less b) {x\| a a = x} DenseIn (Universe, <_R'))) $<
_R	x y x y x < y x = y
>_R	x y x > y y < x
_R	x y x y y x
Sup	ConstSpec ( Sup' A A = {} ( b x x A x b) ( x x A x Sup' A) ( b ( x x A x b) Sup' A b)) Sup
+_R 0_R 1_R	ConstSpec ( (+_R', 0_R', 1_R') ( x y z +_R' (+_R' x y) z = +_R' x (+_R' y z)) ( x y +_R' x y = +_R' y x) ( x +_R' x 0_R' = x) ( x y +_R' x y = 0_R') ( x y z y < z +_R' x y < +_R' x z) 0_R' < 1_R') ($+, 0_R, 1_R)
~_R	ConstSpec ( ~_R' x x + ~_R' x = 0_R) ~
-_R	x y x - y = x + ~ y
	0 = 0_R ( m (m + 1) = m + 1_R)
Abs_R	x Abs x = (if 0 x then x else ~ x)
*_R	ConstSpec ( _R' ( x y z _R' (_R' x y) z = _R' x (_R' y z)) ( x _R' x ( 1) = x) ( x y z _R' x (y + z) = _R' x y + _R' x z) ( x y _R' x y = _R' y x) ( x y 0 < x 0 < y 0 < _R' x y)) $*
/_R	ConstSpec ( /_R' ( y z z = 0 /_R' (y * z) z = y) ( x y z z = 0 /_R' (x * y) z = x * /_R' y z)) $/
/_N	m n m / n = m / n
^-¹	x x ^-¹ = 1 / x
^_N	( x x ^ 0 = 1) ( x m x ^ (m + 1) = x * x ^ m)
	ConstSpec ( $"'" $"'" ( 0) = 0 $"'" ( 1) = 1 ( i j $"'" (i + j) = $"'" i + $"'" j))
^_Z	ConstSpec ( ^_Z' x m ^_Z' x ( m) = x ^ m ^_Z' x (~ ( (m + 1))) = (x ^ (m + 1)) ^-¹) $^
Float	m p e Float m p e = m * 10 ^ (e + ~ p)

Theorems

dy_less_order_lemmas_thm	StrictLinearOrder (Universe, $dy_less) UnboundedBelow (Universe, $dy_less) UnboundedAbove (Universe, $dy_less) Universe DenseIn (Universe, $dy_less)
is__rep_consistent_thm	a Is__Rep a
<_R_consistent	Consistent ( <_R' StrictLinearOrder (Universe, <_R') UnboundedBelow (Universe, <_R') UnboundedAbove (Universe, <_R') Complete (Universe, <_R') ( ( a b <_R' ( a) ( b) a dy_less b) {x\| a a = x} DenseIn (Universe, <_R')))
_unbounded_below_thm	x y y < x
_unbounded_above_thm	x y x < y
_less_irrefl_thm	x x < x
_less_antisym_thm	x y (x < y y < x)
_less_trans_thm	x y z x < y y < z x < z
_less_cases_thm	x y x < y x = y y < x
__cases_thm	x y x y y x
__less_cases_thm	x y x y y < x
_eq__thm	x y x = y x y y x
__antisym_thm	x y x y y x x = y
_less__trans_thm	x y z x < y y z x < z
__less_trans_thm	x y z x y y < z x < z
__refl_thm	x x x
__trans_thm	x y z x y y z x z
___less_thm	x y x y y < x
___less_thm	x y x y y < x
_less__eq_thm	x y x < y x = y
_less_dense_thm	x y x < y ( z x < z z < y)
_complete_thm	A A = {} ( b x x A x b) ( s ( x x A x s) ( b ( x x A x b) s b))
Sup_consistent	Consistent ( Sup' A A = {} ( b x x A x b) ( x x A x Sup' A) ( b ( x x A x b) Sup' A b))
_sup_thm	A a A = {} ( x x A x a) ( x x A x Sup A) ( b ( x x A x b) Sup A b)
_less_sup_thm	A A = {} ( a x x A x a) ( x x < Sup A ( y y A x < y))
_less_sup_bc_thm	A x A = {} ( a x x A x a) ( y y A x < y) x < Sup A
__sup_thm	A a A = {} ( a x x A x a) ( x x Sup A ( y ( z z A z y) x y))
__sup_bc_thm	A a x A = {} ( a x x A x a) ( y ( z z A z y) x y) x Sup A
___sup_bc_thm	A x x A ( a x x A x a) x Sup A
__sup_thm	A B A = {} ( a x x A x a) B = {} ( b y y B y b) A B Sup A Sup B
_sup__bc_thm	A a x A = {} ( a x x A x a) ( y y A y x) Sup A x
_sup_less_bc_thm	A x z A = {} ( a x x A x a) ( y y A y x) x < z Sup A < z
_sup_eq_bc_thm	A a s A = {} ( x x A x s) ( x ( y y A y x) s x) Sup A = s
_eq_sup_bc_thm	A a s A = {} ( x x A x s) ( x ( y y A y x) s x) s = Sup A
_less_sup__thm	A a A = {} ( x x A x a) Sup A A ( x x < Sup A ( y x < y y < Sup A y A))
+_R_consistent 0_R_consistent 1_R_consistent	Consistent ( (+_R', 0_R', 1_R') ( x y z +_R' (+_R' x y) z = +_R' x (+_R' y z)) ( x y +_R' x y = +_R' y x) ( x +_R' x 0_R' = x) ( x y +_R' x y = 0_R') ( x y z y < z +_R' x y < +_R' x z) 0_R' < 1_R')
~_R_consistent	Consistent ( ~_R' x x + ~_R' x = 0_R)
_plus_assoc_thm	x y z (x + y) + z = x + y + z
_plus_comm_thm	x y x + y = y + x
_plus_unit_thm	x x + 0_R = x
_plus_mono_thm	x y z y < z x + y < x + z
_plus_assoc_thm1	x y z x + y + z = (x + y) + z
_plus_mono_thm1	x y z y < z y + x < z + x
_plus_mono_thm2	x y s t x < y s < t x + s < y + t
_plus_0_thm	x x + 0 = x 0 + x = x
_0_1_thm	0_R = 0 1_R = 1
_plus_order_thm	x y z y + x = x + y (x + y) + z = x + y + z y + x + z = x + y + z
_plus_minus_thm	x x + ~ x = 0 ~ x + x = 0
_eq_thm	x y x = y x + ~ y = 0
_plus_homomorphism_thm	m n (m + n) = m + n
_minus_clauses	x y ~ (~ x) = x x + ~ x = 0 ~ x + x = 0 ~ (x + y) = ~ x + ~ y ~ ( 0) = 0
_minus_eq_thm	x y ~ x = ~ y x = y
_0_less_thm	m 0 < (m + 1)
_one_one_thm	m n m = n m = n
_plus_clauses	x y z (x + z = y + z x = y) (z + x = y + z x = y) (x + z = z + y x = y) (z + x = z + y x = y) (x + z = z x = 0) (z + x = z x = 0) (z = z + y y = 0) (z = y + z y = 0) x + 0 = x 0 + x = x 1 = 0 0 = 1
_less_less_0_thm	x y x < y x + ~ y < 0
_less_clauses	x y z (x + z < y + z x < y) (z + x < y + z x < y) (x + z < z + y x < y) (z + x < z + y x < y) (x + z < z x < 0) (z + x < z x < 0) (x < z + x 0 < z) (x < x + z 0 < z) x < x 0 < 1 1 < 0
_less_0_less_thm	x y x < y 0 < y + ~ x
__clauses	x y z (x + z y + z x y) (z + x y + z x y) (x + z z + y x y) (z + x z + y x y) (x + z z x 0) (z + x z x 0) (x z + x 0 z) (x x + z 0 z) x x 0 1 1 0
___0_thm	x y x y x + ~ y 0
__0__thm	x y x y 0 y + ~ x
_less_thm	m n m < n m < n
_less_strong_dense_thm	x y x < y ( d 0 < d x + d < y)
__thm	m n m n m n
_sup_plus_thm	A a x A = {} ( x x A x a) Sup A + x = Sup {t\| a a A t < a + x}
_sup_plus_sup_thm	A a B b A = {} ( x x A x a) B = {} ( y y B y b) Sup A + Sup B = Sup {t\| a b a A b B t < a + b}
_delta_induction_thm	x p ( d 0 < d ( e d < e ( t x < t t < x + e p t)) ( s x < s p s p (s + d))) ( y x < y p y)
_ord_pres_strict_thm	f