|
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
¤ Dauer der Verarbeitung: 0.19 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.
|
