- RAT_EQUIV
-
|- ∀f1 f2. rat_equiv f1 f2 ⇔ (rat_equiv f1 = rat_equiv f2)
- RAT_EQUIV_REF
-
|- ∀a. rat_equiv a a
- RAT_EQUIV_SYM
-
|- ∀a b. rat_equiv a b ⇔ rat_equiv b a
- RAT_EQUIV_TRANS
-
|- ∀a b c. rat_equiv a b ∧ rat_equiv b c ⇒ rat_equiv a c
- RAT_EQUIV_ALT
-
|- ∀a.
rat_equiv a =
(λx.
∃b c.
0 < b ∧ 0 < c ∧
(frac_mul a (abs_frac (b,b)) = frac_mul x (abs_frac (c,c))))
- rat_ABS_REP_CLASS
-
|- (∀a. abs_rat_CLASS (rep_rat_CLASS a) = a) ∧
∀c.
(∃r. rat_equiv r r ∧ (c = rat_equiv r)) ⇔
(rep_rat_CLASS (abs_rat_CLASS c) = c)
- rat_QUOTIENT
-
|- QUOTIENT rat_equiv abs_rat rep_rat
- rat_def
-
|- QUOTIENT rat_equiv abs_rat rep_rat
- rat_of_num_ind
-
|- ∀P. P 0 ∧ P (SUC 0) ∧ (∀n. P (SUC n) ⇒ P (SUC (SUC n))) ⇒ ∀v. P v
- rat_of_num_def
-
|- (0 = rat_0) ∧ (&SUC 0 = rat_1) ∧ ∀n. &SUC (SUC n) = &SUC n + rat_1
- rat_of_num_def_compute
-
|- (0 = rat_0) ∧ (&SUC 0 = rat_1) ∧
(∀n. &SUC (NUMERAL (BIT1 n)) = &NUMERAL (BIT1 n) + rat_1) ∧
∀n. &SUC (NUMERAL (BIT2 n)) = &NUMERAL (BIT2 n) + rat_1
- rat_0
-
|- 0 = abs_rat frac_0
- rat_1
-
|- 1 = abs_rat frac_1
- RAT
-
|- ∀r. abs_rat (rep_rat r) = r
- RAT_ABS_EQUIV
-
|- ∀f1 f2. (abs_rat f1 = abs_rat f2) ⇔ rat_equiv f1 f2
- RAT_EQ
-
|- ∀f1 f2.
(abs_rat f1 = abs_rat f2) ⇔
(frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
- RAT_EQ_ALT
-
|- ∀r1 r2. (r1 = r2) ⇔ (rat_nmr r1 * rat_dnm r2 = rat_nmr r2 * rat_dnm r1)
- RAT_NMREQ0_CONG
-
|- ∀f1. (frac_nmr (rep_rat (abs_rat f1)) = 0) ⇔ (frac_nmr f1 = 0)
- RAT_NMRLT0_CONG
-
|- ∀f1. frac_nmr (rep_rat (abs_rat f1)) < 0 ⇔ frac_nmr f1 < 0
- RAT_NMRGT0_CONG
-
|- ∀f1. frac_nmr (rep_rat (abs_rat f1)) > 0 ⇔ frac_nmr f1 > 0
- RAT_SGN_CONG
-
|- ∀f1. frac_sgn (rep_rat (abs_rat f1)) = frac_sgn f1
- RAT_AINV_CONG
-
|- ∀x. abs_rat (frac_ainv (rep_rat (abs_rat x))) = abs_rat (frac_ainv x)
- RAT_MINV_CONG
-
|- ∀x.
frac_nmr x ≠ 0 ⇒
(abs_rat (frac_minv (rep_rat (abs_rat x))) = abs_rat (frac_minv x))
- RAT_ADD_CONG1
-
|- ∀x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)
- RAT_ADD_CONG2
-
|- ∀x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)
- RAT_ADD_CONG
-
|- (∀x y.
abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)) ∧
∀x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)
- RAT_MUL_CONG1
-
|- ∀x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)
- RAT_MUL_CONG2
-
|- ∀x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)
- RAT_MUL_CONG
-
|- (∀x y.
abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)) ∧
∀x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)
- RAT_SUB_CONG1
-
|- ∀x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)
- RAT_SUB_CONG2
-
|- ∀x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)
- RAT_SUB_CONG
-
|- (∀x y.
abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)) ∧
∀x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)
- RAT_DIV_CONG1
-
|- ∀x y.
frac_nmr y ≠ 0 ⇒
(abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y))
- RAT_DIV_CONG2
-
|- ∀x y.
frac_nmr y ≠ 0 ⇒
(abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y))
- RAT_DIV_CONG
-
|- (∀x y.
frac_nmr y ≠ 0 ⇒
(abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y))) ∧
∀x y.
frac_nmr y ≠ 0 ⇒
(abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y))
- RAT_NMRDNM_EQ
-
|- (abs_rat (abs_frac (frac_nmr f1,frac_dnm f1)) = 1) ⇔
(frac_nmr f1 = frac_dnm f1)
- RAT_AINV_CALCULATE
-
|- ∀f1. -abs_rat f1 = abs_rat (frac_ainv f1)
- RAT_MINV_CALCULATE
-
|- ∀f1. 0 ≠ frac_nmr f1 ⇒ (rat_minv (abs_rat f1) = abs_rat (frac_minv f1))
- RAT_ADD_CALCULATE
-
|- ∀f1 f2. abs_rat f1 + abs_rat f2 = abs_rat (frac_add f1 f2)
- RAT_SUB_CALCULATE
-
|- ∀f1 f2. abs_rat f1 − abs_rat f2 = abs_rat (frac_sub f1 f2)
- RAT_MUL_CALCULATE
-
|- ∀f1 f2. abs_rat f1 * abs_rat f2 = abs_rat (frac_mul f1 f2)
- RAT_DIV_CALCULATE
-
|- ∀f1 f2.
frac_nmr f2 ≠ 0 ⇒ (abs_rat f1 / abs_rat f2 = abs_rat (frac_div f1 f2))
- RAT_EQ_CALCULATE
-
|- ∀f1 f2.
(abs_rat f1 = abs_rat f2) ⇔
(frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
- RAT_LES_CALCULATE
-
|- ∀f1 f2.
abs_rat f1 < abs_rat f2 ⇔
frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1
- RAT_OF_NUM_CALCULATE
-
|- ∀n1. &n1 = abs_rat (abs_frac (&n1,1))
- RAT_EQ0_NMR
-
|- ∀r1. (r1 = 0) ⇔ (rat_nmr r1 = 0)
- RAT_0LES_NMR
-
|- ∀r1. 0 < r1 ⇔ 0 < rat_nmr r1
- RAT_LES0_NMR
-
|- ∀r1. r1 < 0 ⇔ rat_nmr r1 < 0
- RAT_0LEQ_NMR
-
|- ∀r1. 0 ≤ r1 ⇔ 0 ≤ rat_nmr r1
- RAT_LEQ0_NMR
-
|- ∀r1. r1 ≤ 0 ⇔ rat_nmr r1 ≤ 0
- RAT_ADD_ASSOC
-
|- ∀a b c. a + (b + c) = a + b + c
- RAT_MUL_ASSOC
-
|- ∀a b c. a * (b * c) = a * b * c
- RAT_ADD_COMM
-
|- ∀a b. a + b = b + a
- RAT_MUL_COMM
-
|- ∀a b. a * b = b * a
- RAT_ADD_RID
-
|- ∀a. a + 0 = a
- RAT_ADD_LID
-
|- ∀a. 0 + a = a
- RAT_MUL_RID
-
|- ∀a. a * 1 = a
- RAT_MUL_LID
-
|- ∀a. 1 * a = a
- RAT_ADD_RINV
-
|- ∀a. a + -a = 0
- RAT_ADD_LINV
-
|- ∀a. -a + a = 0
- RAT_MUL_RINV
-
|- ∀a. a ≠ 0 ⇒ (a * rat_minv a = 1)
- RAT_MUL_LINV
-
|- ∀a. a ≠ 0 ⇒ (rat_minv a * a = 1)
- RAT_RDISTRIB
-
|- ∀a b c. (a + b) * c = a * c + b * c
- RAT_LDISTRIB
-
|- ∀a b c. c * (a + b) = c * a + c * b
- RAT_1_NOT_0
-
|- 1 ≠ 0
- RAT_MUL_LZERO
-
|- ∀r1. 0 * r1 = 0
- RAT_MUL_RZERO
-
|- ∀r1. r1 * 0 = 0
- RAT_SUB_ADDAINV
-
|- ∀r1 r2. r1 − r2 = r1 + -r2
- RAT_DIV_MULMINV
-
|- ∀r1 r2. r1 / r2 = r1 * rat_minv r2
- RAT_AINV_0
-
|- -0 = 0
- RAT_AINV_AINV
-
|- ∀r1. - -r1 = r1
- RAT_AINV_ADD
-
|- ∀r1 r2. -(r1 + r2) = -r1 + -r2
- RAT_AINV_SUB
-
|- ∀r1 r2. -(r1 − r2) = r2 − r1
- RAT_AINV_RMUL
-
|- ∀r1 r2. -(r1 * r2) = r1 * -r2
- RAT_AINV_LMUL
-
|- ∀r1 r2. -(r1 * r2) = -r1 * r2
- RAT_AINV_MINV
-
|- ∀r1. r1 ≠ 0 ⇒ (-rat_minv r1 = rat_minv (-r1))
- RAT_SUB_RDISTRIB
-
|- ∀a b c. (a − b) * c = a * c − b * c
- RAT_SUB_LDISTRIB
-
|- ∀a b c. c * (a − b) = c * a − c * b
- RAT_SUB_LID
-
|- ∀r1. 0 − r1 = -r1
- RAT_SUB_RID
-
|- ∀r1. r1 − 0 = r1
- RAT_SUB_ID
-
|- ∀r. r − r = 0
- RAT_EQ_SUB0
-
|- ∀r1 r2. (r1 − r2 = 0) ⇔ (r1 = r2)
- RAT_EQ_0SUB
-
|- ∀r1 r2. (0 = r1 − r2) ⇔ (r1 = r2)
- RAT_SGN_CALCULATE
-
|- rat_sgn (abs_rat f1) = frac_sgn f1
- RAT_SGN_CLAUSES
-
|- ∀r1.
((rat_sgn r1 = -1) ⇔ r1 < 0) ∧ ((rat_sgn r1 = 0) ⇔ (r1 = 0)) ∧
((rat_sgn r1 = 1) ⇔ r1 > 0)
- RAT_SGN_0
-
|- rat_sgn 0 = 0
- RAT_SGN_AINV
-
|- ∀r1. -rat_sgn (-r1) = rat_sgn r1
- RAT_SGN_MUL
-
|- ∀r1 r2. rat_sgn (r1 * r2) = rat_sgn r1 * rat_sgn r2
- RAT_SGN_MINV
-
|- ∀r1. r1 ≠ 0 ⇒ (rat_sgn (rat_minv r1) = rat_sgn r1)
- RAT_SGN_TOTAL
-
|- ∀r1. (rat_sgn r1 = -1) ∨ (rat_sgn r1 = 0) ∨ (rat_sgn r1 = 1)
- RAT_SGN_COMPLEMENT
-
|- ∀r1.
(rat_sgn r1 ≠ -1 ⇔ (rat_sgn r1 = 0) ∨ (rat_sgn r1 = 1)) ∧
(rat_sgn r1 ≠ 0 ⇔ (rat_sgn r1 = -1) ∨ (rat_sgn r1 = 1)) ∧
(rat_sgn r1 ≠ 1 ⇔ (rat_sgn r1 = -1) ∨ (rat_sgn r1 = 0))
- RAT_LES_REF
-
|- ∀r1. ¬(r1 < r1)
- RAT_LES_ANTISYM
-
|- ∀r1 r2. r1 < r2 ⇒ ¬(r2 < r1)
- RAT_LES_TRANS
-
|- ∀r1 r2 r3. r1 < r2 ∧ r2 < r3 ⇒ r1 < r3
- RAT_LES_TOTAL
-
|- ∀r1 r2. r1 < r2 ∨ (r1 = r2) ∨ r2 < r1
- RAT_LEQ_REF
-
|- ∀r1. r1 ≤ r1
- RAT_LEQ_ANTISYM
-
|- ∀r1 r2. r1 ≤ r2 ∧ r2 ≤ r1 ⇒ (r1 = r2)
- RAT_LEQ_TRANS
-
|- ∀r1 r2 r3. r1 ≤ r2 ∧ r2 ≤ r3 ⇒ r1 ≤ r3
- RAT_LES_01
-
|- 0 < 1
- RAT_LES_IMP_LEQ
-
|- ∀r1 r2. r1 < r2 ⇒ r1 ≤ r2
- RAT_LES_IMP_NEQ
-
|- ∀r1 r2. r1 < r2 ⇒ r1 ≠ r2
- RAT_LEQ_LES
-
|- ∀r1 r2. ¬(r2 < r1) ⇔ r1 ≤ r2
- RAT_LES_LEQ
-
|- ∀r1 r2. ¬(r2 ≤ r1) ⇔ r1 < r2
- RAT_LES_LEQ2
-
|- ∀r1 r2. r1 < r2 ⇔ r1 ≤ r2 ∧ ¬(r2 ≤ r1)
- RAT_LES_LEQ_TRANS
-
|- ∀a b c. a < b ∧ b ≤ c ⇒ a < c
- RAT_LEQ_LES_TRANS
-
|- ∀a b c. a ≤ b ∧ b < c ⇒ a < c
- RAT_0LES_0LES_ADD
-
|- ∀r1 r2. 0 < r1 ⇒ 0 < r2 ⇒ 0 < r1 + r2
- RAT_LES0_LES0_ADD
-
|- ∀r1 r2. r1 < 0 ⇒ r2 < 0 ⇒ r1 + r2 < 0
- RAT_0LES_0LEQ_ADD
-
|- ∀r1 r2. 0 < r1 ⇒ 0 ≤ r2 ⇒ 0 < r1 + r2
- RAT_LES0_LEQ0_ADD
-
|- ∀r1 r2. r1 < 0 ⇒ r2 ≤ 0 ⇒ r1 + r2 < 0
- RAT_AINV_ONE_ONE
-
|- ONE_ONE numeric_negate
- RAT_ADD_ONE_ONE
-
|- ∀r1. ONE_ONE ($+ r1)
- RAT_MUL_ONE_ONE
-
|- ∀r1. r1 ≠ 0 ⇔ ONE_ONE ($* r1)
- RAT_EQ_AINV
-
|- ∀r1 r2. (-r1 = -r2) ⇔ (r1 = r2)
- RAT_EQ_LADD
-
|- ∀r1 r2 r3. (r3 + r1 = r3 + r2) ⇔ (r1 = r2)
- RAT_EQ_RADD
-
|- ∀r1 r2 r3. (r1 + r3 = r2 + r3) ⇔ (r1 = r2)
- RAT_EQ_RMUL
-
|- ∀r1 r2 r3. r3 ≠ 0 ⇒ ((r1 * r3 = r2 * r3) ⇔ (r1 = r2))
- RAT_EQ_LMUL
-
|- ∀r1 r2 r3. r3 ≠ 0 ⇒ ((r3 * r1 = r3 * r2) ⇔ (r1 = r2))
- RAT_AINV_EQ
-
|- ∀r1 r2. (-r1 = r2) ⇔ (r1 = -r2)
- RAT_LSUB_EQ
-
|- ∀r1 r2 r3. (r1 − r2 = r3) ⇔ (r1 = r2 + r3)
- RAT_RSUB_EQ
-
|- ∀r1 r2 r3. (r1 = r2 − r3) ⇔ (r1 + r3 = r2)
- RAT_LDIV_EQ
-
|- ∀r1 r2 r3. r2 ≠ 0 ⇒ ((r1 / r2 = r3) ⇔ (r1 = r2 * r3))
- RAT_RDIV_EQ
-
|- ∀r1 r2 r3. r3 ≠ 0 ⇒ ((r1 = r2 / r3) ⇔ (r1 * r3 = r2))
- RAT_LES_RADD
-
|- ∀r1 r2 r3. r1 + r3 < r2 + r3 ⇔ r1 < r2
- RAT_LES_LADD
-
|- ∀r1 r2 r3. r3 + r1 < r3 + r2 ⇔ r1 < r2
- RAT_LES_AINV
-
|- ∀r1 r2. -r1 < -r2 ⇔ r2 < r1
- RAT_LSUB_LES
-
|- ∀r1 r2 r3. r1 − r2 < r3 ⇔ r1 < r2 + r3
- RAT_RSUB_LES
-
|- ∀r1 r2 r3. r1 < r2 − r3 ⇔ r1 + r3 < r2
- RAT_LES_RMUL_POS
-
|- ∀r1 r2 r3. 0 < r3 ⇒ (r1 * r3 < r2 * r3 ⇔ r1 < r2)
- RAT_LES_LMUL_POS
-
|- ∀r1 r2 r3. 0 < r3 ⇒ (r3 * r1 < r3 * r2 ⇔ r1 < r2)
- RAT_LES_RMUL_NEG
-
|- ∀r1 r2 r3. r3 < 0 ⇒ (r2 * r3 < r1 * r3 ⇔ r1 < r2)
- RAT_LES_LMUL_NEG
-
|- ∀r1 r2 r3. r3 < 0 ⇒ (r3 * r2 < r3 * r1 ⇔ r1 < r2)
- RAT_AINV_LES
-
|- ∀r1 r2. -r1 < r2 ⇔ -r2 < r1
- RAT_LDIV_LES_POS
-
|- ∀r1 r2 r3. 0 < r2 ⇒ (r1 / r2 < r3 ⇔ r1 < r2 * r3)
- RAT_LDIV_LES_NEG
-
|- ∀r1 r2 r3. r2 < 0 ⇒ (r1 / r2 < r3 ⇔ r2 * r3 < r1)
- RAT_RDIV_LES_POS
-
|- ∀r1 r2 r3. 0 < r3 ⇒ (r1 < r2 / r3 ⇔ r1 * r3 < r2)
- RAT_RDIV_LES_NEG
-
|- ∀r1 r2 r3. r3 < 0 ⇒ (r1 < r2 / r3 ⇔ r2 < r1 * r3)
- RAT_LES_SUB0
-
|- ∀r1 r2. r1 − r2 < 0 ⇔ r1 < r2
- RAT_LES_0SUB
-
|- ∀r1 r2. 0 < r1 − r2 ⇔ r2 < r1
- RAT_MINV_LES
-
|- ∀r1. 0 < r1 ⇒ (rat_minv r1 < 0 ⇔ r1 < 0) ∧ (0 < rat_minv r1 ⇔ 0 < r1)
- RAT_MUL_SIGN_CASES
-
|- ∀p q.
(0 < p * q ⇔ 0 < p ∧ 0 < q ∨ p < 0 ∧ q < 0) ∧
(p * q < 0 ⇔ 0 < p ∧ q < 0 ∨ p < 0 ∧ 0 < q)
- RAT_NO_ZERODIV
-
|- ∀r1 r2. (r1 = 0) ∨ (r2 = 0) ⇔ (r1 * r2 = 0)
- RAT_NO_ZERODIV_NEG
-
|- ∀r1 r2. r1 * r2 ≠ 0 ⇔ r1 ≠ 0 ∧ r2 ≠ 0
- RAT_NO_IDDIV
-
|- ∀r1 r2. (r1 * r2 = r2) ⇔ (r1 = 1) ∨ (r2 = 0)
- RAT_DENSE_THM
-
|- ∀r1 r3. r1 < r3 ⇒ ∃r2. r1 < r2 ∧ r2 < r3
- RAT_SAVE
-
|- ∀r1. ∃a1 b1. r1 = abs_rat (frac_save a1 b1)
- RAT_SAVE_MINV
-
|- ∀a1 b1.
abs_rat (frac_save a1 b1) ≠ 0 ⇒
(rat_minv (abs_rat (frac_save a1 b1)) =
abs_rat (frac_save (SGN a1 * (&b1 + 1)) (Num (ABS a1 − 1))))
- RAT_SAVE_TO_CONS
-
|- ∀a1 b1. abs_rat (frac_save a1 b1) = a1 // (&b1 + 1)
- RAT_OF_NUM
-
|- ∀n. (0 = rat_0) ∧ ∀n. &SUC n = &n + rat_1
- RAT_SAVE_NUM
-
|- ∀n. &n = abs_rat (frac_save (&n) 0)
- RAT_CONS_TO_NUM
-
|- ∀n. (&n // 1 = &n) ∧ (-&n // 1 = -&n)
- RAT_0
-
|- rat_0 = 0
- RAT_1
-
|- rat_1 = 1
- RAT_ADD_NUM_CALCULATE
-
|- (∀n m. &n + &m = &(n + m)) ∧
(∀n m. -&n + &m = if n ≤ m then &(m − n) else -&(n − m)) ∧
(∀n m. &n + -&m = if m ≤ n then &(n − m) else -&(m − n)) ∧
∀n m. -&n + -&m = -&(n + m)
- RAT_MUL_NUM_CALCULATE
-
|- (∀n m. &n * &m = &(n * m)) ∧ (∀n m. -&n * &m = -&(n * m)) ∧
(∀n m. &n * -&m = -&(n * m)) ∧ ∀n m. -&n * -&m = &(n * m)
- RAT_EQ_NUM_CALCULATE
-
|- (∀n m. (&n = &m) ⇔ (n = m)) ∧ (∀n m. (&n = -&m) ⇔ (n = 0) ∧ (m = 0)) ∧
(∀n m. (-&n = &m) ⇔ (n = 0) ∧ (m = 0)) ∧ ∀n m. (-&n = -&m) ⇔ (n = m)