|
% A better root when b is even
quadratic_2b : THEORY
BEGIN
IMPORTING quadratic
a : VAR nzreal
b,c : VAR real
x : VAR real
eps : VAR Sign
discr2b(a,b,c) : real = sq(b) - a*c
discr2b_discr : LEMMA
discr2b(a,b,c) = discr(a,2*b,c)/4
discr_discr2b : LEMMA
discr(a,b,c) = 4*discr2b(a,b/2,c)
discr2b_discr_eq_0 : LEMMA
discr2b(a,b,c) = 0 IFF discr(a,2*b,c) = 0
discr_discr2b_eq_0 : LEMMA
discr(a,b,c) = 0 IFF discr2b(a,b/2,c) = 0
discr2b_discr_ge_0 : LEMMA
discr2b(a,b,c) >= 0 IFF discr(a,2*b,c) >= 0
discr_discr2b_ge_0 : LEMMA
discr(a,b,c) >= 0 IFF discr2b(a,b/2,c) >= 0
discr2b_discr_gt_0 : LEMMA
discr2b(a,b,c) > 0 IFF discr(a,2*b,c) > 0
discr_discr2b_gt_0 : LEMMA
discr(a,b,c) > 0 IFF discr2b(a,b/2,c) > 0
root2b(a:nzreal,b:real,c:real|discr2b(a,b,c)>=0,eps:Sign):real =
(-b + eps*sqrt(discr2b(a,b,c)))/a
root2b_root : LEMMA
discr2b(a,b,c) >= 0 IMPLIES
root2b(a,b,c,eps) = root(a,2*b,c,eps)
root_root2b : LEMMA
discr(a,b,c) >= 0 IMPLIES
root(a,b,c,eps) = root2b(a,b/2,c,eps)
quad2b_eq_0 : THEOREM
quadratic(a,2*b,c)(x) = 0 IFF
discr2b(a,b,c) >= 0 AND
EXISTS (eps): x = root2b(a,b,c,eps)
END quadratic_2b
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
