%Patch files loaded: patch2 version 1.2.2.36 $$$vectors.pvs vectors[L: posnat]: THEORY BEGIN index : TYPE = subrange(1,L) vector: TYPE = [index -> real] reals: LIBRARY "../../lib/reals/" IMPORTING sigma, sqrt a,b: VAR real u,v,w,z: VAR vector i: VAR index zero: vector = (LAMBDA i: 0) ; -(v): vector = (LAMBDA i: -v(i)) ; +(u,v)(i): real = u(i) + v(i) ; -(u,v)(i): real = u(i) - v(i) ; *(u,v): real = sigma(1,L,(LAMBDA i: u(i)*v(i))) ; *(a,v): vector = (LAMBDA i: a*v(i)) plus_neg : LEMMA u + (-v) = u - v dot_neg : LEMMA (-u)*w = -(u*w) dot_neg_r : LEMMA u*(-w) = -(u*w) dot_comm : LEMMA u*v = v*u dot_dist : LEMMA u*(v+w) = u*v + u*w dot_dist_r : LEMMA (v+w)*u = v*u + w*u dot_dist_minus : LEMMA u*(v-w) = u*v - u*w dot_dist_minus_r : LEMMA (v-w)*u = v*u - w*u dot_scal_l : LEMMA (a*u)*v = a*(u*v) dot_scal_r : LEMMA u*(a*v) = a*(u*v) dot_scal_assoc : LEMMA a*(b*u) = (a*b)*u dot_zero : LEMMA zero*u = 0 dot_zero_r : LEMMA u*zero = 0 dot_rw1 : LEMMA (u*v)*a = a*(u*v) sq(u): nonneg_real = u*u sq_lem : LEMMA sq(u) = sigma(1,L,(LAMBDA i: sq(u(i)))) sq_zero : LEMMA sq(zero) = 0 sq_ge_0 : LEMMA sq(u) >= 0 sq_eq_0 : LEMMA sq(u) = 0 IMPLIES u = zero l(u): real = sqrt(sq(u)) l_lem : LEMMA l(u) = sqrt(u*u) l_0 : LEMMA l(v) = 0 IFF v = zero sq_eq_0_l_0 : LEMMA sq(v) = 0 IMPLIES l(v) = 0 dot_sq_minus : LEMMA sq(u-a*v) = sq(u) - 2*a*u*v + sq(a)*sq(v) cauchy_schwartz : LEMMA sq(u*v) <= sq(u)*sq(v) END vectors $$$vectors.prf (|vectors| (|times_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|times_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|plus_neg| "" (SKOSIMP*) (("" (EXPAND "+ ") (("" (EXPAND "-") (("" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL NIL)) NIL)) NIL)) NIL) (|dot_neg| "" (SKOSIMP*) (("" (EXPAND "-") (("" (EXPAND "*") (("" (LEMMA "sigma_mult[1,L]") (("" (INST -1 "(LAMBDA i: u!1(i) * w!1(i))" "L" "1" "-1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dot_neg_r| "" (SKOSIMP*) (("" (EXPAND "-") (("" (EXPAND "*") (("" (LEMMA "sigma_mult[1,L]") (("" (INST -1 "(LAMBDA i: u!1(i) * w!1(i))" "L" "1" "-1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dot_comm| "" (SKOSIMP*) (("" (EXPAND "*") (("" (CASE "FORALL (n: subrange(1,L)): sigma(1, n, LAMBDA i: u!1(i) * v!1(i)) = sigma(1, n, LAMBDA i: v!1(i) * u!1(i))") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "n") (("1" (EXPAND "sigma") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dot_dist| "" (SKOSIMP*) (("" (EXPAND "*") (("" (CASE-REPLACE "(LAMBDA i: u!1(i) * (v!1 + w!1)(i)) = (LAMBDA i: u!1(i) * v!1(i) + u!1(i) * w!1(i))") (("1" (HIDE -1) (("1" (REWRITE "sigma_sum") NIL NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (EXPAND "+ ") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dot_dist_r| "" (SKOSIMP*) (("" (EXPAND "*") (("" (CASE-REPLACE "(LAMBDA i: (v!1 + w!1)(i) * u!1(i)) = (LAMBDA i: v!1(i)* u!1(i) + w!1(i) * u!1(i))") (("1" (HIDE -1) (("1" (REWRITE "sigma_sum") NIL NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (EXPAND "+ ") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dot_dist_minus| "" (SKOSIMP*) (("" (REWRITE "plus_neg" :DIR RL) (("" (REWRITE "dot_dist") (("" (REWRITE "dot_neg_r") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|dot_dist_minus_r| "" (SKOSIMP*) (("" (REWRITE "plus_neg" :DIR RL) (("" (REWRITE "dot_dist_r") (("" (REWRITE "dot_neg") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|dot_scal_l| "" (SKOSIMP*) (("" (EXPAND "*") (("" (LEMMA "sigma_mult[1,L]") (("" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|dot_scal_r| "" (SKOSIMP*) (("" (EXPAND "*") (("" (LEMMA "sigma_mult[1,L]") (("" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|dot_scal_assoc| "" (SKOSIMP*) (("" (EXPAND "*") (("" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL NIL)) NIL)) NIL) (|dot_zero| "" (SKOSIMP*) (("" (EXPAND "*") (("" (EXPAND "zero") (("" (LEMMA "sigma_const[1,L]") (("" (INST -1 "L" "1" "0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dot_zero_r| "" (SKOSIMP*) (("" (EXPAND "*") (("" (EXPAND "zero") (("" (LEMMA "sigma_const[1,L]") (("" (INST -1 "L" "1" "0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|dot_rw1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|sq_TCC1| "" (SKOSIMP*) (("" (EXPAND "*") (("" (CASE-REPLACE "(LAMBDA i: u!1(i) * u!1(i)) = (LAMBDA i: sq(u!1(i)))") (("1" (ASSERT) (("1" (HIDE -1) (("1" (REWRITE "sigma_nonneg") (("1" (HIDE 2) (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (EXPAND "sq") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sq_lem| "" (SKOSIMP*) (("" (EXPAND "sq") (("" (EXPAND "*") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|sq_zero| "" (EXPAND "sq") (("" (EXPAND "*") (("" (EXPAND "zero") (("" (REWRITE "sigma_const") NIL NIL)) NIL)) NIL)) NIL) (|sq_ge_0| "" (SKOSIMP*) (("" (REWRITE "sq_lem") (("" (REWRITE "sigma_nonneg") (("" (HIDE 2) (("" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sq_eq_0| "" (SKOSIMP*) (("" (EXPAND "sq") (("" (EXPAND "*") (("" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL) (|l_lem| "" (SKOSIMP*) (("" (EXPAND "l") (("" (EXPAND "*") (("" (REWRITE "sqrt_eq" :DIR RL) (("" (EXPAND "sq") (("" (EXPAND "*") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|l_0| "" (SKOSIMP*) (("" (GROUND) (("1" (EXPAND "l") (("1" (CASE "sq(v!1) = 0") (("1" (HIDE -2) (("1" (REWRITE "sq_lem") (("1" (LEMMA "sigma_nonnegfun_eq_0[1,L]") (("1" (INST?) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (INST?) (("1" (ASSERT) (("1" (HIDE -2) (("1" (EXPAND "sq") (("1" (REWRITE "zero_times3") (("1" (EXPAND "zero") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REPLACE -1) (("2" (HIDE -1) (("2" (EXPAND "l") (("2" (REWRITE "sq_zero") (("2" (REWRITE "sqrt_0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sq_eq_0_l_0| "" (SKOSIMP*) (("" (LEMMA "sq_eq_0") (("" (INST?) (("" (ASSERT) (("" (REWRITE "l_0") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|dot_sq_minus| "" (SKOSIMP*) (("" (EXPAND "sq" 1 1) (("" (LEMMA "dot_dist_minus") (("" (INST -1 "(u!1 - a!1 * v!1)" "u!1" "a!1*v!1") (("" (REPLACE -1) (("" (HIDE -1) (("" (REWRITE "dot_dist_minus_r") (("" (REWRITE "dot_dist_minus_r") (("" (EXPAND "sq") (("" (ASSERT) (("" (REWRITE "dot_scal_r") (("" (REWRITE "dot_scal_r") (("" (CASE-REPLACE "a!1 * v!1 * u!1 = a!1 * u!1 * v!1") (("1" (HIDE -1) (("1" (CASE-REPLACE "v!1 * v!1 * a!1 * a!1 = a!1*a!1*v!1 * v!1") (("1" (HIDE -1) (("1" (CASE-REPLACE "a!1 * u!1 * v!1 = a!1 * ( u!1 * v!1)") (("1" (CASE-REPLACE "2 * a!1 * u!1 * v!1 = 2 * a!1 * ( u!1 * v!1)") (("1" (NAME-REPLACE UDOTV "u!1 * v!1") (("1" (CASE-REPLACE "a!1 * a!1 * v!1 * v!1 = a!1 *( a!1 * v!1 * v!1)") (("1" (ASSERT) NIL NIL) ("2" (HIDE -1 -2 2) (("2" (LEMMA "dot_scal_assoc") (("2" (INST -1 "a!1" "a!1" "v!1") (("2" (REPLACE -1 * RL) (("2" (REWRITE "dot_scal_l") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2) (("2" (ASSERT) (("2" (REWRITE "dot_scal_l") NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) (("2" (REWRITE "dot_scal_l") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) (("2" (REWRITE "dot_scal_l") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (REWRITE "dot_scal_l") (("2" (ASSERT) (("2" (REWRITE "dot_comm") (("2" (ASSERT) (("2" (REWRITE "dot_scal_l" :DIR RL) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cauchy_schwartz| "" (SKOSIMP*) (("" (CASE "l(v!1) = 0") (("1" (REWRITE "l_0") (("1" (REPLACE -1) (("1" (REWRITE "dot_zero_r") (("1" (REWRITE "sq_zero") (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "(FORALL (t:real): sq(u!1-t*v!1) >= 0)") (("1" (INST -1 "(u!1*v!1)/sq(v!1)") (("1" (REWRITE "dot_sq_minus") (("1" (NAME-REPLACE UDOTV "u!1 * v!1") (("1" (CASE-REPLACE "2 * (UDOTV / sq(v!1)) * u!1 * v!1 = 2 * sq(UDOTV) / sq(v!1) ") (("1" (HIDE -1) (("1" (CASE-REPLACE "sq(UDOTV / sq(v!1)) * sq(v!1) = sq(UDOTV) / sq(v!1) ") (("1" (HIDE -1) (("1" (CASE-REPLACE "sq(u!1) + sq(UDOTV) / sq(v!1) - 2 * sq(UDOTV) / sq(v!1) = sq(u!1) - sq(UDOTV) / sq(v!1)") (("1" (HIDE -1) (("1" (ASSERT) (("1" (LEMMA "both_sides_times_pos_ge1") (("1" (INST -1 "sq(v!1)" "sq(u!1) - sq(UDOTV) / sq(v!1) " "0") (("1" (ASSERT) NIL NIL) ("2" (FLATTEN) (("2" (HIDE -2 2) (("2" (LEMMA "sq_eq_0") (("2" (INST?) (("2" (ASSERT) (("2" (HIDE -2) (("2" (REWRITE "l_0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE -1 3) (("3" (CASE-REPLACE "sq(v!1) = 0") (("1" (LEMMA "sq_eq_0") (("1" (INST?) (("1" (ASSERT) (("1" (REWRITE "l_0") NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) (("3" (FLATTEN) (("3" (HIDE -2 2) (("3" (LEMMA "sq_eq_0") (("3" (INST?) (("3" (ASSERT) (("3" (REWRITE "l_0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE -1 3) (("2" (EXPAND "sq") (("2" (NAME-REPLACE "vdotv" "v!1 * v!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (FLATTEN) (("3" (HIDE -2 2) (("3" (LEMMA "sq_eq_0") (("3" (INST?) (("3" (ASSERT) (("3" (REWRITE "l_0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE -1 3) (("2" (REVEAL -2) (("2" (CASE-REPLACE "2 * (UDOTV / sq(v!1)) * u!1 * v!1 = 2 * (UDOTV / sq(v!1)) * (u!1 * v!1)") (("1" (HIDE -1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 2 3) (("2" (REWRITE "dot_scal_assoc" :DIR RL) (("1" (LEMMA "dot_scal_assoc") (("1" (AUTO-REWRITE "dot_scal_l") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "dot_rw1") (("2" (ASSERT) (("2" (AUTO-REWRITE "dot_scal_l") (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) (("3" (HIDE -1 2) (("3" (REWRITE "sq_eq_0_l_0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (REWRITE "sq_eq_0_l_0") NIL NIL)) NIL)) NIL) ("2" (REWRITE "sq_eq_0_l_0") NIL NIL)) NIL) ("2" (REWRITE "sq_eq_0_l_0") NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$sq.pvs sq: THEORY BEGIN a,b,d: VAR real nna,nnb,nnc : VAR nonneg_real %% added nna, nnb VAC n : VAR nat %% added n VAC sq(a): nonneg_real = a*a sq_neg : LEMMA sq(-a) = sq(a) sq_pos : LEMMA sq(a) >= 0 sq_plus_pos : LEMMA sq(a)+sq(b) >= 0 sq_times : LEMMA sq(a*b) = sq(a) * sq(b) sq_plus : LEMMA sq(a+b) = sq(a) + 2*a*b + sq(b) sq_minus : LEMMA sq(a-b) = sq(a) - 2*a*b + sq(b) sq_neg_minus : LEMMA sq(a-b) = sq(b-a) sq_0 : LEMMA sq(0) = 0 sq_eq_0 : LEMMA sq(a) = 0 IMPLIES a = 0 sq_0_IFF : LEMMA sq(a) = 0 IFF a = 0 %% added VAC sq_gt_0_IFF : LEMMA sq(a) > 0 IFF a /= 0 %% added VAC sq_div : LEMMA d /= 0 => sq(a/d) = sq(a)/sq(d) sq_plus_eq_0 : LEMMA sq(a) + sq(b) = 0 <=> (a = 0 AND b = 0) % -------------------- Inequalities -------------------- sq_ge : LEMMA nna >= nnb IFF sq(nna) >= sq(nnb) sq_le : LEMMA nna <= nnb IFF sq(nna) <= sq(nnb) sq_gt : LEMMA nna > nnb IFF sq(nna) > sq(nnb) sq_lt : LEMMA nna < nnb IFF sq(nna) < sq(nnb) sq_eq : LEMMA nna = nnb IFF sq(nna) = sq(nnb) %% added VAC % The following removed by RWB because has nothing to do with "sq" % both_sides_expt_non_neg_lt_aux: lemma %% added VAC % expt(nna, n+1) < expt(nnb, n+1) IFF nna < nnb % both_sides_expt_non_neg_le_aux: lemma %% added VAC % expt(nna, n+1) <= expt(nnb, n+1) IFF nna <= nnb sq_neg_pos_le : LEMMA sq(a) <= sq(nnc) IMPLIES (-nnc <= a AND a <= nnc) neg_pos_sq_le : LEMMA (-b <= a AND a <= b) IMPLIES sq(a) <= sq(b) sq_neg_pos_lt : LEMMA sq(a) < sq(nnc) IMPLIES (-nnc < a AND a < nnc) neg_pos_sq_lt : LEMMA (-b < a AND a < b) IMPLIES sq(a) < sq(b) sq_le_abs : LEMMA sq(a) <= sq(b) IMPLIES abs(a) <= abs(b) sq_lt_abs : LEMMA sq(a) < sq(b) IMPLIES abs(a) < abs(b) % |\ % | \ C <= c % A | \ % +---- % B triangle_rectangle: LEMMA sq(a)+sq(b) <= sq(nnc) IMPLIES -nnc <= a AND a <= nnc AND -nnc <= b AND b <= nnc triangle_ineq_lt : LEMMA sq(a) + sq(b) < sq(d) IMPLIES %% RWB ADDED abs(a) < abs(d) AND abs(b) < abs(d) triangle_ineq_le : LEMMA sq(a) + sq(b) <= sq(d) IMPLIES %% RWB ADDED abs(a) <= abs(d) AND abs(b) <= abs(d) END sq $$$sq.prf (|sq| (|sq_TCC1| "" (GROUND) NIL NIL) (|sq_neg| "" (GRIND) NIL NIL) (|sq_pos| "" (GRIND) NIL NIL) (|sq_plus_pos| "" (SKOLEM 1 ("a" "b")) (("" (CASE "sq(a)>=0" "sq(b) >= 0") (("1" (GROUND) NIL NIL) ("2" (REWRITE "sq_pos") NIL NIL) ("3" (REWRITE "sq_pos") NIL NIL)) NIL)) NIL) (|sq_times| "" (GRIND) NIL NIL) (|sq_plus| "" (GRIND) NIL NIL) (|sq_minus| "" (GRIND) NIL NIL) (|sq_neg_minus| "" (GRIND) NIL NIL) (|sq_0| "" (GRIND) NIL NIL) (|sq_eq_0| "" (SKOSIMP*) (("" (EXPAND "sq") (("" (LEMMA "zero_times3") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sq_0_IFF| "" (SKOSIMP*) (("" (GROUND) (("1" (REWRITE "sq_eq_0") NIL NIL) ("2" (REPLACE -1 1) (("2" (EXPAND "sq") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sq_gt_0_IFF| "" (SKOSIMP*) (("" (EXPAND "sq") (("" (LEMMA "pos_times_gt") (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sq_div_TCC1| "" (SKOLEM 1 "d") (("" (GROUND) (("" (REWRITE "sq_eq_0") NIL NIL)) NIL)) NIL) (|sq_div| "" (GRIND) NIL NIL) (|sq_plus_eq_0| "" (SKOLEM 1 ("a" "b")) (("" (GROUND) (("1" (LEMMA "sq_pos") (("1" (INST -1 "b") (("1" (CASE "sq(a)>0") (("1" (GROUND) NIL NIL) ("2" (DELETE -) (("2" (EXPAND "sq") (("2" (REWRITE "pos_times_gt") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sq_pos") (("2" (INST -1 "a") (("2" (CASE "sq(b)>0") (("1" (GROUND) NIL NIL) ("2" (DELETE -) (("2" (EXPAND "sq") (("2" (REWRITE "pos_times_gt") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (GRIND) NIL NIL)) NIL)) NIL) (|sq_ge| "" (SKOSIMP*) (("" (GROUND) (("1" (LEMMA "ge_times_ge_pos") (("1" (INST?) (("1" (INST -1 "nnb!1" "nna!1") (("1" (GROUND) (("1" (EXPAND "sq") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "nna!1 < nnb!1") (("1" (CASE "sq(nna!1) < sq(nnb!1)") (("1" (GROUND) NIL NIL) ("2" (HIDE -2 2) (("2" (LEMMA "lt_times_lt_pos1") (("2" (INST -1 "nna!1" "nna!1" "nnb!1" "nnb!1") (("1" (GROUND) (("1" (EXPAND "sq") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (GROUND) (("2" (CASE "nna!1=0") (("1" (GROUND) (("1" (REPLACE -1 :HIDE? T) (("1" (EXPAND "sq") (("1" (GROUND) (("1" (REWRITE "pos_times_lt") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|sq_le| "" (LEMMA "sq_ge") (("" (SKOLEM 1 ("nna" "nnb")) (("" (INST -1 "nnb" "nna") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|sq_gt| "" (SKOSIMP*) (("" (GROUND) (("1" (LEMMA "gt_times_gt_pos1") (("1" (INST?) (("1" (INST -1 "nnb!1" "nna!1") (("1" (ASSERT) (("1" (HIDE -2) (("1" (EXPAND "sq") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "nnb!1 = 0") (("1" (HIDE -1 1) (("1" (EXPAND "sq" 1 2) (("1" (LEMMA "sq_pos") (("1" (INST?) (("1" (ASSERT) (("1" (LEMMA "sq_eq_0") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "nna!1 <= nnb!1") (("1" (CASE "sq(nna!1) <= sq(nnb!1)") (("1" (GROUND) NIL NIL) ("2" (HIDE -2 2) (("2" (LEMMA "le_times_le_pos") (("2" (INST -1 "nna!1" "nna!1" "nnb!1" "nnb!1") (("2" (GROUND) (("2" (EXPAND "sq") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|sq_lt| "" (SKOLEM 1 ("nna" "nnb")) (("" (LEMMA "sq_gt") (("" (INST -1 "nnb" "nna") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|sq_eq| "" (SKOSIMP*) (("" (CASE-REPLACE "nna!1 = 0") (("1" (LEMMA "sq_0_IFF") (("1" (INST -1 "nnb!1") (("1" (EXPAND "sq") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "nnb!1 = 0") (("1" (LEMMA "sq_0_IFF") (("1" (INST?) (("1" (EXPAND "sq") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "both_sides_expt2_aux") (("2" (INST -1 "2" "nna!1" "nnb!1") (("1" (EXPAND "expt") (("1" (EXPAND "expt") (("1" (EXPAND "expt") (("1" (EXPAND "sq") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_non_neg_lt_aux| "" (SKOSIMP*) (("" (CASE "nna!1 = 0") (("1" (CASE "nnb!1 = 0") (("1" (REPLACE*) (("1" (GRIND) NIL NIL)) NIL) ("2" (REPLACE -1) (("2" (EXPAND "expt" 2 1) (("2" (LEMMA "zero_times1") (("2" (INST?) (("2" (REPLACE -1 :HIDE? T) (("2" (LEMMA "expt_pos_aux") (("2" (INST?) (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "nnb!1 = 0") (("1" (REPLACE -1) (("1" (EXPAND "expt" 2 2) (("1" (LEMMA "zero_times1") (("1" (INST?) (("1" (REPLACE -1 :HIDE? T) (("1" (LEMMA "expt_pos_aux") (("1" (INST?) (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "both_sides_expt_pos_lt_aux") (("2" (INST?) (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_non_neg_le_aux| "" (SKOSIMP*) (("" (CASE "nna!1 = 0") (("1" (CASE "nnb!1 = 0") (("1" (REPLACE*) (("1" (GRIND) NIL NIL)) NIL) ("2" (REPLACE*) (("2" (EXPAND "expt") (("2" (LEMMA "zero_times1") (("2" (INST?) (("2" (REPLACE*) (("2" (LEMMA "pos_times_le") (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "nnb!1 = 0") (("1" (REPLACE*) (("1" (EXPAND "expt") (("1" (LEMMA "zero_times1") (("1" (INST?) (("1" (REPLACE*) (("1" (LEMMA "neg_times_le") (("1" (INST?) (("1" (LEMMA "expt_pos_aux") (("1" (INST -1 "n!1" "nna!1") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "both_sides_expt_pos_le_aux") (("2" (INST?) (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sq_neg_pos_le| "" (SKOLEM 1 ("a" "c")) (("" (FLATTEN) (("" (CASE "a >= 0") (("1" (LEMMA "sq_le") (("1" (INST -1 "a" "c") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "sq_le") (("2" (INST -1 "-a" "c") (("1" (REWRITE "sq_neg") (("1" (GROUND) NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|neg_pos_sq_le| "" (SKOLEM 1 ("a" "b")) (("" (GROUND) (("" (CASE "a > 0") (("1" (LEMMA "sq_le") (("1" (INST -1 "a" "b") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL) ("2" (CASE "-a <= b") (("1" (LEMMA "sq_le") (("1" (INST -1 "-a" "b") (("1" (GROUND) (("1" (REWRITE "sq_neg") NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sq_neg_pos_lt| "" (SKOLEM 1 ("a" "c")) (("" (FLATTEN) (("" (CASE "a >= 0") (("1" (LEMMA "sq_lt") (("1" (INST -1 "a" "c") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "sq_lt") (("2" (INST -1 "-a" "c") (("1" (REWRITE "sq_neg") (("1" (GROUND) NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|neg_pos_sq_lt| "" (SKOLEM 1 ("a" "b")) (("" (GROUND) (("" (CASE "a > 0") (("1" (LEMMA "sq_lt") (("1" (INST -1 "a" "b") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL) ("2" (CASE "-a < b") (("1" (LEMMA "sq_lt") (("1" (INST -1 "-a" "b") (("1" (GROUND) (("1" (REWRITE "sq_neg") NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sq_le_abs| "" (SKOSIMP*) (("" (CASE-REPLACE "b!1 >= 0") (("1" (LEMMA "sq_neg_pos_le") (("1" (INST -1 "a!1" "b!1") (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sq_neg_pos_le") (("2" (INST -1 "a!1" "-b!1") (("1" (ASSERT) (("1" (CASE-REPLACE "sq(-b!1) = sq(b!1)") (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 3) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sq_lt_abs| "" (SKOSIMP*) (("" (CASE-REPLACE "b!1 >= 0") (("1" (LEMMA "sq_neg_pos_lt") (("1" (INST -1 "a!1" "b!1") (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sq_neg_pos_lt") (("2" (INST -1 "a!1" "-b!1") (("1" (ASSERT) (("1" (CASE-REPLACE "sq(-b!1) = sq(b!1)") (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -2 3) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|triangle_rectangle| "" (SKOLEM 1 ("a" "b" "c")) (("" (FLATTEN) (("" (CASE "sq(a)>=0" "sq(b)>=0" "sq(c)>=0") (("1" (CASE "sq(a) <= sq(c)") (("1" (CASE "sq(b) <= sq(c)") (("1" (LEMMA "sq_neg_pos_le") (("1" (INST-CP -1 "a" "c") (("1" (INST -1 "b" "c") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 -1) (("2" (GROUND) NIL NIL)) NIL)) NIL) ("2" (HIDE 2 -1) (("2" (GROUND) NIL NIL)) NIL)) NIL) ("2" (REWRITE "sq_pos") NIL NIL) ("3" (REWRITE "sq_pos") NIL NIL) ("4" (REWRITE "sq_pos") NIL NIL)) NIL)) NIL)) NIL) (|triangle_ineq_lt| "" (SKOSIMP*) (("" (LEMMA "sq_lt_abs") (("" (INST?) (("" (ASSERT) (("" (LEMMA "sq_lt_abs") (("" (INST -1 "b!1" "d!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|triangle_ineq_le| "" (SKOSIMP*) (("" (LEMMA "sq_le_abs") (("" (INST?) (("" (ASSERT) (("" (LEMMA "sq_le_abs") (("" (INST -1 "b!1" "d!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$sqrt.pvs sqrt: THEORY %------------------------------------------------------------------------ % % Square root of non-negative real: AXIOMATIC VERSION % %------------------------------------------------------------------------ BEGIN IMPORTING sq % sq(a): nonneg_real = a*a nnx, nny, nnz: VAR nonneg_real x,y,z,xx: VAR real sqrt_exists: AXIOM (EXISTS (f: [nnx: nonneg_real -> {nnz: nonneg_real | nnz * nnz = nnx}]): TRUE) sqrt(nnx): {nnz | nnz*nnz = nnx} sqrt_pos : JUDGEMENT sqrt(px: posreal) HAS_TYPE posreal sqrt_nnr : JUDGEMENT sqrt(px: nonneg_real) HAS_TYPE nonneg_real % -------------------- Special Arguments -------------------- sqrt_0 : LEMMA sqrt(0) = 0 sqrt_1 : LEMMA sqrt(1) = 1 sqrt_eq_0 : LEMMA sqrt(nnx) = 0 IMPLIES nnx = 0 % -------------------- Basic Properties -------------------- sqrt_lem : LEMMA sqrt(nny) = nnz IFF nnz * nnz = nny sqrt_def : LEMMA sqrt(nnx) * sqrt(nnx) = nnx sqrt_square : LEMMA sqrt(nnx * nnx) = nnx sqrt_sq : LEMMA x >= 0 IMPLIES sqrt(sq(x)) = x sqrt_sq_abs : LEMMA sqrt(sq(x)) = abs(x) sq_sqrt : LEMMA x >= 0 IMPLIES sq(sqrt(x))=x sqrt_times : LEMMA sqrt(nny * nnz) = sqrt(nny) * sqrt(nnz) sqrt_div : LEMMA nnz /= 0 IMPLIES sqrt(nny / nnz) = sqrt(nny) / sqrt(nnz) % --------------------- Inequalities -------------------- sqrt_lt : LEMMA nny < nnz IFF sqrt(nny) < sqrt(nnz) sqrt_le : LEMMA nny <= nnz IFF sqrt(nny) <= sqrt(nnz) sqrt_gt : LEMMA nny > nnz IFF sqrt(nny) > sqrt(nnz) sqrt_ge : LEMMA nny >= nnz IFF sqrt(nny) >= sqrt(nnz) sqrt_eq : LEMMA nny = nnz IFF sqrt(nny) = sqrt(nnz) %% added VAC sqrt_less : LEMMA nnx > 1 IMPLIES sqrt(nnx) < nnx sqrt_more : LEMMA nnx > 0 AND nnx < 1 IMPLIES sqrt(nnx) > nnx % --------------------- Real Arguments --------------------- sides_lt_hypotenuse : LEMMA sqrt(sq(x) + sq(y)) < z IMPLIES %% added VAC abs(x) < z AND abs(y) < z sides_le_hypotenuse : LEMMA sqrt(sq(x) + sq(y)) <= z IMPLIES %% added VAC abs(x) <= z AND abs(y) <= z D: VAR real sqrt_sides_over_magnitude : LEMMA D > 0 AND D = sqrt(sq(y) + sq(x)) IMPLIES sqrt(sq(y/D) + sq(x/D)) = 1 %% added VAC % ------ the following theorems seem too specific to be in the sqrt library ------ one_over_sqrt_1 : LEMMA x > 0 IMPLIES %% added VAC (1 / (sqrt(1 + sq(y / x))) = x * (1 / sqrt(sq(x) + sq(y)))) sqrt_1_plus_yx: LEMMA x > 0 IMPLIES %% RWB proposed alternative x*sqrt(1 + sq(y/x)) = sqrt(sq(x) + sq(y)) one_over_sqrt_2 : LEMMA %% added VAC x < 0 IMPLIES (1 / (sqrt(1 + sq(y / x))) = - x * (1 / sqrt(sq(x) + sq(y)))) yx_over_sqrt_1 : LEMMA %% added VAC x > 0 implies (y/x / (sqrt(1 + sq(y / x))) = y * (1 / sqrt(sq(x) + sq(y)))) END sqrt $$$sqrt.prf (|sqrt| (|sqrt_TCC1| "" (LEMMA "sqrt_exists") (("" (PROPAX) NIL NIL)) NIL) (|sqrt_pos| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|sqrt_0| "" (TYPEPRED "sqrt(0)") (("" (LEMMA "zero_times3") (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|sqrt_1| "" (TYPEPRED "sqrt(1)") (("" (LEMMA "sqrt_1") (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|sqrt_eq_0| "" (SKOSIMP*) (("" (TYPEPRED "sqrt(nnx!1)") (("" (LEMMA "both_sides_expt2") (("" (INST -1 "2" "_" "_") (("" (EXPAND "^") (("" (EXPAND "expt") (("" (EXPAND "expt") (("" (EXPAND "expt") (("" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_lem| "" (SKOSIMP*) (("" (GROUND) (("" (TYPEPRED "sqrt(nny!1)") (("" (REPLACE -2 - RL) (("" (HIDE -1 -2) (("" (LEMMA "both_sides_expt2") (("" (INST -1 "2" "_" "_") (("" (EXPAND "^") (("" (EXPAND "expt") (("" (EXPAND "expt") (("" (EXPAND "expt") (("" (CASE-REPLACE "nnz!1 = 0") (("1" (LEMMA "zero_times3") (("1" (HIDE -2 -3) (("1" (INST -1 "sqrt(nny!1)" "sqrt(nny!1)") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "sqrt(nny!1) = 0") (("1" (HIDE -1) (("1" (LEMMA "zero_times3") (("1" (HIDE -2) (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("1" (GROUND) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_def| "" (SKOSIMP*) (("" (TYPEPRED "sqrt(nnx!1)") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|sqrt_square| "" (SKOSIMP*) (("" (TYPEPRED "sqrt(nnx!1 * nnx!1)") (("" (CASE-REPLACE "nnx!1 = 0") (("1" (ASSERT) (("1" (LEMMA "zero_times3") (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "sqrt(nnx!1 * nnx!1) = 0") (("1" (LEMMA "zero_times3") (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (LEMMA "both_sides_expt2") (("2" (INST -1 "2" "_" "_") (("2" (EXPAND "^") (("2" (EXPAND "expt") (("2" (EXPAND "expt") (("2" (EXPAND "expt") (("2" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_sq| "" (SKOSIMP*) (("" (EXPAND "sq") (("" (REWRITE "sqrt_square") NIL NIL)) NIL)) NIL) (|sqrt_sq_abs| "" (SKOSIMP*) (("" (CASE "x!1 >= 0") (("1" (EXPAND "sq") (("1" (REWRITE "sqrt_square") (("1" (EXPAND "abs") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sq_neg") (("2" (INST?) (("2" (REPLACE -1 :HIDE? T :DIR RL) (("2" (EXPAND "sq") (("2" (REWRITE "sqrt_square") (("2" (EXPAND "abs") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sq_sqrt| "" (SKOSIMP*) (("" (EXPAND "sq") (("" (REWRITE "sqrt_def") NIL NIL)) NIL)) NIL) (|sqrt_times| "" (SKOSIMP*) (("" (CASE "sqrt(nny!1) = 0 OR sqrt(nnz!1) = 0") (("1" (GROUND) NIL NIL) ("2" (FLATTEN) (("2" (LEMMA "both_sides_expt2") (("2" (INST -1 "2" "_" "_") (("2" (EXPAND "^") (("2" (EXPAND "expt") (("2" (EXPAND "expt") (("2" (EXPAND "expt") (("2" (INST -1 "sqrt(nny!1) * sqrt(nnz!1)" "sqrt(nny!1 * nnz!1)") (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (CASE-REPLACE "sqrt(nny!1 * nnz!1) = 0") (("1" (LEMMA "sqrt_eq_0") (("1" (INST -1 "nny!1*nnz!1") (("1" (ASSERT) (("1" (LEMMA "zero_times3") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (TYPEPRED "sqrt(nny!1 * nnz!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (CASE-REPLACE "sqrt(nny!1) * sqrt(nnz!1) = 0") (("1" (LEMMA "zero_times3") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_div_TCC1| "" (SKOSIMP*) (("" (REWRITE "pos_div_ge") NIL NIL)) NIL) (|sqrt_div_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|sqrt_div| "" (SKOSIMP*) (("" (LEMMA "sqrt_sq") (("" (INST -1 "sqrt(nny!1)/sqrt(nnz!1)") (("1" (GROUND) (("1" (HIDE 2 3) (("1" (LEMMA "sqrt_pos") (("1" (INST -1 "nny!1") (("1" (REWRITE "pos_div_ge") NIL NIL) ("2" (CASE-REPLACE "nny!1=0") (("1" (REWRITE "sqrt_0") (("1" (ASSERT) NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sqrt_eq_0") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_lt| "" (SKOSIMP*) (("" (GROUND) (("1" (TYPEPRED "sqrt(nny!1)") (("1" (REPLACE -2 - RL) (("1" (HIDE -2) (("1" (TYPEPRED "sqrt(nnz!1)") (("1" (REPLACE -2 - RL) (("1" (HIDE -1 -2 -3) (("1" (LEMMA "both_sides_expt_pos_lt_aux") (("1" (INST -1 "1" "sqrt(nny!1)" "sqrt(nnz!1)") (("1" (EXPAND "expt") (("1" (EXPAND "expt") (("1" (EXPAND "expt") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "gt_times_gt_pos1") (("2" (INST -1 "sqrt(nny!1)" "sqrt(nny!1)" "sqrt(nnz!1)" "sqrt(nnz!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_le| "" (SKOSIMP*) (("" (LEMMA "sqrt_lt") (("" (INST -1 "nny!1" "nnz!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|sqrt_gt| "" (SKOSIMP*) (("" (LEMMA "sqrt_lt") (("" (INST -1 "nny!1" "nnz!1") (("" (ASSERT) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_ge| "" (SKOSIMP*) (("" (LEMMA "sqrt_le") (("" (INST -1 "nny!1" "nnz!1") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|sqrt_eq| "" (SKOSIMP*) (("" (GROUND) NIL NIL)) NIL) (|sqrt_less| "" (SKOSIMP*) (("" (TYPEPRED "sqrt(nnx!1)") (("" (LEMMA "both_sides_expt_pos_gt_aux") (("" (INST -1 "1" "nnx!1" "sqrt(nnx!1)") (("1" (FLATTEN) (("1" (HIDE -2) (("1" (ASSERT) (("1" (EXPAND "expt") (("1" (EXPAND "expt") (("1" (EXPAND "expt") (("1" (REPLACE -2) (("1" (HIDE -2 2) (("1" (LEMMA "both_sides_times_pos_gt1") (("1" (INST -1 "nnx!1" "nnx!1" "1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "sqrt(nnx!1) = 0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_more| "" (SKOSIMP*) (("" (TYPEPRED "sqrt(nnx!1)") (("" (LEMMA "both_sides_expt_pos_gt_aux") (("" (INST -1 "1" "sqrt(nnx!1)" "nnx!1") (("1" (FLATTEN) (("1" (HIDE -2) (("1" (ASSERT) (("1" (EXPAND "expt") (("1" (EXPAND "expt") (("1" (EXPAND "expt") (("1" (REPLACE -2) (("1" (HIDE -2 2) (("1" (LEMMA "both_sides_times_pos_gt1") (("1" (INST -1 "nnx!1" "1" "nnx!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sides_lt_hypotenuse| "" (SKOSIMP*) (("" (LEMMA "sq_lt") (("" (INST -1 "sqrt(sq(x!1) + sq(y!1))" "z!1") (("1" (ASSERT) (("1" (HIDE -2) (("1" (REWRITE "sq_sqrt") (("1" (LEMMA "triangle_ineq_lt") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE -2) (("1" (FLATTEN) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sides_le_hypotenuse| "" (SKOSIMP*) (("" (LEMMA "sq_le") (("" (INST -1 "sqrt(sq(x!1) + sq(y!1))" "z!1") (("1" (ASSERT) (("1" (HIDE -2) (("1" (REWRITE "sq_sqrt") (("1" (LEMMA "triangle_ineq_le") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE -2) (("1" (FLATTEN) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|sqrt_sides_over_magnitude_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sqrt_sides_over_magnitude| "" (SKOSIMP*) (("" (CASE-REPLACE "sq(y!1 / D!1) + sq(x!1 / D!1) = (sq(y!1) + sq(x!1))/sq(D!1)") (("1" (HIDE -1) (("1" (CASE-REPLACE "sq(y!1) + sq(x!1) = sq(D!1)") (("1" (HIDE -1) (("1" (ASSERT) (("1" (CASE-REPLACE "sq(D!1) / sq(D!1) = 1") (("1" (HIDE -1 -2) (("1" (CASE-REPLACE "sqrt(1) = sqrt(1*1)") (("1" (HIDE -1) (("1" (REWRITE "sqrt_square") NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) NIL NIL)) NIL) ("3" (HIDE -2 2) (("3" (EXPAND "sq") (("3" (ASSERT) (("3" (LEMMA "zero_times3") (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "sqrt_lem") (("2" (EXPAND "sq" 1 3) (("2" (INST?) (("2" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (HIDE -2) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE -2 2) (("3" (EXPAND "sq") (("3" (LEMMA "zero_times3") (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "zero_times3") (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|one_over_sqrt_1_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|one_over_sqrt_1_TCC2| "" (SKOSIMP*) (("" (CASE-REPLACE "sq(x!1) + sq(y!1) = 0") (("1" (HIDE -3) (("1" (LEMMA "sq_plus_eq_0") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "sqrt_eq_0") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|one_over_sqrt_1| "" (SKOLEM 1 ("x" "y")) (("" (SKOSIMP*) (("" (REWRITE "sq_div") (("" (CASE-REPLACE "1 + sq(y) / sq(x) = (sq(x) + sq(y)) / sq(x)") (("1" (REWRITE "sqrt_div") (("1" (REWRITE "sqrt_sq") (("1" (GROUND) NIL NIL)) NIL) ("2" (HIDE -1 2) (("2" (REWRITE "sq_eq_0") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (REWRITE "sq_eq_0") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sqrt_1_plus_yx| "" (SKOSIMP*) (("" (CASE-REPLACE "1 + sq(y!1 / x!1) = (sq(x!1) + sq(y!1))/sq(x!1)") (("1" (HIDE -1) (("1" (REWRITE "sqrt_div") (("1" (REWRITE "sqrt_sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (LEMMA "sq_eq_0") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (LEMMA "sq_eq_0") (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("4" (ASSERT) NIL NIL)) NIL)) NIL) (|one_over_sqrt_2_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|one_over_sqrt_2_TCC2| "" (SKOSIMP*) (("" (LEMMA "sqrt_eq_0") (("" (INST -1 "sq(x!1) + sq(y!1)") (("" (REPLACE -3) (("" (SPLIT -1) (("1" (HIDE -3) (("1" (CASE-REPLACE "sq(x!1) = 0") (("1" (ASSERT) (("1" (EXPAND "sq") (("1" (ASSERT) (("1" (LEMMA "zero_times3") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|one_over_sqrt_2| "" (SKOLEM 1 ("x" "y")) (("" (SKOSIMP*) (("" (REWRITE "sq_div") (("" (CASE-REPLACE "1 + sq(y) / sq(x) = (sq(x) + sq(y)) / sq(x)") (("1" (REWRITE "sqrt_div") (("1" (REWRITE "sqrt_sq_abs") (("1" (EXPAND "abs") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) (("2" (HIDE -1 2) (("2" (LEMMA "zero_times3") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (REWRITE "sq_eq_0") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|yx_over_sqrt_1| "" (SKOSIMP*) (("" (CASE-REPLACE "(y!1 / x!1 / (sqrt(1 + sq(y!1 / x!1)))) = ((y!1 / x!1) * (1 / (sqrt(1 + sq(y!1 / x!1)))))") (("1" (REWRITE "one_over_sqrt_1") (("1" (GROUND) NIL NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (GROUND) NIL NIL)) NIL)) NIL)) $$$sigma.pvs sigma[ii,jj: nat]: THEORY %------------------------------------------------------------------------------ % The summations theory introduces and defines properties of the sigma % function that sums an arbitrary function F: [subrange(ii,jj) -> real] over % a range from low to high % % high % ---- % sigma(low, high, F) = \ F(j) % / % ---- % j = low % %------------------------------------------------------------------------------ BEGIN low, high,l,h: VAR subrange(ii,jj) m,n: VAR nat i: VAR subrange(ii,jj) rng: VAR nat x,B: VAR real F, G: VAR function[subrange(ii,jj) -> 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: high) sigma_sum : THEOREM sigma(low, high, F) + sigma(low, high, G) = sigma(low, high, (LAMBDA i: F(i) + G(i))) 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_split : THEOREM low <= m AND m < high IMPLIES sigma(low, high, F) = sigma(low, m, F) + sigma(m+1, high, F) sigma_first : THEOREM high > low IMPLIES sigma(low, high, F) = F(low) + sigma(low+1, high, F) 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_mult : THEOREM sigma(low, high, (LAMBDA i: x * F(i))) = x * 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 i: abs(F(i))) restrict(F, low, high): function[subrange(ii,jj) -> 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_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[subrange(ii,jj) -> nonneg_real] Fnpr: VAR function[subrange(ii,jj) -> nonpos_real] Fnat: VAR function[subrange(ii,jj) -> nat] Fnni: VAR function[subrange(ii,jj) -> nonneg_int] Fnpi: VAR function[subrange(ii,jj) -> nonpos_int] Fn: VAR function[subrange(ii,jj) -> nat] 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,Fnni) HAS_TYPE nonneg_int JUDGEMENT sigma(low,high,Fnpi) HAS_TYPE nonpos_int JUDGEMENT sigma(low,high,Fn) HAS_TYPE nat sigma_nonnegfun_eq_0: LEMMA sigma(low,high,Fnnr) = 0 AND low <= i AND i <= high IMPLIES Fnnr(i) = 0 END sigma $$$sigma.prf (|sigma| (|sigma_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sigma_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|sigma_sum| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (LIFT-IF) (("2" (GROUND) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (GROUND) NIL NIL)) NIL)) NIL) (|sigma_diff_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sigma_diff_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|sigma_diff| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1 1) (("2" (GROUND) (("2" (EXPAND "sigma" 1 3) (("2" (GROUND) (("2" (LIFT-IF) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) 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" (HIDE 2) (("5" (ASSERT) NIL NIL)) NIL)) NIL) (|sigma_diff_neg| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1 2) (("2" (GROUND) (("2" (EXPAND "sigma" 1 3) (("2" (LIFT-IF) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) 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" (HIDE 2) (("5" (ASSERT) NIL NIL)) NIL)) NIL) (|sigma_split| "" (CASE "(FORALL (F: [subrange(ii,jj) -> real]), low,m,rng: m >= low AND m < low+rng AND low+rng <= jj 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) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (TYPEPRED "rng!2") (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (ASSERT) (("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("5" (HIDE 2) (("5" (SKOSIMP*) NIL 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" (HIDE 2) (("5" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_first_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sigma_first| "" (SKOSIMP*) (("" (LEMMA "sigma_split") (("" (INST?) (("" (INST -1 "low!1") (("" (ASSERT) (("" (EXPAND "sigma" -1 3) (("" (PROPAX) 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): low!1 + rng <= jj 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-AND-SIMPLIFY "rng") NIL NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) (|sigma_mult| "" (SKOSIMP*) (("" (CASE "(FORALL (rng:nat): low!1+rng <= jj IMPLIES sigma(low!1, low!1+rng, (LAMBDA i: x!1 * F!1(i))) = x!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" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_bound| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): (FORALL i: i >= low!1 AND i <= low!1+rng IMPLIES F!1(i) <= B!1) AND low!1 + rng <= jj 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" (INST?) (("2" (ASSERT) (("2" (SPLIT -1) (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "abs") (("2" (ASSERT) (("2" (EXPAND "sigma") (("2" (ASSERT) (("2" (LIFT-IF) (("2" (GROUND) (("1" (REVEAL -1) (("1" (INST -1 "low!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REVEAL -1) (("2" (INST -1 "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_abs| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): low!1 + rng <= high!1 IMPLIES abs(sigma(low!1, low!1+rng, F!1)) <= sigma(low!1, low!1+rng, LAMBDA i: abs(F!1(i))))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (EXPAND "sigma") (("2" (ASSERT) (("2" (EXPAND "abs") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "sigma") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) (("2" (LEMMA "triangle") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_restrict| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (LIFT-IF) (("1" (GROUND) (("1" (EXPAND "restrict") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (EXPAND "restrict") (("2" (LIFT-IF) (("2" (LIFT-IF) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) 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_TCC1| "" (SUBTYPE-TCC) 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_nonneg| "" (CASE " FORALL (F: [subrange(ii, jj) -> real], rng:nat, low: subrange(ii, jj)): (FORALL i: F(i) >= 0) AND low + rng <= jj IMPLIES sigma(low, low+rng, F) >= 0") (("1" (SKOSIMP*) (("1" (INST?) (("1" (INST -1 "high!1-low!1" "low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (INST?) (("2" (INST?) (("1" (ASSERT) (("1" (REVEAL -1) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_nonpos| "" (CASE " FORALL (F: [subrange(ii, jj) -> real], rng:nat, low: subrange(ii, jj)): (FORALL i: F(i) <= 0) AND low + rng <= jj IMPLIES sigma(low, low+rng, F) <= 0") (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) (("1" (INST -1 "high!1-low!1" "low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (INST?) (("2" (INST?) (("1" (ASSERT) (("1" (REVEAL -1) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_TCC3| "" (SKOSIMP*) (("" (REWRITE "sigma_nonneg") (("" (HIDE 2) (("" (SKOSIMP*) (("" (ASSERT) NIL 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") (("" (MEASURE-INDUCT+ "high~low" ("high" "low")) (("" (SKOSIMP*) (("" (EXPAND "sigma" 1) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "~") (("1" (GROUND) (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "~") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) (("2" (TYPEPRED "Fnat!1(x!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LIFT-IF) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_TCC6| "" (AUTO-REWRITE-THEORY "integers") (("" (AUTO-REWRITE-THEORY "rationals") (("" (MEASURE-INDUCT+ "high~low" ("high" "low")) (("" (SKOSIMP*) (("" (EXPAND "sigma" 1) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "~") (("1" (GROUND) (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "~") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LIFT-IF) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_nonnegfun_eq_0| "" (SKOSIMP*) (("" (CASE "FORALL (Fnnr: [subrange(ii, jj) -> nonneg_real], rng:nat, low: subrange(ii, jj)): low + rng <= jj AND sigma(low, low+rng, Fnnr) = 0 AND low <= i!1 AND i!1 <= low + rng IMPLIES Fnnr(i!1) = 0") (("1" (INST?) (("1" (INST -1 "high!1-low!1" "low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (HIDE -5 2) (("1" (EXPAND "sigma") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (EXPAND "sigma" -3) (("2" (CASE-REPLACE "i!1 = low!2 + (j!1 + 1)") (("1" (HIDE -1 -2 -3 -5 -6 -7 -8 -9 2) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST -1 "low!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL))