Quelle  quadratic_2b.pvs

% 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