| products/sources/formale Sprachen/C/Lyx/po/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: ROOT Sprache: Unknown
|
sq: THEORY
BEGIN a,b,d: VAR real nna,nnb,nnc : VAR nonneg_real nz : VAR nzreal n : VAR nat sq(a): nonneg_real = a*a sq_nz_pos : JUDGEMENT sq(nz) HAS_TYPE posreal sq_rew : LEMMA a*a = sq(a) sq_expt2 : LEMMA sq(a) = a^2 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_abs : LEMMA sq(abs(a)) = sq(a) sq_abs_neg : LEMMA sq(abs(-a)) = sq(a) sq_0 : LEMMA sq(0) = 0 sq_1 : LEMMA sq(1) = 1 sq_eq_0 : LEMMA sq(a) = 0 IFF a = 0 sq_gt_0 : LEMMA sq(a) > 0 IFF a /= 0 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) AUTO_REWRITE- sq_neg_minus % -------------------- Inequalities -------------------- sq_ge : LEMMA sq(nna) >= sq(nnb) IFF nna >= nnb sq_le : LEMMA sq(nna) <= sq(nnb) IFF nna <= nnb sq_gt : LEMMA sq(nna) > sq(nnb) IFF nna > nnb sq_lt : LEMMA sq(nna) < sq(nnb) IFF nna < nnb sq_eq : LEMMA sq(nna) = sq(nnb) IFF nna = nnb sq_neg_pos_le : LEMMA sq(a) <= sq(nnc) IFF (-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) IFF (-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) IFF abs(a) <= abs(b) sq_lt_abs : LEMMA sq(a) < sq(b) IFF abs(a) < abs(b) sq_ge_abs : LEMMA sq(a) >= sq(b) IFF abs(a) >= abs(b) sq_gt_abs : LEMMA sq(a) > sq(b) IFF abs(a) > abs(b) sq_eq_abs : LEMMA sq(a) = sq(b) IFF abs(a) = abs(b) sq_eq_rew : LEMMA a = b IMPLIES sq(a) = sq(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 abs(a) < abs(d) AND abs(b) < abs(d) triangle_ineq_le : LEMMA sq(a) + sq(b) <= sq(d) IMPLIES abs(a) <= abs(d) AND abs(b) <= abs(d) AUTO_REWRITE+ sq_0 AUTO_REWRITE+ sq_1 AUTO_REWRITE+ sq_abs AUTO_REWRITE+ sq_abs_neg END sq [ Dauer der Verarbeitung: 0.6 Sekunden (vorverarbeitet) ] |