|
util : THEORY
BEGIN
IMPORTING reals@sign,
reals@sqrt
b,d : VAR nnreal
a,c,e : VAR real
% An algebraic way to determine a*sqrt(b) = e
eq(a,b,e) : bool =
a*e >= 0 AND sq(a)*b = sq(e)
eq_correct_1 : LEMMA
eq(a,b,e) IFF a*sqrt(b) = e
eq_neg : LEMMA
eq(-a,b,-e) = eq(a,b,e)
% An algebraic way to determine a*sqrt(b) > e
gt(a,b,e) : bool =
IF a >= 0 THEN
e < 0 OR sq(a)*b > sq(e)
ELSE
e < 0 AND sq(a)*b < sq(e)
ENDIF
gt_correct_1 : LEMMA
gt(a,b,e) IFF a*sqrt(b) > e
% An algebraic way to determine a*sqrt(b) < e
lt(a,b,e) : bool =
gt(-a,b,-e)
lt_correct_1 : LEMMA
lt(a,b,e) IFF a*sqrt(b) < e
% An algebraic way to determine a*sqrt(b) >= e
ge(a,b,e) : bool =
NOT lt(a,b,e)
ge_correct_1 : LEMMA
ge(a,b,e) IFF a*sqrt(b) >= e
% An algebraic way to determine a*sqrt(b) <= e
le(a,b,e) : bool =
NOT gt(a,b,e)
le_correct_1 : LEMMA
le(a,b,e) IFF a*sqrt(b) <= e
% An algebraic way to determine if a*sqrt(b) > c*sqrt(d)+e
gt(a,b,c,d,e) : bool =
IF a >= 0 THEN
lt(c,d,-e) OR lt(2*e*c,d,sq(a)*b-sq(c)*d-sq(e))
ELSE
lt(c,d,-e) AND gt(2*e*c,d,sq(a)*b-sq(c)*d-sq(e))
ENDIF
gt_correct_2 : LEMMA
gt(a,b,c,d,e) IFF a*sqrt(b) > c*sqrt(d)+e
% An algebraic way to determine a*sqrt(b) < c*sqrt(d)+e
lt(a,b,c,d,e) : bool =
gt(-a,b,-c,d,-e)
lt_correct_2 : LEMMA
lt(a,b,c,d,e) IFF a*sqrt(b) < c*sqrt(d)+e
% An algebraic way to determine a*sqrt(b) >= c*sqrt(d)+e
ge(a,b,c,d,e) : bool =
NOT lt(a,b,c,d,e)
ge_correct_2 : LEMMA
ge(a,b,c,d,e) IFF a*sqrt(b) >= c*sqrt(d)+e
% An algebraic way to determine a*sqrt(b) <= c*sqrt(d)+e
le(a,b,c,d,e) : bool =
NOT gt(a,b,c,d,e)
le_correct_2 : LEMMA
le(a,b,c,d,e) IFF a*sqrt(b) <= c*sqrt(d)+e
END util
¤ Dauer der Verarbeitung: 0.16 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.
|
