|
%% 3-valued sign
%% Created by Cesar Munoz
sign3 : THEORY
BEGIN
IMPORTING sign,sq
Sign3 : TYPE = {i:int |i=1 OR i=-1 OR i=0}
sign3(x:real): Sign3 = IF x = 0 THEN 0
ELSIF x > 0 THEN 1
ELSE -1 ENDIF
eps,
eps1,eps2 : VAR Sign3
epsnz : VAR Sign
x,y,z : VAR real
sign3_mult_clos: JUDGEMENT *(eps1,eps2) HAS_TYPE Sign3
sign3_div_clos : JUDGEMENT /(eps,epsnz) HAS_TYPE Sign3
sign3_neg_clos : JUDGEMENT -(eps1) HAS_TYPE Sign3
sign3_sq_clos : JUDGEMENT sq(eps1) HAS_TYPE Sign3
sign3_sign : LEMMA x /= 0 IMPLIES sign3(x)=sign(x)
sign3_id : LEMMA sign3(eps) = eps
sign3_0 : LEMMA sign3(0) = 0
sign3_eq_1 : LEMMA x > 0 IMPLIES sign3(x) = 1
sign3_eq_neg1 : LEMMA x < 0 IMPLIES sign3(x) = -1
sign3_pos : LEMMA sign3(x)*x >= 0
sign3_abs : LEMMA abs(x) = sign3(x)*x
sign3_nneg : LEMMA sign3(x)*x >= 0
square_eps : LEMMA eps*eps <= 1
sq_eps : LEMMA sq(eps) <= 1
sq_sign3 : LEMMA sq(sign3(x)) <= 1
sign3_times_abs: LEMMA sign3(x)*abs(x) = x
abs_sign3 : LEMMA eps*x > 0 IMPLIES eps*x = abs(x)
sign3_neg : LEMMA -sign3(x) = sign3(-x)
sign3_minus : LEMMA -sign3(x-y) = sign3(y-x)
sign3_mult : LEMMA sign3(x*y) = sign3(x)*sign3(y)
sign3_div : LEMMA y /= 0 IMPLIES sign3(x/y) = sign3(x)*sign3(y)
sign3_mult_pos : LEMMA x > 0 IMPLIES sign3(x*y) = sign3(y)
sign3_div_pos1 : LEMMA x > 0 AND y /= 0 IMPLIES sign3(x/y) = sign3(y)
sign3_div_pos2 : LEMMA y > 0 IMPLIES sign3(x/y) = sign3(x)
sign3_mult_neg : LEMMA x < 0 IMPLIES sign3(x*y) = -sign3(y)
sign3_div_neg1 : LEMMA x < 0 AND y /= 0 IMPLIES sign3(x/y) = -sign3(y)
sign3_div_neg2 : LEMMA y < 0 IMPLIES sign3(x/y) = -sign3(x)
sign3_div_mult : LEMMA
y /= 0 IMPLIES sign3(x)/sign3(y) = sign3(x)*sign3(y)
sign3_and_abs : LEMMA sign3(x) = sign3(y) AND abs(x) = abs(y) IFF x = y
sign3_le : LEMMA
x <= y IMPLIES sign3(x) <= sign3(y)
sign3_ge : LEMMA
x >= y IMPLIES sign3(x) >= sign3(y)
AUTO_REWRITE+ sign3_0
END sign3
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
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.
|
