|
number_fields_sq: THEORY
BEGIN
IMPORTING number_fields_bis
a,b : VAR numfield
d,nz: VAR nznum
sq(a): numfield = a*a
sq_nz_pos : JUDGEMENT sq(nz) HAS_TYPE nznum
sq_rew : LEMMA a*a = sq(a)
sq_neg : LEMMA sq(-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_0 : LEMMA sq(0) = 0
sq_1 : LEMMA sq(1) = 1
sq_eq_0 : LEMMA sq(a) = 0 IFF a = 0
sq_div : LEMMA sq(a/nz) = sq(a)/sq(nz)
AUTO_REWRITE- sq_neg_minus
END number_fields_sq
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot
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
|
