| products/sources/formale Sprachen/Isabelle/Tools/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: .project Sprache: PVSUntersuchung PVS© |
|
||||||
|
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
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
