% 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
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.
