%Patch files loaded: patch2 version 1.2.2.36 $$$PVSHOME/pvs-strategies (load "/home/rwb/fm/pvs/bld/manip-strategies") $$$top.pvs top: THEORY %------------------------------------------------------------------------------ % % Test suites designed to explore the capabilities/efficiency of theorem % provers for nonlinear arithmetic and algebraic manipulations. % % Author: Ricky W. Butler NASA Langley % %------------------------------------------------------------------------------ BEGIN IMPORTING algebra_probs, trig_probs END top $$$trig_inverses.pvs trig_inverses: THEORY %----------------------------------------------------------------------------- % trig_inverses % ------------- % - defines inverse trig functions: arcsin, arccos, and arctan %----------------------------------------------------------------------------- BEGIN IMPORTING trig_basic rngPI2: TYPE = {x: real | -PI/2 <= x AND x <= PI/2} rngPI: TYPE = {x: real | 0 <= x AND x <= PI} rngPI2_lt: TYPE = {x: real | -PI/2 < x AND x < PI/2} rng1 : TYPE = {y: real | -1 <= y AND y <= 1} a,x: VAR real y : VAR rng1 % -------------------- Arcsin -------------------- rsin(x: rngPI2): rng1 = sin(x) rsin_bij: AXIOM bijective?(rsin) arcsin(y: rng1): {x: rngPI2 | y = rsin(x)} arcsin_def: LEMMA arcsin = inverse(rsin) sin_arcsin: LEMMA (FORALL (y: rng1): sin(arcsin(y)) = y) arcsin_sin: LEMMA (FORALL (x: rngPI2): arcsin(sin(x)) = x) % -------------------- Arccos -------------------- rcos(x: rngPI): rng1 = cos(x) rcos_bij: AXIOM bijective?(rcos) arccos(y: rng1): {x: rngPI | y = rcos(x)} arccos_def: LEMMA arccos = inverse(rcos) cos_arccos: LEMMA (FORALL (y: rng1): cos(arccos(y)) = y) arccos_cos: LEMMA (FORALL (x: rngPI): arccos(cos(x)) = x) % -------------------- Arctan -------------------- rtan_prep: LEMMA FORALL (x: rngPI2_lt): Tan?(x); rtan(x: rngPI2_lt): real = tan(x) rtan_bij: AXIOM bijective?(rtan) arctan(y: real): {x: rngPI2_lt | y = rtan(x)} arctan_def: LEMMA arctan = inverse(rtan) tan_arctan: LEMMA (FORALL (y: real): tan(arctan(y)) = y) arctan_tan: LEMMA (FORALL (x: rngPI2_lt): arctan(tan(x)) = x) END trig_inverses $$$trig_inverses.prf (|trig_inverses| (|arcsin_TCC1| "" (INST + "inverse(rsin)") (("" (SKOSIMP*) (("" (LEMMA "bijective_inverse[rngPI2,rng1]") (("" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (HIDE 2) (("2" (LEMMA "rsin_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|arcsin_def_TCC1| "" (INST 1 "PI/2") (("" (ASSERT) NIL NIL)) NIL) (|arcsin_def| "" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (TYPEPRED "arcsin(x!1)") (("1" (LEMMA "bijective_inverse[rngPI2,rng1]") (("1" (INST?) (("1" (ASSERT) NIL NIL) ("2" (LEMMA "rsin_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (LEMMA "bijective_inverse[rngPI2,rng1]") (("2" (INST?) (("1" (ASSERT) NIL NIL) ("2" (LEMMA "rsin_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_arcsin| "" (SKOSIMP*) (("" (TYPEPRED "arcsin(y!1)") (("" (EXPAND "rsin") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|arcsin_sin| "" (SKOSIMP*) (("" (TYPEPRED "arcsin(sin(x!1))") (("" (LEMMA "rsin_bij") (("" (EXPAND "bijective?") (("" (FLATTEN) (("" (EXPAND "injective?") (("" (INST -1 "x!1" "arcsin(sin(x!1))") (("" (EXPAND "rsin") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|arcsin_abcde| "" (SKOSIMP*) (("" (REPLACE -1 * RL) (("" (HIDE -1) (("" (CASE "(EXISTS (i:int),(c: rngPI2): c = a!1 + 2*i*PI)") (("1" (SKOSIMP*) (("1" (CASE-REPLACE "sin(a!1) = sin(c!1)") (("1" (HIDE -1) (("1" (REWRITE "arcsin_sin") (("1" (INST + "-i!1") (("1" (ASSERT) NIL))))))) ("2" (HIDE 2) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REWRITE "sin_plus") (("2" (LEMMA "sin_k_PI") (("2" (INST -1 "2*i!1") (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (LEMMA "cos_k_PI") (("2" (INST -1 "2*i!1") (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (ASSERT) (("2" (LEMMA "even_m1_pow") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))) ("2" (HIDE 2) (("2" (NAME "J" "floor(a!1/(4*PI))") (("2" (INST + "-J" "(a!1-2*J*PI)") (("1" (ASSERT) NIL) ("2" (POSTPONE) NIL))))))))))))))) (|arccos_TCC1| "" (INST + "inverse(rcos)") (("" (SKOSIMP*) (("" (LEMMA "bijective_inverse[rngPI,rng1]") (("" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (HIDE 2) (("2" (LEMMA "rcos_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|arccos_def_TCC1| "" (INST + "PI") (("" (ASSERT) NIL NIL)) NIL) (|arccos_def| "" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (TYPEPRED "arccos(x!1)") (("1" (LEMMA "bijective_inverse[rngPI,rng1]") (("1" (INST?) (("1" (ASSERT) NIL NIL) ("2" (LEMMA "rcos_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (LEMMA "bijective_inverse[rngPI,rng1]") (("2" (INST?) (("1" (ASSERT) NIL NIL) ("2" (LEMMA "rcos_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_arccos| "" (SKOSIMP*) (("" (TYPEPRED "arccos(y!1)") (("" (EXPAND "rcos") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|arccos_cos| "" (SKOSIMP*) (("" (TYPEPRED "arccos(cos(x!1))") (("" (LEMMA "rcos_bij") (("" (EXPAND "bijective?") (("" (FLATTEN) (("" (EXPAND "injective?") (("" (INST -1 "x!1" "arccos(cos(x!1))") (("" (EXPAND "rcos") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rtan_prep| "" (SKOSIMP*) (("" (EXPAND "Tan?") (("" (TYPEPRED "x!1") (("" (LEMMA "cos_eq_0_2PI") (("" (INST?) (("" (ASSERT) (("" (LEMMA "cos_period") (("" (INST?) (("" (INST -1 "1") (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "cos_eq_0_2PI") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rtan_TCC1| "" (SKOSIMP*) (("" (REWRITE "rtan_prep") NIL NIL)) NIL) (|arctan_TCC1| "" (INST + "inverse(rtan)") (("" (SKOSIMP*) (("" (LEMMA "bijective_inverse[rngPI2_lt,real]") (("" (INST?) (("1" (ASSERT) NIL NIL) ("2" (HIDE 2) (("2" (LEMMA "rtan_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|arctan_def_TCC1| "" (INST 1 "0") (("" (ASSERT) (("" (CASE-REPLACE "0 < PI ") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|arctan_def| "" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (TYPEPRED "arctan(x!1)") (("1" (LEMMA "bijective_inverse[rngPI2_lt,real]") (("1" (INST?) (("1" (ASSERT) NIL NIL) ("2" (LEMMA "rtan_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (LEMMA "bijective_inverse[rngPI2_lt,real]") (("2" (INST?) (("1" (ASSERT) NIL NIL) ("2" (LEMMA "rtan_bij") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|tan_arctan_TCC1| "" (SKOSIMP*) (("" (TYPEPRED "arctan(y!1)") (("" (LEMMA "rtan_prep") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|tan_arctan| "" (SKOSIMP*) (("" (TYPEPRED "arctan(y!1)") (("" (EXPAND "rtan") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|arctan_tan| "" (SKOSIMP*) (("" (TYPEPRED "arctan(tan(x!1))") (("1" (LEMMA "rtan_bij") (("1" (EXPAND "bijective?") (("1" (FLATTEN) (("1" (EXPAND "injective?") (("1" (INST -1 "x!1" "arctan(tan(x!1))") (("1" (EXPAND "rtan") (("1" (ASSERT) NIL NIL)) NIL) ("2" (LEMMA "rtan_prep") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "rtan_prep") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) $$$sigma.pvs sigma[T: TYPE FROM int]: THEORY %------------------------------------------------------------------------------ % The summations theory introduces and defines properties of the sigma % function that sums an arbitrary function F: [T -> real] over a range % from low to high % % high % ---- % sigma(low, high, F) = \ F(j) % / % ---- % j = low % %------------------------------------------------------------------------------ BEGIN ASSUMING connected_domain: ASSUMPTION (FORALL (x, y: T), (z: integer): x <= z AND z <= y IMPLIES T_pred(z)) ENDASSUMING low,high, l,h,n,m,i : VAR T rng, nn : VAR nat pn : VAR posnat z : VAR int a,x,B : VAR real F, G: VAR function[T -> real] sigma(low, high, F): RECURSIVE real = IF low > high THEN 0 ELSIF high = low THEN F(low) ELSE F(high) + sigma(low, high-1, F) ENDIF MEASURE (LAMBDA low, high, F: abs(high-low)) sigma_sum : THEOREM sigma(low, high, F) + sigma(low, high, G) = sigma(low, high, (LAMBDA i: F(i) + G(i))) sigma_split : THEOREM low <= m AND m < high IMPLIES sigma(low, high, F) = sigma(low, m, F) + sigma(m+1, high, F) sigma_diff : THEOREM low <= m AND m < high IMPLIES sigma(low, high, F) - sigma(low, m, F) = sigma(m+1, high, F) sigma_diff_neg: THEOREM low <= m AND m < high IMPLIES sigma(low, m, F) - sigma(low, high, F) = - sigma(m+1, high, F) sigma_spl : THEOREM T_pred(low + nn + pn) IMPLIES sigma(low, low+nn+pn, F) = sigma(low,low+nn,F) + sigma(low+nn+1,low+nn+pn,F) sigma_first : THEOREM high > low IMPLIES sigma(low, high, F) = F(low) + sigma(low+1, high, F) sigma_last : THEOREM high > low IMPLIES sigma(low, high, F) = sigma(low, high-1, F) + F(high) sigma_eq_arg : THEOREM sigma(low, low, F) = F(low) sigma_const : THEOREM sigma(low, high, (LAMBDA i: x)) = IF high >= low THEN (high-low+1) * x ELSE 0 ENDIF sigma_scal : THEOREM sigma(low, high, (LAMBDA i: a * F(i))) = a * sigma(low, high, F) sigma_bound : THEOREM low <= high AND (FORALL i: i >= low AND i <= high IMPLIES F(i) <= B) IMPLIES sigma(low, high, F) <= B*abs(high-low+1) sigma_abs : THEOREM abs(sigma(low, high, F)) <= sigma(low, high, LAMBDA (n: T): abs(F(n))) sigma_abs_bnd : THEOREM (FORALL (i: subrange(low,high)): abs(F(i)) <= G(i)) IMPLIES sigma(low, high, LAMBDA (n: T): abs(F(n))) <= sigma(low, high, G) restrict(F, low, high): function[T -> real] = (LAMBDA i: IF i < low OR i > high THEN 0 ELSE F(i) ENDIF ) sigma_restrict : THEOREM l <= low AND h >= high IMPLIES sigma(low,high,F) = sigma(low,high,restrict(F,l,h)) sigma_restrict_eq: THEOREM restrict(F,low,high) = restrict(G,low,high) IMPLIES sigma(low,high,F) = sigma(low,high,G) sigma_eq : THEOREM (FORALL (n: subrange(low,high)): F(n) = G(n)) IMPLIES sigma(low,high,F) = sigma(low,high,G) sigma_shift_T : THEOREM (FORALL (i:T): T_pred(i+z)) IMPLIES sigma(low+z,high+z,F) = sigma(low,high, (LAMBDA (i:T): F(i+z))) % ------------------- Alternate Summation --------------------- sigma_nonneg : THEOREM (FORALL i: F(i) >= 0) IMPLIES sigma(low, high, F) >= 0 sigma_nonpos : THEOREM (FORALL i: F(i) <= 0) IMPLIES sigma(low, high, F) <= 0 Fnnr: VAR function[T -> nonneg_real] Fnpr: VAR function[T -> nonpos_real] Fnat: VAR function[T -> nat] Fnpi: VAR function[T -> nonpos_int] JUDGEMENT sigma(low,high,Fnnr) HAS_TYPE nonneg_real JUDGEMENT sigma(low,high,Fnpr) HAS_TYPE nonpos_real JUDGEMENT sigma(low,high,Fnat) HAS_TYPE nat JUDGEMENT sigma(low,high,Fnpi) HAS_TYPE nonpos_int sigma_nonneg_eq_0 : THEOREM sigma(low,high,Fnnr) = 0 AND low <= i AND i <= high IMPLIES Fnnr(i) = 0 % ------------------- Iterative Summation (tail recursion) ------------ sum_it_def(low, high, F,a): RECURSIVE real = IF low > high THEN a ELSIF low = high THEN a+F(low) ELSE sum_it_def(low+1,high,F,a+F(low)) ENDIF MEASURE (LAMBDA low, high, F, a: abs(high-low)) sum_it(low,high,F) : real = sum_it_def(low,high,F,0) sum_it_prop : LEMMA low <= i AND i < high => sum_it_def(i+1,high,F,sigma(low,i,F)) = sigma(low,high,F) sum_it_sigma: LEMMA sum_it(low,high,F) = sigma(low,high,F) END sigma $$$sigma.prf (|sigma| (|sigma_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (LEMMA "connected_domain") (("" (INST?) (("" (INST -1 "low!1" "high!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_TCC2| "" (SKOSIMP*) (("" (GRIND) NIL NIL)) NIL) (|sigma_sum| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): T_pred(low!1+rng) IMPLIES sigma(low!1, low!1+rng, F!1) + sigma(low!1, low!1+rng, G!1) = sigma(low!1, low!1+rng, LAMBDA i: F!1(i) + G!1(i)))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng" 1) (("1" (FLATTEN) (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SPLIT -1) (("1" (EXPAND "sigma" 1) (("1" (PROPAX) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "j!1+low!1+1" "j!1+low!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_split_TCC1| "" (SKOSIMP*) (("" (LEMMA "connected_domain") (("" (INST -1 "low!1" "high!1" "m!1+1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sigma_split| "" (CASE "(FORALL (F: [T -> real]), low,m,rng: m >= low AND m < low+rng AND T_pred(low+rng) IMPLIES sigma(low, low+rng, F) = sigma(low, m, F) + sigma(m+1, low+rng, F))") (("1" (SKOSIMP*) (("1" (INST -1 "F!1" "low!1" "m!1" "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (EXPAND "sigma" 1 3) (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE-REPLACE "m!1 = 1 + j!1 + low!1") (("1" (HIDE -1) (("1" (EXPAND "sigma" + 3) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (INST -1 "F!1" "low!1" "m!1") (("2" (EXPAND "sigma" + 1) (("2" (EXPAND "sigma" + 2) (("2" (LIFT-IF) (("2" (GROUND) (("2" (HIDE 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "1+j!1+low!1" "j!1+low!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (LEMMA "connected_domain") (("3" (INST -1 "m!1" "low!1 + rng!2" "1+m!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (LEMMA "connected_domain") (("3" (INST -1 "low!1" "low!1 + rng!1" "1+m!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_diff| "" (SKOSIMP*) (("" (LEMMA "sigma_split") (("" (INST?) (("" (INST -1 "m!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_diff_neg| "" (SKOSIMP*) (("" (LEMMA "sigma_diff") (("" (INST -1 "F!1" "high!1" "low!1" "m!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sigma_spl_TCC1| "" (SKOSIMP*) (("" (LEMMA "connected_domain") (("" (INST -1 "low!1" "low!1+nn!1+pn!1" "nn!1+low!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sigma_spl_TCC2| "" (SKOSIMP*) (("" (LEMMA "connected_domain") (("" (INST -1 "low!1" "low!1+nn!1+pn!1" "nn!1+low!1+1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sigma_spl| "" (INDUCT "pn" 1) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (SKOSIMP*) (("3" (EXPAND "sigma" 1 1) (("3" (EXPAND "sigma" 1 3) (("3" (GROUND) (("1" (INST?) (("1" (SPLIT -1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LIFT-IF) (("1" (GROUND) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (EXPAND "sigma" 1 2) (("1" (EXPAND "sigma" 1 2) (("1" (LIFT-IF) (("1" (GROUND) (("1" (REPLACE -1) (("1" (ASSERT) (("1" (EXPAND "sigma" 1) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "sigma" 2 3) (("2" (LIFT-IF) (("2" (GROUND) (("1" (EXPAND "sigma" 1 2) (("1" (REPLACE -1) (("1" (ASSERT) (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "sigma" 2 1) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "1 + j!1 + low!1 + nn!1" "j!1 + low!1 + nn!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (CASE-REPLACE "j!1 = 0") (("1" (ASSERT) (("1" (HIDE -1) (("1" (LIFT-IF) (("1" (GROUND) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "sigma" 2 1) (("2" (EXPAND "sigma") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (LEMMA "connected_domain") (("4" (INST -1 "low!1" "low!1 + nn!1 +pn!2" "1 + low!1 + nn!1") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("5" (HIDE 2) (("5" (SKOSIMP*) (("5" (LEMMA "connected_domain") (("5" (INST -1 "low!1" "low!1 + nn!1 +pn!2" "low!1 + nn!1") (("5" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_first_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (LEMMA "connected_domain") (("" (INST -1 "low!1" "high!1" "low!1+1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_first| "" (SKOSIMP*) (("" (CASE-REPLACE "low!1=high!1") (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL) ("2" (LEMMA "sigma_split") (("2" (INST?) (("2" (INST -1 "low!1") (("2" (ASSERT) (("2" (EXPAND "sigma" -1 3) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_last_TCC1| "" (SKOSIMP*) (("" (LEMMA "connected_domain") (("" (INST -1 "low!1" "high!1" "high!1-1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sigma_last| "" (SKOSIMP*) (("" (CASE-REPLACE "low!1=high!1") (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL) ("2" (LEMMA "sigma_split") (("2" (INST -1 "F!1" "high!1" "low!1" "high!1-1") (("1" (ASSERT) (("1" (EXPAND "sigma" -1 2) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "high!1" "high!1-1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_eq_arg| "" (SKOSIMP*) (("" (EXPAND "sigma") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|sigma_const| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): T_pred(low!1+rng) IMPLIES sigma(low!1, low!1+rng, (LAMBDA i: x!1)) = IF low!1+rng >= low!1 THEN (low!1+rng - low!1 + 1) * x!1 ELSE 0 ENDIF)") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (REWRITE "sigma_eq_arg") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) (("2" (HIDE 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "j!1+low!1+1" "j!1+low!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_scal| "" (SKOSIMP*) (("" (CASE "(FORALL (rng:nat): T_pred(low!1+rng) IMPLIES sigma(low!1, low!1+rng, (LAMBDA i: a!1 * F!1(i))) = a!1 * sigma(low!1, low!1+rng, F!1))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (ASSERT) (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) (("2" (HIDE 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "j!1+low!1+1" "j!1+low!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_bound| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): T_pred(low!1+rng) AND (FORALL i: i >= low!1 AND i <= low!1+rng IMPLIES F!1(i) <= B!1) IMPLIES sigma(low!1, low!1+rng, F!1) <= B!1 * abs(low!1+rng - low!1 + 1))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (HIDE -2 2) (("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (REWRITE "sigma_eq_arg") (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) (("2" (SPLIT -1) (("1" (EXPAND "abs") (("1" (INST - "1+j!1+low!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE -2 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "1+j!1+low!1" "j!1+low!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE -2 2) (("3" (SKOSIMP*) (("3" (REVEAL -1) (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_abs| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): T_pred(low!1+rng) IMPLIES abs(sigma(low!1, low!1+rng, F!1)) <= sigma(low!1, low!1+rng, LAMBDA (n: T): abs(F!1(n))))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (EXPAND "sigma") (("2" (EXPAND "abs") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (ASSERT) (("1" (EXPAND "sigma") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (SPLIT -1) (("1" (LEMMA "triangle") (("1" (INST?) (("1" (ASSERT) NIL NIL) ("2" (HIDE -1 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "1+j!1+low!1" "j!1+low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "1+j!1+low!1" "j!1+low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_abs_bnd_TCC1| "" (SKOSIMP*) (("" (TYPEPRED "i!1") (("" (LEMMA "connected_domain") (("" (INST -1 "low!1" "high!1" "i!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_abs_bnd| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): T_pred(low!1+rng) AND (FORALL (i: subrange(low!1, low!1+rng)): abs(F!1(i)) <= G!1(i)) IMPLIES sigma(low!1, low!1+rng, LAMBDA (n: T): abs(F!1(n))) <= sigma(low!1, low!1+rng, G!1))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (EXPAND "sigma") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng" 1) (("1" (ASSERT) (("1" (FLATTEN) (("1" (EXPAND "sigma") (("1" (INST -1 "low!1") NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (SPLIT -1) (("1" (EXPAND "sigma" 1) (("1" (INST - "1+j!1+low!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE -2 -3 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "1+j!1+low!1" "j!1+low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST -2 "i!1") NIL NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (TYPEPRED "i!1") (("3" (LEMMA "connected_domain") (("3" (INST -1 "low!1" "low!1+rng!2" "i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (ASSERT) (("4" (SKOSIMP*) (("4" (TYPEPRED "i!1") (("4" (LEMMA "connected_domain") (("4" (INST -1 "low!1" "low!1+rng!2" "i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (ASSERT) (("5" (SKOSIMP*) (("5" (TYPEPRED "i!1") (("5" (LEMMA "connected_domain") (("5" (INST -1 "low!1" "low!1+rng!2" "i!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (TYPEPRED "i!1") (("3" (LEMMA "connected_domain") (("3" (INST -1 "low!1" "low!1+rng!1" "i!1") (("1" (ASSERT) NIL NIL) ("2" (LEMMA "connected_domain") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_restrict| "" (SKOSIMP*) (("" (CASE "(FORALL (rng:nat): low!1+rng <= high!1 IMPLIES sigma(low!1, low!1+rng, F!1) = sigma(low!1, low!1+rng, restrict(F!1, l!1, h!1)))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INDUCT "rng") (("1" (HIDE 2) (("1" (REWRITE "sigma_eq_arg") (("1" (REWRITE "sigma_eq_arg") (("1" (EXPAND "restrict") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (EXPAND "restrict") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2 3) (("3" (SKOSIMP*) (("3" (LEMMA "connected_domain") (("3" (INST -1 "low!1" "high!1" "rng!2+low!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (HIDE 2) (("3" (LEMMA "connected_domain") (("3" (INST -1 "low!1" "high!1" "rng!1+low!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_restrict_eq| "" (SKOSIMP*) (("" (LEMMA "sigma_restrict") (("" (INST?) (("" (INST -1 "high!1" "low!1") (("" (ASSERT) (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "sigma_restrict") (("" (INST -1 "G!1" "high!1" "high!1" "low!1" "low!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_eq| "" (SKOSIMP*) (("" (LEMMA "sigma_restrict_eq") (("" (INST?) (("" (ASSERT) (("" (HIDE 2) (("" (EXPAND "restrict") (("" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("" (LIFT-IF) (("" (GROUND) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_shift_T_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sigma_shift_T_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|sigma_shift_T_TCC3| "" (SUBTYPE-TCC) NIL NIL) (|sigma_shift_T| "" (SKOLEM 1 ("F" "high" "low" "z")) (("" (GROUND) (("" (CASE "low <= high") (("1" (CASE "(FORALL (lh: T| low <= lh AND lh <= high): sigma(low + z, lh + z, F) = sigma(low, lh, LAMBDA (n:T): F(n + z)))") (("1" (INST -1 "high") NIL NIL) ("2" (HIDE 2) (("2" (LEMMA "subrange_induction[low,high]") (("1" (INST -1 "LAMBDA (lh: T | low <= lh AND lh <= high): sigma(low + z, lh + z, F) = sigma(low, lh, LAMBDA (n: T): F(n + z))") (("1" (GROUND) (("1" (SKOLEM 1 "r") (("1" (INST -1 "r") NIL NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "sigma") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOLEM 1 "k") (("3" (GROUND) (("3" (EXPAND "sigma" 1) (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (GROUND) (("2" (SKOLEM 1 "xx") (("2" (GROUND) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low" "high" "xx") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOLEM 1 ("r" "n")) (("3" (INST -2 "n") NIL NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (SKOLEM 1 "r") (("4" (INST -2 "r") NIL NIL)) NIL)) NIL) ("5" (HIDE 2) (("5" (SKOLEM 1 "r") (("5" (INST -2 "low") NIL NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOLEM 1 ("r" "n")) (("3" (INST -2 "n") NIL NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (SKOLEM 1 "r") (("4" (INST -2 "r") NIL NIL)) NIL)) NIL) ("5" (HIDE 2) (("5" (SKOLEM 1 "r") (("5" (INST -2 "low") NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE "low + z > high + z") (("1" (EXPAND "sigma") (("1" (GROUND) NIL NIL)) NIL) ("2" (HIDE -1 3) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_nonneg| "" (SKOSIMP*) (("" (CASE "(FORALL (rng:nat): T_pred(low!1+rng) IMPLIES sigma(low!1,low!1+rng, F!1) >= 0)") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INDUCT "rng") (("1" (ASSERT) (("1" (REWRITE "sigma_eq_arg") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SPLIT -1) (("1" (EXPAND "sigma" 1) (("1" (ASSERT) (("1" (INST -3 "1 + j!1 + low!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "1 + j!1 + low!1" "j!1 + low!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_nonpos| "" (SKOSIMP*) (("" (CASE "(FORALL (rng:nat): T_pred(low!1+rng) IMPLIES sigma(low!1,low!1+rng, F!1) <= 0)") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INDUCT "rng") (("1" (ASSERT) (("1" (REWRITE "sigma_eq_arg") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SPLIT -1) (("1" (EXPAND "sigma" 1) (("1" (ASSERT) (("1" (INST -3 "1 + j!1 + low!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "1 + j!1 + low!1" "j!1 + low!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_TCC3| "" (SKOSIMP*) (("" (REWRITE "sigma_nonneg") (("" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sigma_TCC4| "" (SKOSIMP*) (("" (REWRITE "sigma_nonpos") (("" (HIDE 2) (("" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_TCC5| "" (AUTO-REWRITE-THEORY "integers") (("" (AUTO-REWRITE-THEORY "rationals") (("" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): T_pred(low!1+rng) IMPLIES (rational_pred(sigma(low!1, low!1+rng, Fnat!1)) AND integer_pred(sigma(low!1, low!1+rng, Fnat!1))) AND sigma(low!1, low!1+rng, Fnat!1) >= 0)") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng" 1) (("1" (EXPAND "sigma") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (SPLIT -1) (("1" (FLATTEN) (("1" (GROUND) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "low!1 + (j!1 + 1)" "low!1 + j!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_TCC6| "" (AUTO-REWRITE-THEORY "integers") (("" (AUTO-REWRITE-THEORY "rationals") (("" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): T_pred(low!1+rng) IMPLIES (rational_pred(sigma(low!1, low!1+rng, Fnpi!1)) AND integer_pred(sigma(low!1, low!1+rng, Fnpi!1))) AND sigma(low!1, low!1+rng, Fnpi!1) <= 0)") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng" 1) (("1" (EXPAND "sigma") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (SPLIT -1) (("1" (FLATTEN) (("1" (GROUND) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "low!1 + (j!1 + 1)" "low!1 + j!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_nonneg_eq_0| "" (SKOSIMP*) (("" (CASE "FORALL (rng:nat): T_pred(low!1+rng) AND sigma(low!1, low!1+rng, Fnnr!1) = 0 AND low!1 <= i!1 AND i!1 <= low!1 + rng IMPLIES Fnnr!1(i!1) = 0") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (SPLIT -1) (("1" (PROPAX) NIL NIL) ("2" (HIDE -2 -3 -4 -5 -6 -7 -8 2 3) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low!1" "low!1+j!1+1" "low!1+j!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (EXPAND "sigma" -2) (("3" (ASSERT) NIL NIL)) NIL) ("4" (PROPAX) NIL NIL) ("5" (EXPAND "sigma" -2) (("5" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_it_def_TCC1| "" (SKOLEM 1 ("h" "l")) (("" (GROUND) (("" (LEMMA "connected_domain") (("" (INST -1 "l" "h" "1+l") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_it_def_TCC2| "" (TERMINATION-TCC) NIL NIL) (|sum_it_prop| "" (SKOLEM 1 ("F" "high" "i" "low")) (("" (GROUND) (("" (LEMMA "subrange_induction[low,high-1]") (("" (INST -1 "lambda(lh:T| low <= lh AND lh < high): sum_it_def((high-lh)+low, high, F, sigma(low,(high-lh)+low-1, F)) = sigma(low, high, F)") (("1" (GROUND) (("1" (INST -1 "high-i+low-1") (("1" (GROUND) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "sum_it_def") (("2" (NAME-REPLACE "SS" "sigma(low,high-1,F)") (("1" (EXPAND "sigma") (("1" (REVEAL -1) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (REVEAL -1) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low" "high" "high-1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOLEM 1 "k") (("3" (GROUND) (("3" (EXPAND "sum_it_def" 1) (("3" (CASE-REPLACE " F(-1 - k + high + low) + sigma(low, -2 - k + high + low, F) = sigma(low, -1 - k + high + low, F)") (("1" (HIDE 2) (("1" (NAME-REPLACE "SS" "sigma(low, -2 - k + high + low, F)") (("1" (EXPAND "sigma" 1) (("1" (REVEAL -1) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low" "high" "-2 - k + high + low") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2 2) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low" "high" "-2 - k + high + low") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE -2 2) (("3" (LEMMA "connected_domain") (("3" (GROUND) (("3" (INST -1 "low" "high" "-1 - k + high + low") (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (SKOLEM 1 "lh") (("2" (GROUND) (("2" (LEMMA "connected_domain") (("2" (INST -1 "low" "high" "lh") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOLEM 1 "lh") (("3" (LEMMA "connected_domain") (("3" (INST -1 "low" "high" "-1 - lh + high + low") (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (LEMMA "connected_domain") (("4" (SKOLEM 1 "lh") (("4" (INST -1 "low" "high" "high-lh+low") (("4" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_it_sigma| "" (SKOLEM 1 ("F" "high" "low")) (("" (CASE "low > high") (("1" (EXPAND "sum_it") (("1" (EXPAND "sum_it_def") (("1" (EXPAND "sigma") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE "low = high") (("1" (HIDE 1) (("1" (REPLACE -1 :HIDE? T) (("1" (EXPAND "sum_it") (("1" (EXPAND "sum_it_def") (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "low < high") (("1" (HIDE 1 2) (("1" (EXPAND "sum_it") (("1" (EXPAND "sum_it_def") (("1" (GROUND) (("1" (LEMMA "sum_it_prop") (("1" (INST -1 "F" "high" "low" "low") (("1" (GROUND) (("1" (HIDE -2) (("1" (CASE-REPLACE "sigma(low,low,F) = F(low)") (("1" (HIDE -1 2) (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$sigma_posnat.pvs sigma_posnat: THEORY %------------------------------------------------------------------------------ % The summations theory introduces and defines properties of the sigma % function that sums an arbitrary function F: [T -> real] over a range % from low to high % % high % ---- % sigma(low, high, F) = \ F(j) % / % ---- % j = low % %------------------------------------------------------------------------------ BEGIN IMPORTING sigma[posnat] low, high, n, m: VAR posnat F: VAR function[posnat -> real] % --------- Following Theorems Not Provable In Generic Framework ------- sigma_shift: THEOREM sigma(low+m,high+m,F) = sigma(low,high, (LAMBDA (n: posnat): F(n+m))) sigma_shift_neg: THEOREM low - m > 0 and low <= high IMPLIES sigma(low-m,high-m,F) = sigma(low,high, (LAMBDA n: IF n-m <= 0 THEN 0 ELSE F(n-m) ENDIF)) END sigma_posnat $$$sigma_posnat.prf (|sigma_posnat| (|IMP_sigma_TCC1| "" (ASSUMING-TCC) NIL NIL) (|IMP_sigma_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|sigma_shift| "" (SKOSIMP*) (("" (REWRITE "sigma_shift_T") NIL NIL)) NIL) (|sigma_shift_neg_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|sigma_shift_neg_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|sigma_shift_neg_TCC3| "" (SUBTYPE-TCC) NIL NIL) (|sigma_shift_neg| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): sigma(low!1 - m!1, low!1+rng - m!1, F!1) = sigma(low!1, low!1+rng, LAMBDA n: IF n - m!1 <= 0 THEN 0 ELSE F!1(n - m!1) ENDIF))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (ASSERT) (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (ASSERT) NIL NIL)) NIL)) NIL)) $$$trig_approx.pvs trig_approx : THEORY %----------------------------------------------------------------------------- % trig_approx % ----------- % - taylor series approximations to trig functions: % sin_approx(a,n): sum first n terms of taylor expansion of sin % cos_approx(a,n): sum first n terms of taylor expansion of cos % tan_approx(a,n): sum first n terms of taylor expansion of tan % - defines upper and lower bounds on trig functions: % sin_lb(a) = sin_approx(a,4) % sin_ub(a) = sin_approx(a,5) % cos_lb(a) = cos_approx(a,3) % cos_ub(a) = cos_approx(a,4) % tan_ub(a) = sin_ub(a)/cos_lb(a) % tan_lb(a) = sin_lb(a)/cos_ub(a) %----------------------------------------------------------------------------- BEGIN % sigmal: LIBRARY = "../reals" IMPORTING trig_basic, sigma_posnat, factorial i : VAR posnat n : VAR posnat a : VAR real sin_term(a)(i) : real = (-1)^(i-1) * a^(2*i-1)/factorial(2*i-1) cos_term(a)(i) : real = (-1)^i * a^(2*i)/factorial(2*i) sin_approx(a,n) : real = sigma(1, n, sin_term(a)) cos_approx(a,n) : real = 1+sigma(1, n, cos_term(a)) sin_bound : AXIOM 0 <= a AND a <= PI IMPLIES sin_approx(a,2*n) <= sin(a) AND sin(a) <= sin_approx(a,2*n+1) cos_bound : AXIOM -PI/2 <= a AND a <= PI/2 IMPLIES cos_approx(a,2*n+1) <= cos(a) AND cos(a) <= cos_approx(a,2*(n+1)) sin_lb(a) : real = sin_approx(a,4) sin_ub(a) : real = sin_approx(a,5) cos_lb(a) : real = cos_approx(a,3) cos_ub(a) : real = cos_approx(a,4) tan_ub(a:real|cos_lb(a) /= 0) : real = sin_ub(a)/cos_lb(a) tan_lb(a:real|cos_ub(a) /= 0) : real = sin_lb(a)/cos_ub(a) % --------------------- Taylor expansion of sin >= 0 --------------------- sin_term_nonzero : LEMMA 0 /= a IMPLIES sin_term(a)(n) /= 0 sin_term_next : LEMMA sin_term(a)(n+1) = sin_term(a)(n) * -1 * a*a / ((2*n+1) * 2*n) sin_terms_alternate : LEMMA 0 < a IMPLIES (sin_term(a)(n+1) < 0 IFF sin_term(a)(n) > 0) sin_terms_decr : LEMMA 0 < a AND a <= PI/2 IMPLIES abs(sin_term(a)(n)) > 2 * abs(sin_term(a)(n+1)) sin_approx_gt_term : LEMMA 0 < a AND a <= PI/2 IMPLIES sin_approx(a,n) > 2 * abs(sin_term(a)(n+1)) sin_approx_n_gt_0 : LEMMA 0 < a AND a <= PI/2 IMPLIES sin_approx(a,n) > 0 sin_lb_gt_0 : LEMMA 0 < a AND a <= PI/2 IMPLIES sin_lb(a) > 0 SIN : LEMMA 0 <= a AND a <= PI IMPLIES sin_lb(a) <= sin(a) AND sin_ub(a) >= sin(a) COS : LEMMA -PI/2 <= a AND a <= PI/2 IMPLIES cos_lb(a) <= cos(a) AND cos_ub(a) >= cos(a) TAN : LEMMA 0 <= a AND a < PI/2 AND cos_lb(a) > 0 IMPLIES tan_ub(a) >= tan(a) AND tan_lb(a) <= tan(a) END trig_approx $$$trig_approx.prf (|trig_approx| (|sin_term_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sin_term_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|cos_term_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|tan_ub_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|tan_lb_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sin_term_nonzero| "" (SKOSIMP*) (("" (EXPAND "sin_term") (("" (REWRITE "div_eq_zero") (("" (REWRITE "zero_times3") (("" (GENERALIZE "n!1" "n") (("" (INDUCT "n") (("1" (TYPEPRED "n!2") (("1" (PROPAX) NIL NIL)) NIL) ("2" (TYPEPRED "n!2") (("2" (PROPAX) NIL NIL)) NIL) ("3" (GROUND) NIL NIL) ("4" (SKOSIMP*) (("4" (CASE "j!1 = 0") (("1" (REPLACE -1) (("1" (HIDE -1 -2 -3) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "^") (("2" (EXPAND "expt" -2) (("2" (GROUND) (("2" (EXPAND "expt" -1) (("2" (REWRITE "zero_times3") (("2" (REWRITE "zero_times3") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (SKOSIMP*) (("5" (GROUND) NIL NIL)) NIL) ("6" (SKOSIMP*) (("6" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_term_next| "" (SKOSIMP*) (("" (EXPAND "sin_term") (("" (EXPAND "^") (("" (EXPAND "expt" + (1 2)) (("" (EXPAND "expt" + 2) (("" (EXPAND "factorial" + 1) (("" (EXPAND "factorial" + (1 2)) (("" (CASE "exists (x:int),(b:real),(k:posnat): x = expt((-1), n!1 - 1) & b = expt(a!1, 2 * n!1 - 1) & k = factorial(2 * n!1 - 1)") (("1" (SKOSIMP*) (("1" (REPLACE -1 + RL) (("1" (REPLACE -2 + RL) (("1" (REPLACE -3 + RL) (("1" (HIDE -1 -2 -3) (("1" (CASE "2 * (k!1 * n!1) + 4 * (k!1 * n!1 * n!1) = k!1 * (4 * (n!1 * n!1) + 2 * n!1)") (("1" (REPLACE -1) (("1" (CASE "x!1 * b!1 / k!1 * a!1 * a!1 = x!1 * b!1 * a!1 * a!1 / k!1") (("1" (REPLACE -1) (("1" (CASE "(x!1 * b!1 * a!1 * a!1) / (k!1 * (4 * (n!1 * n!1) + 2 * n!1)) = (x!1 * b!1 * a!1 * a!1 / k!1) / (4 * (n!1 * n!1) + 2 * n!1)") (("1" (GROUND) NIL NIL) ("2" (HIDE -1 -2 2) (("2" (REWRITE "div_div2") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INST 1 "expt((-1), n!1 - 1)" "expt(a!1, 2 * n!1 - 1)" "factorial(2 * n!1 - 1)") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_terms_alternate| "" (SKOSIMP*) (("" (REWRITE "sin_term_next") (("" (LEMMA "neg_times_lt") (("" (INST -1 "-1" "(sin_term(a!1)(n!1) * a!1 * a!1) / (4 * (n!1 * n!1) + 2 * n!1)") (("" (REPLACE -1) (("" (HIDE -1) (("" (SIMPLIFY) (("" (REWRITE "pos_div_lt") (("" (REWRITE "pos_times_lt") (("" (GROUND) (("1" (REWRITE "pos_times_lt") NIL NIL) ("2" (REWRITE "pos_times_lt") NIL NIL) ("3" (REWRITE "pos_times_lt") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_terms_decr| "" (INDUCT "n") (("1" (TYPEPRED "n!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (SKOSIMP*) (("3" (HIDE -1) (("3" (LEMMA "sin_term_next") (("3" (INST -1 "a!1" "j!1+1") (("3" (REPLACE -1) (("3" (HIDE -1) (("3" (CASE "sin_term(a!1)(j!1 + 1) * -1 * a!1 * a!1 / ((2 * (j!1 + 1) + 1) * 2 * (j!1 + 1)) = sin_term(a!1)(j!1 + 1) * -1 * ( a!1 * a!1 / ((2 * (j!1 + 1) + 1) * 2 * (j!1 + 1)))") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "abs_mult") (("1" (REWRITE "abs_mult") (("1" (CASE "2 * (abs(sin_term(a!1)(1 + j!1)) * abs(-1) * abs((a!1 * a!1 / (6 + 6 * j!1 + (4 * (j!1 * j!1) + 4 * j!1))))) = abs(sin_term(a!1)(1 + j!1)) * abs(-1) * 2 * abs((a!1 * a!1 / (6 + 6 * j!1 + (4 * (j!1 * j!1) + 4 * j!1))))") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (LEMMA "both_sides_times_pos_gt2") (("1" (INST -1 "abs(sin_term(a!1)(j!1 + 1))" "1" "abs(-1) * 2 * abs((a!1 * a!1 / (6 + 6 * j!1 + (4 * (j!1 * j!1) + 4 * j!1))))") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) (("1" (HIDE 1) (("1" (REWRITE "neg_div_lt") NIL NIL)) NIL) ("2" (HIDE 1) (("2" (TYPEPRED "PI") (("2" (EXPAND "PI_ub") (("2" (CASE "2 * a!1 * a!1 / 6 >= 2 * ((a!1 * a!1 / (6 + 4 * (j!1 * j!1) + 10 * j!1)) * --1)") (("1" (CASE "315*315/(200*200) >= a!1 * a!1") (("1" (GROUND) NIL NIL) ("2" (HIDE -1 2) (("2" (CASE "315/200 >= a!1") (("1" (LEMMA "div_mult_pos_ge1") (("1" (INST -1 "200 * 200" "a!1 * a!1" "315 * 315") (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REWRITE "div_mult_pos_ge1") (("1" (CASE "a!1 * a!1 * (200 * 200) = (200*a!1)*(200*a!1)") (("1" (REPLACE -1) (("1" (USE "ge_times_ge_pos") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (CASE "2 * a!1 * a!1 / 6 = 2 * (a!1 * a!1 / 6)") (("1" (REPLACE -1) (("1" (REWRITE "both_sides_times_pos_ge2") (("1" (CASE "((a!1 * a!1 / (6 + 4 * (j!1 * j!1) + 10 * j!1)) * --1) = a!1 * a!1 / (6 + 4 * (j!1 * j!1) + 10 * j!1)") (("1" (REPLACE -1) (("1" (REWRITE "both_sides_div_pos_ge2") NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (USE "sin_term_nonzero") (("2" (GROUND) (("2" (EXPAND "abs") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_approx_gt_term| "" (INDUCT "n") (("1" (TYPEPRED "n!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (SKOSIMP*) (("3" (EXPAND "sin_approx") (("3" (EXPAND "sigma" +) (("3" (LIFT-IF) (("3" (SPLIT 1) (("1" (HIDE -1 -2) (("1" (GROUND) (("1" (LEMMA "sin_terms_decr") (("1" (INST -1 "a!1" "1") (("1" (REPLACE -2) (("1" (GROUND) (("1" (EXPAND "abs" -1 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) (("2" (INST?) (("2" (GROUND) (("2" (USE "sin_terms_decr") (("2" (GROUND) (("2" (EXPAND "abs" -1 1) (("2" (EXPAND "abs" -2) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_approx_n_gt_0| "" (INDUCT "n") (("1" (TYPEPRED "n!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (SKOSIMP*) (("3" (CASE "j!1 = 0") (("1" (REPLACE -1) (("1" (HIDE -1 -2) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GROUND) (("2" (INST?) (("2" (LEMMA "sin_approx_gt_term") (("2" (INST -1 "a!1" "j!1") (("2" (GROUND) (("2" (EXPAND "sin_approx") (("2" (EXPAND "sigma" +) (("2" (EXPAND "abs") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_lb_gt_0| "" (SKOSIMP*) (("" (EXPAND "sin_lb") (("" (USE "sin_approx_n_gt_0") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (SIN "" (SKOLEM 1 "a") (("" (LEMMA "sin_bound") (("" (INST -1 "a" "2") (("" (EXPAND "sin_lb") (("" (EXPAND "sin_ub") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (COS "" (SKOLEM 1 "a") (("" (LEMMA "cos_bound") (("" (INST -1 "a" "1") (("" (EXPAND "cos_lb") (("" (EXPAND "cos_ub") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (TAN_TCC1 "" (SUBTYPE-TCC) NIL NIL) (TAN_TCC2 "" (SKOLEM 1 "a") (("" (GROUND) (("" (EXPAND "Tan?") (("" (LEMMA "cos_eq_0_2PI") (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (TAN_TCC3 "" (SKOLEM 1 "a") (("" (GROUND) (("" (LEMMA "COS") (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (TAN "" (SKOLEM 1 "a") (("" (GROUND) (("1" (EXPAND "tan_ub") (("1" (EXPAND "tan") (("1" (CASE "sin_ub(a) / cos_lb(a) >= sin(a)/cos_lb(a)") (("1" (CASE "sin(a)/cos_lb(a) >= sin(a)/cos(a)") (("1" (GROUND) NIL NIL) ("2" (HIDE -1 2) (("2" (CASE-REPLACE "sin(a)=0") (("1" (GROUND) NIL NIL) ("2" (LEMMA "both_sides_div_pos_ge2") (("2" (INST?) (("1" (GROUND) (("1" (LEMMA "COS") (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sin_lb_gt_0") (("2" (INST?) (("2" (ASSERT) (("2" (CASE-REPLACE "a = 0") (("1" (REWRITE "sin_0") NIL NIL) ("2" (ASSERT) (("2" (LEMMA "SIN") (("2" (INST?) (("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2 3) (("3" (LEMMA "cos_eq_0_2PI") (("3" (INST?) (("3" (GROUND) (("1" (CASE-REPLACE "a = 0") (("1" (REWRITE "cos_0") (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (LEMMA "COS") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "COS") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LEMMA "cos_eq_0_2PI") (("3" (INST?) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "both_sides_div_pos_ge1") (("2" (INST?) (("2" (GROUND) (("2" (LEMMA "SIN") (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "tan_lb") (("2" (EXPAND "tan") (("2" (CASE "sin_lb(a) / cos_ub(a) <= sin(a) / cos_ub(a)" "sin(a) / cos_ub(a) <= sin(a) / cos(a)") (("1" (GROUND) NIL NIL) ("2" (HIDE -1 2) (("2" (CASE-REPLACE "sin(a)=0") (("1" (GROUND) NIL NIL) ("2" (CASE-REPLACE "a = 0") (("1" (REWRITE "sin_0") NIL NIL) ("2" (CASE "sin(a) > 0") (("1" (LEMMA "both_sides_div_pos_le2") (("1" (INST?) (("1" (GROUND) (("1" (LEMMA "COS") (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (LEMMA "COS") (("3" (INST?) (("3" (GROUND) NIL NIL)) NIL)) NIL) ("4" (HIDE 2 3) (("4" (LEMMA "COS") (("4" (INST?) (("4" (ASSERT) (("4" (FLATTEN) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sin_lb_gt_0") (("2" (INST?) (("2" (ASSERT) (("2" (LEMMA "SIN") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (LEMMA "both_sides_div_pos_le1") (("3" (INST?) (("1" (GROUND) (("1" (LEMMA "SIN") (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "COS") (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "cos_eq_0_2PI") (("4" (INST?) (("4" (GROUND) NIL NIL)) NIL)) NIL) ("5" (LEMMA "COS") (("5" (INST?) (("5" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$trig_ineq.pvs trig_ineq : THEORY %----------------------------------------------------------------------------- % trig_ineq % --------- % - regions where functions are greater than 0 % - regions where functions are less than 0 % - regions where functions are increasing % - regions where functions are decreasing %----------------------------------------------------------------------------- BEGIN IMPORTING trig_approx a,b : VAR real % ------------------- Sign of sin, cos, and tan ----------------------- sin_gt_0 : LEMMA 0 < a AND a < PI IMPLIES sin(a) > 0 cos_gt_0 : LEMMA -PI/2 < a AND a < PI/2 IMPLIES cos(a) > 0 sin_ge_0 : LEMMA 0 <= a AND a <= PI IMPLIES sin(a) >= 0 cos_ge_0 : LEMMA -PI/2 <= a AND a <= PI/2 IMPLIES cos(a) >= 0 sin_le_0 : LEMMA PI <= a AND a <= 2*PI IMPLIES sin(a) <= 0 cos_le_0 : LEMMA PI/2 <= a AND a <= 3*PI/2 IMPLIES cos(a) <= 0 sin_lt_0 : LEMMA PI < a AND a < 2*PI IMPLIES sin(a) < 0 cos_lt_0 : LEMMA PI/2 < a AND a < 3*PI/2 IMPLIES cos(a) < 0 tan_gt_0 : LEMMA 0 < a AND a < PI/2 IMPLIES tan(a) > 0 tan_lt_0 : LEMMA -PI/2 < a AND a < 0 IMPLIES tan(a) < 0 cos_ge_0_3PI2 : LEMMA 3*PI/2 <= a AND a <= 2*PI IMPLIES cos(a) >= 0 % -------------------- Strict Inequalities -------------------- sin_increasing_imp : LEMMA a <= PI/2 AND a >= -PI/2 AND b <= PI/2 AND b >= -PI/2 AND a > b => sin(a) > sin(b) sin_increasing : LEMMA a <= PI/2 AND a >= -PI/2 AND b <= PI/2 AND b >= -PI/2 IMPLIES (sin(a) > sin(b) <=> a > b) sin_decreasing : LEMMA a <= 3*PI/2 AND a >= PI/2 AND b <= 3*PI/2 AND b >= PI/2 IMPLIES (sin(b) > sin(a) <=> a > b) cos_increasing : LEMMA a >= PI AND a <= 2*PI AND b >= PI AND b <= 2*PI IMPLIES (cos(a) > cos(b) <=> a > b) cos_decreasing : LEMMA a <= PI AND a >= 0 AND b <= PI AND b >= 0 IMPLIES (cos(b) > cos(a) <=> a > b) tan_PI4_def : LEMMA -PI/4 <= a AND a <= PI/4 IMPLIES Tan?(a) tan_increasing_imp: LEMMA -PI/4 <= a AND a <= PI/4 AND -PI/4 <= b AND b <= PI/4 AND a > b IMPLIES tan(a) > tan(b) tan_increasing : LEMMA -PI/4 <= a AND a <= PI/4 AND -PI/4 <= b AND b <= PI/4 IMPLIES (tan(a) > tan(b) <=> a > b) % -------------------- Non-Strict Inequalities -------------------- sin_incr : LEMMA a <= PI/2 AND a >= -PI/2 AND b <= PI/2 AND b >= -PI/2 IMPLIES (sin(a) >= sin(b) <=> a >= b) sin_decr : LEMMA a <= 3*PI/2 AND a >= PI/2 AND b <= 3*PI/2 AND b >= PI/2 IMPLIES (sin(b) >= sin(a) <=> a >= b) cos_incr : LEMMA a >= PI AND a <= 2*PI AND b >= PI AND b <= 2*PI IMPLIES (cos(a) >= cos(b) <=> a >= b) cos_decr : LEMMA a <= PI AND a >= 0 AND b <= PI AND b >= 0 IMPLIES (cos(b) >= cos(a) <=> a >= b) tan_incr : LEMMA -PI/4 <= a AND a <= PI/4 AND -PI/4 <= b AND b <= PI/4 IMPLIES (tan(a) >= tan(b) <=> a >= b) END trig_ineq $$$trig_ineq.prf (|trig_ineq| (|sin_gt_0| "" (SKOSIMP) (("" (CASE "a!1<=PI/2") (("1" (CASE "EXISTS (d: real): sin(a!1) >= d AND d > 0") (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (INST 1 "sin_lb(a!1)") (("2" (SPLIT) (("1" (LEMMA "SIN") (("1" (INST -1 "a!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "sin_lb_gt_0") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sin_minus") (("2" (INST -1 "PI" "a!1") (("2" (REWRITE "sin_PI") (("2" (REWRITE "cos_PI") (("2" (ASSERT) (("2" (REPLACE -1 * RL) (("2" (HIDE -1) (("2" (CASE-REPLACE "EXISTS (d: real): sin(PI - a!1) >= d AND d > 0") (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 3) (("2" (INST + "sin_lb(PI-a!1)") (("2" (LEMMA "SIN") (("2" (INST -1 "a!1") (("2" (ASSERT) (("2" (FLATTEN) (("2" (SPLIT) (("1" (ASSERT) (("1" (HIDE -2 -1) (("1" (LEMMA "SIN") (("1" (INST -1 "PI-a!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2 -1) (("2" (REWRITE "sin_lb_gt_0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_gt_0| "" (SKOSIMP) (("" (LEMMA "sin_shift") (("" (INST -1 "a!1") (("" (REPLACE -1 * RL) (("" (HIDE -1) (("" (REWRITE "sin_gt_0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_ge_0| "" (SKOSIMP) (("" (CASE "a!1=0") (("1" (REPLACE -1 * LR) (("1" (REWRITE "sin_0") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "a!1=PI") (("1" (REPLACE -1 * LR) (("1" (REWRITE "sin_PI") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "sin_gt_0") (("2" (INST -1 "a!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_ge_0| "" (SKOSIMP) (("" (CASE "a!1=-PI/2") (("1" (REPLACE -1 * LR) (("1" (LEMMA "cos_neg") (("1" (INST -1 "PI/2") (("1" (ASSERT) (("1" (REPLACE -1 * LR) (("1" (REWRITE "cos_PI2") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "a!1=PI/2") (("1" (REPLACE -1 * LR) (("1" (REWRITE "cos_PI2") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "cos_gt_0") (("2" (INST -1 "a!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_le_0| "" (SKOSIMP) (("" (LEMMA "sin_ge_0") (("" (INST -1 "a!1-PI") (("" (REWRITE "sin_minus") (("" (REWRITE "sin_PI") (("" (REWRITE "cos_PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_le_0| "" (SKOSIMP) (("" (LEMMA "cos_ge_0") (("" (INST -1 "a!1-PI") (("" (REWRITE "cos_minus") (("" (REWRITE "cos_PI") (("" (REWRITE "sin_PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_lt_0| "" (SKOSIMP*) (("" (LEMMA "sin_le_0") (("" (INST?) (("" (ASSERT) (("" (CASE-REPLACE "sin(a!1) = 0") (("1" (HIDE -2 1) (("1" (REWRITE "sin_eq_0") (("1" (SKOSIMP*) (("1" (REPLACE -) (("1" (HIDE -1) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE -3) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "PI" "1" "i!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_lt_0| "" (SKOSIMP*) (("" (LEMMA "cos_le_0") (("" (INST?) (("" (ASSERT) (("" (CASE-REPLACE "cos(a!1) = 0") (("1" (HIDE -2 1) (("1" (LEMMA "cos_eq_0") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE -2) (("1" (SKOSIMP*) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE-REPLACE "0 < i!1 * PI") (("1" (HIDE -2) (("1" (CASE "i!1 * PI < PI ") (("1" (HIDE -3) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "PI" "i!1" "1") (("1" (ASSERT) (("1" (HIDE -2) (("1" (LEMMA "both_sides_times_pos_lt1") (("1" (INST -1 "PI" "0" "i!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|tan_gt_0_TCC1| "" (SKOSIMP) (("" (EXPAND "Tan?") (("" (LEMMA "cos_gt_0") (("" (INST -1 "a!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_gt_0| "" (SKOSIMP) (("" (EXPAND "tan") (("" (LEMMA "cos_gt_0") (("" (INST -1 "a!1") (("" (ASSERT) (("" (REWRITE "pos_div_gt" 1) (("" (REWRITE "sin_gt_0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|tan_lt_0_TCC1| "" (SKOSIMP*) (("" (EXPAND "Tan?") (("" (LEMMA "cos_gt_0") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_lt_0| "" (SKOSIMP) (("" (EXPAND "tan") (("" (LEMMA "cos_gt_0") (("" (INST -1 "a!1") (("" (ASSERT) (("" (LEMMA "sin_period") (("" (INST?) (("" (INST -1 "1") (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "sin_lt_0") (("" (INST?) (("" (ASSERT) (("" (LEMMA "neg_div_lt") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_ge_0_3PI2| "" (SKOSIMP*) (("" (NAME "BB" "a!1 - 2 * PI") (("" (CASE-REPLACE "a!1 = BB + 2*PI") (("1" (HIDE -1 -2) (("1" (ASSERT) (("1" (CASE-REPLACE "-PI/2 <= BB AND BB <= 0") (("1" (HIDE -2 -3) (("1" (REWRITE "cos_plus") (("1" (REWRITE "cos_2PI") (("1" (REWRITE "sin_2PI") (("1" (FLATTEN) (("1" (ASSERT) (("1" (LEMMA "cos_gt_0") (("1" (INST?) (("1" (LEMMA "cos_PI2") (("1" (LEMMA "cos_neg") (("1" (INST -1 "PI/2") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sin_increasing_imp| "" (SKOSIMP) (("" (CASE "sin(a!1) - sin(b!1) > 0") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2) (("2" (ASSERT) (("2" (LEMMA "sin_plus") (("2" (INST -1 "(a!1+b!1)/2" "(a!1-b!1)/2") (("2" (LEMMA "sin_minus") (("2" (INST -1 "(a!1+b!1)/2" "(a!1-b!1)/2") (("2" (REPLACE -2 * LR) (("2" (REPLACE -1 * LR) (("2" (HIDE -2 -1) (("2" (ASSERT) (("2" (ASSERT) (("2" (LEMMA "pos_times_gt") (("2" (INST -1 "2" "sin((a!1 - b!1) / 2) * cos((a!1 + b!1) / 2)") (("2" (REPLACE -1 * LR) (("2" (HIDE -1) (("2" (FLATTEN) (("2" (HIDE 1) (("2" (REWRITE "pos_times_gt" 1) (("2" (ASSERT) (("2" (FLATTEN) (("2" (HIDE 1) (("2" (REWRITE "sin_gt_0") (("2" (REWRITE "cos_gt_0") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_increasing| "" (SKOSIMP) (("" (PROP) (("1" (LEMMA "sin_increasing_imp") (("1" (INST -1 "b!1" "a!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "sin_increasing_imp") NIL NIL)) NIL)) NIL) (|sin_decreasing| "" (LEMMA "sin_increasing") (("" (SKOSIMP) (("" (INST -1 "PI-b!1" "PI-a!1") (("" (REWRITE "sin_minus") (("" (REWRITE "sin_PI") (("" (REWRITE "cos_PI") (("" (REWRITE "sin_minus") (("" (REWRITE "sin_PI") (("" (REWRITE "cos_PI") (("" (ASSERT) (("" (CASE-REPLACE "-1 * (sin(b!1) * -1) = sin(b!1)") (("1" (HIDE -1) (("1" (CASE-REPLACE "-1 * (sin(a!1) * -1) = sin(a!1)") (("1" (HIDE -1) (("1" (GROUND) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_increasing| "" (SKOSIMP) (("" (LEMMA "sin_increasing") (("" (INST -1 "a!1-3*PI/2" "b!1-3*PI/2") (("" (ASSERT) (("" (REWRITE "sin_minus") (("" (REWRITE "cos_3PI2") (("" (REWRITE "sin_3PI2") (("" (REWRITE "sin_minus") (("" (REWRITE "cos_3PI2") (("" (REWRITE "sin_3PI2") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_decreasing| "" (SKOSIMP) (("" (LEMMA "sin_increasing") (("" (INST -1 "a!1-PI/2" "b!1-PI/2") (("" (ASSERT) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_PI2") (("" (REWRITE "cos_PI2") (("" (ASSERT) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_PI2") (("" (REWRITE "cos_PI2") (("" (ASSERT) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|tan_PI4_def| "" (SKOSIMP) (("" (EXPAND "Tan?") (("" (LEMMA "cos_gt_0") (("" (INST -1 "a!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_increasing_imp_TCC1| "" (SKOSIMP) (("" (REWRITE "tan_PI4_def") NIL NIL)) NIL) (|tan_increasing_imp_TCC2| "" (SKOSIMP) (("" (REWRITE "tan_PI4_def") NIL NIL)) NIL) (|tan_increasing_imp| "" (SKOSIMP) (("" (EXPAND "tan") (("" (LEMMA "cos_gt_0") (("" (INST -1 "a!1") (("" (LEMMA "cos_gt_0") (("" (INST -1 "b!1") (("" (ASSERT) (("" (CASE "a!1>0" "b!1<0") (("1" (CASE "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)") (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (INST 1 "0") (("2" (REWRITE "pos_div_gt" 1) (("2" (REWRITE "sin_gt_0") (("2" (REWRITE "neg_div_ge" 1) (("2" (LEMMA "sin_gt_0") (("2" (INST -1 "-b!1") (("2" (REWRITE "sin_neg" -1) (("2" (CASE "0 < -b!1 AND -b!1 < PI IMPLIES sin(b!1) < 0") (("1" (HIDE -2) (("1" (ASSERT) NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)") (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 3) (("2" (INST + "sin(b!1)/cos(a!1)") (("2" (SPLIT) (("1" (LEMMA "both_sides_div_pos_lt1") (("1" (INST -1 "cos(a!1)" "sin(b!1)" "sin(a!1)") (("1" (ASSERT) (("1" (LEMMA "sin_increasing") (("1" (INST -1 "a!1" "b!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "(sin(b!1) = 0 OR sin(b!1) > 0 AND cos(a!1) <= cos(b!1) OR sin(b!1) < 0 AND cos(a!1) >= cos(b!1))") (("1" (ASSERT) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (LEMMA "both_sides_div_pos_le2") (("1" (INST -1 "cos(b!1)" "cos(a!1)" "sin(b!1)") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (LEMMA "both_sides_div_pos_le3") (("2" (INST -1 "sin(b!1)" "cos(b!1)" "cos(a!1)") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "cos_decreasing") (("2" (INST -1 "a!1" "b!1") (("2" (ASSERT) (("2" (LEMMA "sin_ge_0") (("2" (INST -1 "b!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (CASE "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)") (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 3) (("2" (INST + "sin(b!1)/cos(a!1)") (("2" (SPLIT) (("1" (LEMMA "both_sides_div_pos_gt1") (("1" (INST -1 "cos(a!1)" "sin(a!1)" "sin(b!1)") (("1" (ASSERT) (("1" (HIDE 2) (("1" (REWRITE "sin_increasing") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "(sin(b!1) = 0 OR sin(b!1) > 0 AND cos(a!1) <= cos(b!1) OR sin(b!1) < 0 AND cos(a!1) >= cos(b!1))") (("1" (ASSERT) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (LEMMA "both_sides_div_pos_le2") (("1" (INST -1 "cos(b!1)" "cos(a!1)" "sin(b!1)") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "both_sides_div_pos_le3") (("2" (INST -1 "sin(b!1)" "cos(b!1)" "cos(a!1)") (("1" (ASSERT) NIL NIL) ("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "sin_gt_0") (("2" (INST -1 "-b!1") (("2" (REWRITE "sin_neg" -1) (("2" (CASE "0 < -b!1 AND -b!1 < PI IMPLIES sin(b!1) < 0") (("1" (HIDE -2) (("1" (ASSERT) (("1" (LEMMA "cos_decreasing") (("1" (INST -1 "-b!1" "-a!1") (("1" (REWRITE "cos_neg" -1) (("1" (REWRITE "cos_neg" -1) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|tan_increasing_TCC1| "" (SKOSIMP) (("" (REWRITE "tan_PI4_def") NIL NIL)) NIL) (|tan_increasing_TCC2| "" (SKOSIMP*) (("" (REWRITE "tan_PI4_def") NIL NIL)) NIL) (|tan_increasing| "" (SKOSIMP) (("" (ASSERT) (("" (PROP) (("1" (CASE "a!1=b!1") (("1" (REPLACE -1 * LR) (("1" (ASSERT) NIL NIL)) NIL) ("2" (LEMMA "trich_gt") (("2" (INST -1 "a!1" "b!1") (("2" (REPLACE 1 * LR) (("2" (PROP) (("2" (LEMMA "tan_increasing_imp") (("2" (INST -1 "b!1" "a!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "tan_increasing_imp") NIL NIL)) NIL)) NIL)) NIL) (|sin_incr| "" (SKOSIMP*) (("" (CASE-REPLACE "a!1=b!1") (("1" (GROUND) NIL NIL) ("2" (LEMMA "sin_increasing") (("2" (INST-CP -1 "b!1" "a!1") (("2" (INST -1 "a!1" "b!1") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_decr| "" (SKOSIMP*) (("" (LEMMA "sin_decreasing") (("" (INST -1 "a!1" "b!1") (("" (ASSERT) (("" (LEMMA "sin_decreasing") (("" (INST -1 "b!1" "a!1") (("" (ASSERT) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_incr| "" (SKOSIMP*) (("" (LEMMA "cos_increasing") (("" (INST-CP -1 "b!1" "a!1") (("" (INST -1 "a!1" "b!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_decr| "" (SKOSIMP*) (("" (LEMMA "cos_decreasing") (("" (INST-CP -1 "b!1" "a!1") (("" (INST -1 "a!1" "b!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_incr| "" (SKOSIMP*) (("" (LEMMA "tan_increasing") (("" (INST-CP -1 "b!1" "a!1") (("" (INST -1 "a!1" "b!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$trig_extra.pvs trig_extra : THEORY %----------------------------------------------------------------------------- % trig_extra % ---------- % - reduction theorems % - sum and product identities % - half-angle identities and zeros % - triple angle formulas %----------------------------------------------------------------------------- BEGIN IMPORTING trig_basic a,b : VAR real % ------------------------- Reduction Theorems ------------------------- sin_minus_2PI : LEMMA sin(a - 2*PI) = sin(a) cos_minus_2PI : LEMMA cos(a - 2*PI) = cos(a) tan_minus_2PI : LEMMA cos(a) /= 0 IMPLIES tan(a - 2*PI) = tan(a) sin_minus_3PI2 : LEMMA sin(a - 3*PI/2) = cos(a) cos_minus_3PI2 : LEMMA cos(a - 3*PI/2) = - sin(a) tan_minus_3PI2 : LEMMA sin(a) /= 0 AND cos(a) /= 0 IMPLIES tan(a - 3*PI/2) = - 1/tan(a) sin_minus_PI : LEMMA sin(a - PI) = - sin(a) cos_minus_PI : LEMMA cos(a - PI) = - cos(a) tan_minus_PI : LEMMA cos(a) /= 0 IMPLIES tan(a - PI) = tan(a) sin_minus_PI2 : LEMMA sin(a - PI/2) = - cos(a) cos_minus_PI2 : LEMMA cos(a - PI/2) = sin(a) tan_minus_PI2 : LEMMA sin(a) /= 0 AND cos(a) /= 0 IMPLIES tan(a - PI/2) = - 1/tan(a) sin_2PI_minus : LEMMA sin(2*PI - a) = - sin(a) cos_2PI_minus : LEMMA cos(2*PI - a) = cos(a) tan_2PI_minus : LEMMA sin(a) /= 0 AND cos(a) /= 0 IMPLIES tan(2*PI - a) = - tan(a) sin_3PI2_minus : LEMMA sin(3*PI/2 - a) = - cos(a) cos_3PI2_minus : LEMMA cos(3*PI/2 - a) = - sin(a) tan_3PI2_minus : LEMMA sin(a) /= 0 AND cos(a) /= 0 IMPLIES tan(3*PI/2 - a) = 1/tan(a) sin_PI_minus : LEMMA sin(PI - a) = sin(a) cos_PI_minus : LEMMA cos(PI - a) = - cos(a) tan_PI_minus : LEMMA cos(a) /= 0 IMPLIES tan(PI - a) = - tan(a) sin_PI2_minus : LEMMA sin(PI/2 - a) = cos(a) cos_PI2_minus : LEMMA cos(PI/2 - a) = sin(a) tan_PI2_minus : LEMMA sin(a) /= 0 AND cos(a) /= 0 IMPLIES tan(PI/2 - a) = 1/tan(a) % ------------------------- Sum and Product Formulas ------------------------- sin_times_cos : LEMMA sin(a)*cos(b) = (sin(a+b) + sin(a-b))/2 cos_times_cos : LEMMA cos(a)*cos(b) = (cos(a+b) + cos(a-b))/2 sin_times_sin : LEMMA sin(a)*sin(b) = (cos(a-b) - cos(a+b))/2 sin_sum : LEMMA sin(a) + sin(b) = 2 * sin((a+b)/2)*cos((a-b)/2) sin_diff : LEMMA sin(a) - sin(b) = 2 * cos((a+b)/2)*sin((a-b)/2) cos_sum : LEMMA cos(a) + cos(b) = 2 * cos((a+b)/2)*cos((a-b)/2) cos_diff : LEMMA cos(a) - cos(b) = - 2 * sin((a+b)/2)*sin((a-b)/2) tan_diff : LEMMA Tan?(a) AND Tan?(b) IMPLIES tan(a) - tan(b) = sin(a-b)/(cos(a)*cos(b)) % ------------------------- Squares of sin and cos ------------------------- sq_sin : LEMMA sq(sin(a)) = (1-cos(2*a))/2 sq_cos : LEMMA sq(cos(a)) = (1+cos(2*a))/2 sin_half_zeroes : LEMMA sin(a/2) = 0 IFF 1-cos(a) = 0 cos_half_zeroes : LEMMA cos(a/2) = 0 IFF 1+cos(a) = 0 cos_half_zeroes2 : LEMMA cos(a/2) = 0 IMPLIES sin(a) = 0 sq_tan : LEMMA (1+cos(2*a)) /= 0 IMPLIES sq(tan(a)) = (1-cos(2*a))/(1+cos(2*a)) % ------------------------- Half Angle Formulas ------------------------- IMPORTING trig_ineq sin_half : LEMMA ( 0 <= a/2 AND a/2 <= PI IMPLIES sin(a/2) = sqrt((1-cos(a))/2)) AND ( PI <= a/2 AND a/2 <= 2*PI IMPLIES sin(a/2) = -sqrt((1-cos(a))/2)) cos_half : LEMMA ( 0 <= a/2 AND a/2 <= PI/2 IMPLIES cos(a/2) = sqrt((1+cos(a))/2)) AND ( PI/2 <= a/2 AND a/2 <= 3*PI/2 IMPLIES cos(a/2) = -sqrt((1+cos(a))/2)) AND ( 3*PI/2 <= a/2 AND a/2 <= 2*PI IMPLIES cos(a/2) = sqrt((1+cos(a))/2)) tan_half : LEMMA cos(a) /= -1 IMPLIES tan(a/2) = sin(a)/(1 + cos(a)) tan_half2 : LEMMA sin(a) /= 0 IMPLIES tan(a/2) = (1 - cos(a))/sin(a) % ---------------------- Triple Angle Formulas ---------------------- sin_3a : LEMMA sin(3*a) = 3 * sin(a) - 4 * expt(sin(a),3) cos_3a : LEMMA cos(3*a) = 4 * expt(cos(a),3) - 3 * cos(a) % ---------------------- Base equations --------------------- sin_eq_sin : LEMMA sin(a) = sin(b) <=> (EXISTS (k: int): (a = b + 2*k*PI) OR (a = PI - b + 2*k*PI)) cos_eq_cos : LEMMA cos(a) = cos(b) <=> (EXISTS (k: int): (a = b + 2*k*PI) OR (a = -b + 2*k*PI)) tan_eq_tan : LEMMA Tan?(a) AND Tan?(b) IMPLIES ( tan(a) = tan(b) <=> (EXISTS (k: int): (a = b + k*PI)) ) i,j: VAR integer sin_eq_pm1 : LEMMA sin(a) = (-1)^i IFF (EXISTS j: a = (i+2*j)*PI + PI/2) cos_eq_pm1 : LEMMA cos(a) = (-1)^i IFF (EXISTS j: a = (i+2*j)*PI) END trig_extra $$$trig_extra.prf (|trig_extra| (|sin_minus_2PI| "" (SKOSIMP) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_2PI") (("" (REWRITE "cos_2PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_minus_2PI| "" (SKOSIMP) (("" (REWRITE "cos_minus") (("" (REWRITE "cos_2PI") (("" (REWRITE "sin_2PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_minus_2PI_TCC1| "" (SKOSIMP) (("" (EXPAND "Tan?") (("" (REWRITE "cos_minus_2PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|tan_minus_2PI_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|tan_minus_2PI| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sin_minus_2PI") (("" (REWRITE "cos_minus_2PI") NIL NIL)) NIL)) NIL)) NIL) (|sin_minus_3PI2| "" (SKOSIMP) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_3PI2") (("" (REWRITE "cos_3PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_minus_3PI2| "" (SKOSIMP) (("" (REWRITE "cos_minus") (("" (REWRITE "cos_3PI2") (("" (REWRITE "sin_3PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_minus_3PI2_TCC1| "" (SUBTYPE-TCC) (("" (REWRITE "cos_minus_3PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|tan_minus_3PI2_TCC2| "" (SKOSIMP) (("" (EXPAND "tan") (("" (LEMMA "div_eq_zero") (("" (INST -1 "cos(a!1)" "sin(a!1)") (("1" (REPLACE -1 * LR) (("1" (PROPAX) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_minus_3PI2| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sin_minus_3PI2") (("" (REWRITE "cos_minus_3PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sin_minus_PI| "" (SKOSIMP) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_PI") (("" (REWRITE "cos_PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_minus_PI| "" (SKOSIMP) (("" (REWRITE "cos_minus") (("" (REWRITE "cos_PI") (("" (REWRITE "sin_PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_minus_PI_TCC1| "" (SUBTYPE-TCC) (("" (REWRITE "cos_minus_PI") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|tan_minus_PI| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sin_minus_PI") (("" (REWRITE "cos_minus_PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sin_minus_PI2| "" (SKOSIMP) (("" (REWRITE "sin_minus") (("" (REWRITE "cos_PI2") (("" (REWRITE "sin_PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_minus_PI2| "" (SKOSIMP) (("" (REWRITE "cos_minus") (("" (REWRITE "cos_PI2") (("" (REWRITE "sin_PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_minus_PI2_TCC1| "" (SUBTYPE-TCC) (("" (REWRITE "cos_minus_PI2") NIL NIL)) NIL) (|tan_minus_PI2| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sin_minus_PI2") (("" (REWRITE "cos_minus_PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sin_2PI_minus| "" (SKOSIMP) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_2PI") (("" (REWRITE "cos_2PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_2PI_minus| "" (SKOSIMP) (("" (REWRITE "cos_minus") (("" (REWRITE "cos_2PI") (("" (REWRITE "sin_2PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_2PI_minus_TCC1| "" (SKOSIMP) (("" (EXPAND "Tan?") (("" (REWRITE "cos_2PI_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|tan_2PI_minus| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sin_2PI_minus") (("" (REWRITE "cos_2PI_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sin_3PI2_minus| "" (SKOSIMP) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_3PI2") (("" (REWRITE "cos_3PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_3PI2_minus| "" (SKOSIMP) (("" (REWRITE "cos_minus") (("" (REWRITE "cos_3PI2") (("" (REWRITE "sin_3PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_3PI2_minus_TCC1| "" (SUBTYPE-TCC) (("" (REWRITE "cos_3PI2_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|tan_3PI2_minus| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sin_3PI2_minus") (("" (REWRITE "cos_3PI2_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sin_PI_minus| "" (SKOSIMP) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_PI") (("" (REWRITE "cos_PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_PI_minus| "" (SKOSIMP) (("" (REWRITE "cos_minus") (("" (REWRITE "cos_PI") (("" (REWRITE "sin_PI") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_PI_minus_TCC1| "" (SUBTYPE-TCC) (("" (REWRITE "cos_PI_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|tan_PI_minus| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sin_PI_minus") (("" (REWRITE "cos_PI_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sin_PI2_minus| "" (SKOSIMP) (("" (REWRITE "sin_minus") (("" (REWRITE "sin_PI2") (("" (REWRITE "cos_PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_PI2_minus| "" (SKOSIMP) (("" (REWRITE "cos_minus") (("" (REWRITE "cos_PI2") (("" (REWRITE "sin_PI2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_PI2_minus_TCC1| "" (SUBTYPE-TCC) (("" (REWRITE "cos_PI2_minus") NIL NIL)) NIL) (|tan_PI2_minus| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sin_PI2_minus") (("" (REWRITE "cos_PI2_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sin_times_cos| "" (SKOSIMP) (("" (REWRITE "sin_plus") (("" (REWRITE "sin_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|cos_times_cos| "" (SKOSIMP) (("" (REWRITE "cos_plus") (("" (REWRITE "cos_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sin_times_sin| "" (SKOSIMP) (("" (REWRITE "cos_plus") (("" (REWRITE "cos_minus") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sin_sum| "" (SKOSIMP*) (("" (NAME "A" "(a!1+b!1)/2") (("" (NAME "B" "(a!1-b!1)/2") (("" (REPLACE -1) (("" (REPLACE -2) (("" (CASE "a!1= A+B") (("1" (CASE "b!1= A-B") (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (HIDE -1 -2) (("1" (REWRITE "sin_plus") (("1" (REWRITE "sin_minus") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_diff| "" (SKOSIMP*) (("" (NAME "A" "(a!1+b!1)/2") (("" (NAME "B" "(a!1-b!1)/2") (("" (REPLACE -1) (("" (REPLACE -2) (("" (CASE "a!1= A+B") (("1" (CASE "b!1= A-B") (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (HIDE -1 -2) (("1" (REWRITE "sin_plus") (("1" (REWRITE "sin_minus") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_sum| "" (SKOSIMP*) (("" (NAME "A" "(a!1+b!1)/2") (("" (NAME "B" "(a!1-b!1)/2") (("" (REPLACE -1) (("" (REPLACE -2) (("" (CASE "a!1= A+B") (("1" (CASE "b!1= A-B") (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (HIDE -1 -2) (("1" (REWRITE "cos_plus") (("1" (REWRITE "cos_minus") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_diff| "" (SKOSIMP*) (("" (NAME "A" "(a!1+b!1)/2") (("" (NAME "B" "(a!1-b!1)/2") (("" (REPLACE -1) (("" (REPLACE -2) (("" (CASE "a!1= A+B") (("1" (CASE "b!1= A-B") (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (REPLACE -1 +) (("1" (HIDE -1) (("1" (HIDE -1 -2) (("1" (REWRITE "cos_plus") (("1" (REWRITE "cos_minus") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|tan_diff_TCC1| "" (SKOSIMP*) (("" (EXPAND "Tan?") (("" (REWRITE "zero_times3") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|tan_diff| "" (SKOSIMP*) (("" (EXPAND "tan") (("" (CASE "(sin(a!1) / cos(a!1) - sin(b!1) / cos(b!1) = sin(a!1 - b!1) / (cos(a!1) * cos(b!1))) = (sin(a!1 - b!1) / (cos(a!1) * cos (b!1)) = sin(a!1) / cos(a!1) - sin(b!1) / cos(b!1))") (("1" (REPLACE -1 1 :HIDE? T) (("1" (REWRITE "div_cancel3" 1) (("1" (REWRITE "times_div1" 1) (("1" (CASE-REPLACE "(cos(a!1) * cos(b!1) * sin(a!1)) / cos(a!1) = cos(b!1) * sin(a!1)") (("1" (CASE-REPLACE "cos(a!1) * cos(b!1) * (sin(b!1) / cos(b!1)) = cos(a!1) * sin(b!1)") (("1" (HIDE -1 -2) (("1" (REWRITE "sin_minus") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL) ("3" (ASSERT) (("3" (ASSERT) (("3" (HIDE 2) (("3" (EXPAND "Tan?") (("3" (LEMMA "zero_times3") (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (ASSERT) (("4" (ASSERT) (("4" (EXPAND "Tan?") (("4" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("5" (ASSERT) (("5" (ASSERT) (("5" (EXPAND "Tan?") (("5" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sq_sin| "" (SKOSIMP) (("" (LEMMA "sin2_cos2") (("" (INST -1 "a!1") (("" (REPLACE -1 * RL) (("" (HIDE -1) (("" (LEMMA "cos_plus") (("" (INST -1 "a!1" "a!1") (("" (REPLACE -1 * LR) (("" (HIDE -1) (("" (EXPAND "sq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sq_cos| "" (SKOSIMP) (("" (LEMMA "sin2_cos2") (("" (INST -1 "a!1") (("" (REPLACE -1 * RL) (("" (HIDE -1) (("" (LEMMA "cos_plus") (("" (INST -1 "a!1" "a!1") (("" (REPLACE -1 * LR) (("" (HIDE -1) (("" (EXPAND "sq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_half_zeroes| "" (SKOSIMP) (("" (PROP) (("1" (LEMMA "sq_sin") (("1" (INST -1 "a!1/2") (("1" (REPLACE -2 * LR) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sq_sin") (("2" (INST -1 "a!1/2") (("2" (REPLACE -2 * LR) (("2" (ASSERT) (("2" (LEMMA "sq_eq_0") (("2" (INST -1 "sin(a!1/2)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_half_zeroes| "" (SKOSIMP) (("" (PROP) (("1" (LEMMA "sq_cos") (("1" (INST -1 "a!1/2") (("1" (REPLACE -2 * LR) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sq_cos") (("2" (INST -1 "a!1/2") (("2" (REPLACE -2 * LR) (("2" (LEMMA "sq_eq_0") (("2" (INST -1 "cos(a!1/2)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cos_half_zeroes2| "" (SKOSIMP) (("" (LEMMA "sin_plus") (("" (INST -1 "a!1/2" "a!1/2") (("" (REPLACE -2 * LR) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sq_tan_TCC1| "" (SKOSIMP) (("" (EXPAND "Tan?") (("" (PROP) (("" (REWRITE "cos_half_zeroes" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sq_tan| "" (SKOSIMP) (("" (EXPAND "tan") (("" (REWRITE "sq_div") (("1" (REWRITE "sq_sin") (("1" (REWRITE "sq_cos") (("1" (ASSERT) (("1" (REWRITE "div_div2") (("1" (REWRITE "div_cancel1") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (LEMMA "sq_cos") (("2" (INST -1 "a!1") (("2" (PROP) (("2" (REPLACE -2 * LR) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sin_half_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sin_half_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|sin_half| "" (SKOSIMP*) (("" (LEMMA "cos_2a_sin") (("" (INST -1 "a!1/2") (("" (CASE-REPLACE "2 * (a!1 / 2) = a!1") (("1" (HIDE -1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (CASE-REPLACE "(2 * (sin(a!1 / 2) * sin(a!1 / 2)) / 2) = sq(sin(a!1/2))") (("1" (HIDE -1) (("1" (PROP) (("1" (REWRITE "sqrt_sq") (("1" (HIDE 2) (("1" (REWRITE "sin_ge_0") NIL NIL)) NIL)) NIL) ("2" (REWRITE "sqrt_sq_abs") (("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (GROUND) (("2" (LEMMA "sin_le_0") (("2" (INST -1 "a!1/2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cos_half_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|cos_half_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|cos_half_TCC3| "" (SUBTYPE-TCC) NIL NIL) (|cos_half| "" (SKOSIMP*) (("" (LEMMA "cos_2a_sin") (("" (INST -1 "a!1/2") (("" (CASE-REPLACE "2 * (a!1 / 2) = a!1") (("1" (HIDE -1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (CASE-REPLACE "sin(a!1 / 2) * sin(a!1 / 2) = sq(sin(a!1/2))") (("1" (CASE-REPLACE "(2 - 2 * sq(sin(a!1 / 2))) / 2 = (1 - sq(sin(a!1 / 2)))") (("1" (HIDE -1) (("1" (REWRITE "cos2" :DIR RL) (("1" (GROUND) (("1" (CASE-REPLACE "cos(a!1/2) >= 0") (("1" (REWRITE "sqrt_sq") NIL NIL) ("2" (HIDE 2) (("2" (REWRITE "cos_ge_0") NIL NIL)) NIL)) NIL) ("2" (CASE "cos(a!1/2) <= 0") (("1" (REWRITE "sqrt_sq_abs") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (REWRITE "cos_le_0") NIL NIL)) NIL)) NIL) ("3" (CASE "cos(a!1/2) >= 0") (("1" (REWRITE "sqrt_sq") NIL NIL) ("2" (HIDE 2) (("2" (REWRITE "cos_ge_0_3PI2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "sq") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|tan_half_TCC1| "" (SKOSIMP) (("" (EXPAND "Tan?") (("" (LEMMA "cos_2a") (("" (INST -1 "a!1/2") (("" (REPLACE -1 * LR) (("" (HIDE -1) (("" (PROP) (("" (REPLACE -1 * LR) (("" (ASSERT) (("" (LEMMA "sin2") (("" (INST -1 "a!1/2") (("" (EXPAND "sq") (("" (REPLACE -1 * LR) (("" (HIDE -1) (("" (ASSERT) NIL NIL)) NIL)) NIL))