products/sources/formale sprachen/Delphi/Agenda 1.1 image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: min_max.pvs   Sprache: Unknown

% 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

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]