|
%
%
% Purpose : extra properties of absolute value
%
%
abs_props: THEORY
BEGIN
IMPORTING minmax_ineq
x, y: VAR real
nny: VAR nnreal
abs_max: LEMMA
abs(x) = max(-x,x)
abs_add: LEMMA
x*y >= 0 IMPLIES abs(x+y) = abs(x) + abs(y)
abs_le_nonneg: LEMMA
abs(x) <= nny IFF -nny <= x AND x <= nny
abs_diff_commutes: LEMMA abs(x-y) = abs(y-x) % from hacks
END abs_props
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
