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