Quelle sq.pvs Sprache: 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

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.