Quelle min_max.pvs Sprache: PVS

% A few lemmas about min and max
min_max : THEORY
BEGIN

  nnx   : VAR nnreal
  npx   : VAR npreal
  x,y,z : VAR real
  px    : VAR posreal

  min_id : LEMMA
    min(x,x) = x

  max_id : LEMMA
    max(x,x) = x

  min_comm : LEMMA
    min(x,y) = min(y,x)

  max_nnreal_0 : LEMMA
    FORALL(x:nnreal): max(x,0) = x

  max_0_nnreal : LEMMA
    FORALL(x:nnreal): max(0,x) = x

  min_nnreal_0 : LEMMA
    FORALL(x:nnreal): min(x,0) = 0

  min_0_nnreal : LEMMA
    FORALL(x:nnreal): min(0,x) = 0

  min_npreal_0 : LEMMA
    FORALL(x:npreal): min(x,0) = x

  min_0_npreal : LEMMA
    FORALL(x:npreal): min(0,x) = x

  max_npreal_0 : LEMMA
    FORALL(x:npreal): max(x,0) = 0

  max_0_npreal : LEMMA
    FORALL(x:npreal): max(0,x) = 0

  max_comm : LEMMA
    max(x,y) = max(y,x)

  min_assoc : LEMMA
    min(min(x,y),z) = min(x,min(y,z))

  max_assoc : LEMMA
    max(max(x,y),z) = max(x,max(y,z))

  min_max_id : LEMMA
    min(x,y)+max(x,y) = x+y

  min_max : LEMMA
    min(x,y) = -max(-x,-y)

  max_min : LEMMA
    max(x,y) = -min(-x,-y)

  add_min : LEMMA
    z+min(x,y) = min(z+x,z+y)

  min_sub : LEMMA
    min(x,y)-z = min(x-z,y-z)

  sub_min : LEMMA
    z-min(x,y) = max(z-x,z-y)

  add_max : LEMMA
    z+max(x,y) = max(z+x,z+y)

  max_sub : LEMMA
    max(x,y)-z = max(x-z,y-z)

  sub_max : LEMMA
    z-max(x,y) = min(z-x,z-y)

  abs_max : LEMMA
    abs(x) = max(x,-x)

  abs_min : LEMMA
    abs(x) = -min(x,-x)

  max_abs : LEMMA
    max(x,y) = (x+y+abs(x-y))/2

  nneg_mult_min : LEMMA
    nnx*min(y,z) = min(nnx*y,nnx*z)

  npos_mult_min : LEMMA
    npx*min(y,z) = max(npx*y,npx*z)

  nneg_mult_max : LEMMA
    nnx*max(y,z) = max(nnx*y,nnx*z)

  npos_mult_max : LEMMA
    npx*max(y,z) = min(npx*y,npx*z)

  min_div_pos : LEMMA
    min(y,z)/px = min(y/px,z/px)

  max_div_pos : LEMMA
    max(y,z)/px = max(y/px,z/px)

  min_le_max_left : LEMMA
    min(max(x,y),z) <= max(min(x,y),z)

  min_le_max_right : LEMMA
    min(max(x,y),z) <= max(x,min(y,z))

  max_rec(F:[nat->real],j:nat,(k:nat|j<=k)): RECURSIVE {r:real|
    (EXISTS (i:nat): j<=i AND i<=k AND F(i)=r) AND
    (FORALL (i:nat): j<=i AND i<=k IMPLIES F(i)<=r)} =
    IF k = j THEN F(j) ELSE
    max(F(k),max_rec(F,j,k-1)) ENDIF
    MEASURE k

  min_rec(F:[nat->real],j:nat,(k:nat|j<=k)): RECURSIVE {r:real|
    (EXISTS (i:nat): j<=i AND i<=k AND F(i)=r) AND
    (FORALL (i:nat): j<=i AND i<=k IMPLIES F(i)>=r)} =
    IF k = j THEN F(j) ELSE
    min(F(k),min_rec(F,j,k-1)) ENDIF
    MEASURE k

  AUTO_REWRITE+ min_id
  AUTO_REWRITE+ max_id
  AUTO_REWRITE+ max_nnreal_0
  AUTO_REWRITE+ max_0_nnreal
  AUTO_REWRITE+ min_nnreal_0
  AUTO_REWRITE+ min_0_nnreal
  AUTO_REWRITE+ min_npreal_0
  AUTO_REWRITE+ min_0_npreal
  AUTO_REWRITE+ max_npreal_0
  AUTO_REWRITE+ max_0_npreal

END min_max

quality68%

¤ 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.