%% 3-valued sign %% Created by Cesar Munoz THEORY BEGIN IMPORTING sign,sqTYPE = {i:int |i=1 OR i=-1 OR i=0} IF x = 0 THEN 0ELSIF x > 0 THEN 1ELSE -1 ENDIF VAR Sign3VAR Sign VAR realJUDGEMENT *(eps1,eps2) HAS_TYPE Sign3JUDGEMENT /(eps,epsnz) HAS_TYPE Sign3JUDGEMENT -(eps1) HAS_TYPE Sign3JUDGEMENT sq(eps1) HAS_TYPE Sign3LEMMA x /= 0 IMPLIES sign3(x)=sign(x)LEMMA sign3(eps) = epsLEMMA sign3(0) = 0LEMMA x > 0 IMPLIES sign3(x) = 1LEMMA x < 0 IMPLIES sign3(x) = -1LEMMA sign3(x)*x >= 0LEMMA abs(x) = sign3(x)*xLEMMA sign3(x)*x >= 0LEMMA eps*eps <= 1LEMMA sq(eps) <= 1LEMMA sq(sign3(x)) <= 1LEMMA sign3(x)*abs(x) = xLEMMA eps*x > 0 IMPLIES eps*x = abs(x)LEMMA -sign3(x) = sign3(-x)LEMMA -sign3(x-y) = sign3(y-x)LEMMA sign3(x*y) = sign3(x)*sign3(y)LEMMA y /= 0 IMPLIES sign3(x/y) = sign3(x)*sign3(y)LEMMA x > 0 IMPLIES sign3(x*y) = sign3(y)LEMMA x > 0 AND y /= 0 IMPLIES sign3(x/y) = sign3(y)LEMMA y > 0 IMPLIES sign3(x/y) = sign3(x)LEMMA x < 0 IMPLIES sign3(x*y) = -sign3(y)LEMMA x < 0 AND y /= 0 IMPLIES sign3(x/y) = -sign3(y)LEMMA y < 0 IMPLIES sign3(x/y) = -sign3(x)LEMMA IMPLIES sign3(x)/sign3(y) = sign3(x)*sign3(y)LEMMA sign3(x) = sign3(y) AND abs(x) = abs(y) IFF x = yLEMMA IMPLIES sign3(x) <= sign3(y)LEMMA IMPLIES sign3(x) >= sign3(y)END sign3quality 95%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
