| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle sq_rew.pvsSprache: 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
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-06-16) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09