|
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.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
