Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sq.pvs Sprache: PVS

Original von: PVS^©

sq: THEORY
BEGIN

  a,b,d: VAR real
  nna,nnb,nnc : VAR nonneg_real
  nz          : VAR nzreal
  n           : VAR nat

  sq(a): nonneg_real = a*a

  sq_nz_pos         : JUDGEMENT sq(nz) HAS_TYPE posreal

  sq_rew            : LEMMA a*a = sq(a)

  sq_expt2          : LEMMA sq(a) = a^2

  sq_neg            : LEMMA sq(-a) = sq(a)

  sq_pos            : LEMMA sq(a) >= 0

  sq_plus_pos       : LEMMA sq(a)+sq(b) >= 0

  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_abs            : LEMMA sq(abs(a)) = sq(a)

  sq_abs_neg        : LEMMA sq(abs(-a)) = sq(a)

  sq_0              : LEMMA sq(0) = 0

  sq_1              : LEMMA sq(1) = 1

  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)

  AUTO_REWRITE-     sq_neg_minus

% -------------------- 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

  sq_neg_pos_le : LEMMA sq(a) <= sq(nnc) IFF (-nnc <= a AND a <= nnc)

  neg_pos_sq_le : LEMMA (-b <= a AND a <= b) IMPLIES sq(a) <= sq(b)

  sq_neg_pos_lt : LEMMA  sq(a) < sq(nnc) IFF (-nnc < a AND a < nnc)

  neg_pos_sq_lt : LEMMA (-b < a AND a < b) IMPLIES sq(a) < sq(b)

  sq_le_abs     : LEMMA sq(a) <= sq(b) IFF abs(a) <= abs(b)

  sq_lt_abs     : LEMMA sq(a) < sq(b) IFF abs(a) < abs(b)

  sq_ge_abs     : LEMMA sq(a) >= sq(b) IFF abs(a) >= abs(b)

  sq_gt_abs     : LEMMA sq(a) > sq(b) IFF abs(a) > abs(b)

  sq_eq_abs     : LEMMA sq(a) = sq(b) IFF abs(a) = abs(b)

  sq_eq_rew     : LEMMA a = b IMPLIES sq(a) = sq(b)

  %   |\
  %   | \ C <= c
  % A |  \
  %   +----
  %    B

  triangle_rectangle: LEMMA sq(a)+sq(b) <= sq(nnc) IMPLIES
                              -nnc <= a AND a <= nnc AND
                              -nnc <= b AND b <= nnc

  triangle_ineq_lt  : LEMMA sq(a) + sq(b) < sq(d) IMPLIES
                                  abs(a) < abs(d) AND
                                  abs(b) < abs(d)

  triangle_ineq_le  : LEMMA sq(a) + sq(b) <= sq(d) IMPLIES
                                  abs(a) <= abs(d) AND
                                  abs(b) <= abs(d)

  AUTO_REWRITE+ sq_0
  AUTO_REWRITE+ sq_1
  AUTO_REWRITE+ sq_abs
  AUTO_REWRITE+ sq_abs_neg

END sq

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.