sq_rew: THEORY
BEGIN
IMPORTING sq
% sq_rew : LEMMA a*a = sq(a)
AUTO_REWRITE+ sq_neg % LEMMA sq(-a) = sq(a)
AUTO_REWRITE+ sq_0 % LEMMA sq(0) = 0
AUTO_REWRITE+ sq_1 % LEMMA sq(1) = 1
AUTO_REWRITE+ sq_abs % LEMMA sq(abs(a)) = sq(a)
AUTO_REWRITE+ sq_abs_neg % LEMMA sq(abs(-a)) = sq(a)
% 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_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)
% -------------------- 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
END sq_rew
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|