|
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
¤ Dauer der Verarbeitung: 0.722 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
