Wiki Agenda Contact English version

Floating-point computations with exponential and logarithm functions

These are examples of floating-point computations involving the exponential and the logarithm functions. They are presented in details in the technical report Generating and Certifying Accuracy Properties of Floating-Point Programs.

Auteurs: Claude Marché / Paul Bonnot

Catégories: Floating-Point Computations / Non-linear Arithmetic

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

download ZIP archive
The following provides the WhyML code where the programs are specified and implemented. After are given the prover results on each verification conditions. 
module ExpLogSingle
  use real.RealInfix
  use real.Abs
  use real.ExpLog
  use ufloat.USingle
  use ufloat.USingleLemmas

(* not easy to support
  constant log_max : real
  axiom exp_log_bounds: 1.0 <. log_max (* <=. ? *)
*)
  constant log_rel_err:real
  axiom log_rel_err_bounds : 0. <=. log_rel_err <=. 1.
  constant log_abs_err:real
  axiom log_abs_err_bounds : 0. <=. log_abs_err <=. 1.
  val function log_approx (x:usingle) : (r : usingle)
    requires { 0.0 <. to_real x }
(*    requires { 1.0 /. log_max <=. to_real x <=. log_max } *)
    ensures {
      abs (to_real r -. log (to_real x)) <=. abs (log (to_real x)) *. log_rel_err +. log_abs_err
    }

  constant log2_error:real
  axiom log2_error_bounds : 0. <=. log2_error <=. 1.
  val function log2_approx (x:usingle) : usingle
    requires { 0. <. to_real x }
    ensures {
      abs (to_real result -. log2 (to_real x)) <=. abs (log2 (to_real x)) *. log2_error
    }

  constant log10_error:real
  axiom log10_error_bounds : 0. <=. log10_error <=. 1.
  val function log10_approx (x:usingle) : usingle
    requires { 0. <. to_real x }
    ensures {
      abs (to_real result -. log10 (to_real x)) <=. abs (log10 (to_real x)) *. log10_error
    }

  constant exp_max : real
  axiom exp_max_bounds: 0.0 <. exp_max <=. 89.0 (* maximal reasonable bound for single format *)
  constant exp_rel_err:real
  axiom exp_rel_err_bounds : 0. <=. exp_rel_err <=. 0.5
  val function exp_approx (x:usingle) : usingle
    requires { abs (to_real x) <=. exp_max }
    ensures {
      abs (to_real result -. exp (to_real x)) <=. exp_rel_err *. exp (to_real x)
    }

  let example1 (x y : usingle) : (r : usingle)
    requires { abs (to_real x) <=. exp_max }
    requires { abs (to_real y) <=. exp_max }
    ensures {
    let t = log (exp (to_real y)) in
    let t1 = log (exp (to_real x)) in
    let t2 =
      ((1.0 +. eps) +. log_rel_err)
      *. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err))
          +. log_abs_err)
    in
    abs (to_real r -. (t1 +. t))
    <=. ((((log_rel_err +. log_rel_err) +. eps) *. (abs t1 +. abs t))
         +. (t2 +. t2))
    }
  = log_approx (exp_approx(x)) ++. log_approx (exp_approx(y))

  let example2 (x y : usingle) : (r : usingle)
    requires { exp_rel_err <=. 0x1p-2 }
    requires { abs (to_real x) <=. exp_max }
    requires { abs (to_real y) <=. exp_max }
    ensures {
      let exact = log(exp(to_real x) +. exp (to_real y)) in
      abs (to_real r -. exact)
      <=. abs exact *. log_rel_err
         +. ((-. log (1.0 -. ((2. *. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err
    }
  = log_approx (exp_approx(x) ++. exp_approx(y))

  let example3 (x y : usingle) : (r : usingle)
    requires { 0. <. to_real x }
    requires { 0. <. to_real y }
    ensures {
      let exact = log2(to_real x +. to_real y) in
      abs (to_real r -. exact)
      <=. abs exact *. log2_error
         +. ((-. log2 (1.0 -. (eps))) *. (1.0 +. log2_error))
    }
  = log2_approx (x ++. y)

  let example4 (x y : usingle) : (r : usingle)
    requires { 0. <. to_real x }
    requires { 0. <. to_real y }
    ensures {
      let exact = log10(to_real x +. to_real y) in
      abs (to_real r -. exact)
      <=. abs exact *. log10_error
         +. ((-. log10 (1.0 -. (eps))) *. (1.0 +. log10_error))
    }
  = log10_approx (x ++. y)

end

module ExpLogDouble
  use real.RealInfix
  use real.Abs
  use real.ExpLog
  use ufloat.UDouble
  use ufloat.UDoubleLemmas

  constant log_rel_err:real
  axiom log_rel_err_bounds : 0. <=. log_rel_err <=. 1.
  constant log_abs_err:real
  axiom log_abs_err_bounds : 0. <=. log_abs_err <=. 1.
  val function log_approx (x:udouble) : (r : udouble)
    requires { 0. <. to_real x }
    ensures {
      abs (to_real r -. log (to_real x)) <=. abs (log (to_real x)) *. log_rel_err +. log_abs_err
    }

  constant exp_max : real
  axiom exp_max_bounds: 0.0 <. exp_max <=. 708.0 (* maximal reasonable bound for double format *)
  constant exp_rel_err:real
  axiom exp_rel_err_bounds : 0. <=. exp_rel_err <=. 0.5
  val function exp_approx (x:udouble) : (r : udouble)
    requires { abs (to_real x) <=. exp_max }
    ensures {
      abs (to_real r -. exp (to_real x)) <=. exp_rel_err *. exp (to_real x)
    }

  let lemma exp_approx_pos (x:udouble)
    requires { abs (to_real x) <=. exp_max }
    ensures { to_real (exp_approx x) >. 0.0 }
  = ()

  let example1 (x y : udouble) : (r : udouble)
    requires { abs (to_real x) <=. exp_max }
    requires { abs (to_real y) <=. exp_max }
    ensures {
    let t = log (exp (to_real y)) in
    let t1 = log (exp (to_real x)) in
    let t2 =
      ((1.0 +. eps) +. log_rel_err)
      *. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err))
          +. log_abs_err)
    in
    abs (to_real r -. (t1 +. t))
    <=. ((((log_rel_err +. log_rel_err) +. eps) *. (abs t1 +. abs t))
         +. (t2 +. t2))
    }
  = log_approx (exp_approx(x)) ++. log_approx (exp_approx(y))

  let example2 (x y : udouble) : (r : udouble)
    requires { exp_rel_err <=. 0x1p-2 }
    requires { abs (to_real x) <=. exp_max }
    requires { abs (to_real y) <=. exp_max }
    ensures {
      let exact = log(exp(to_real x) +. exp (to_real y)) in
      abs (to_real r -. exact)
      <=. abs exact *. log_rel_err
         +. ((-. log (1.0 -. ((2. *. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err
    }
  = log_approx (exp_approx(x) ++. exp_approx(y))

  let lse4 (x1 x2 x3 x4 : udouble) : (r : udouble)
   requires { exp_rel_err <=. 0x1p-3 }
   requires { abs (to_real x1) <=. exp_max }
   requires { abs (to_real x2) <=. exp_max }
   requires { abs (to_real x3) <=. exp_max }
   requires { abs (to_real x4) <=. exp_max }
   ensures {
      let exact =
        log (exp (to_real x1) +. exp (to_real x2) +.
             exp (to_real x3) +. exp (to_real x4))
      in
      abs (to_real r -. exact)
      <=. abs exact *. log_rel_err
          -. log (1.0 -. (4.0 *. exp_rel_err +. 3.0 *. eps))
             *. (1.0 +. log_rel_err)
          +. log_abs_err
          }
  = log_approx (exp_approx(x1) ++. exp_approx(x2) ++. exp_approx(x3) ++. exp_approx(x4))

  let lse5 (x1 x2 x3 x4 x5: udouble) : (r : udouble)
    requires { exp_rel_err <=. 0x1p-3 }
    requires { abs (to_real x1) <=. exp_max }
    requires { abs (to_real x2) <=. exp_max }
    requires { abs (to_real x3) <=. exp_max }
    requires { abs (to_real x4) <=. exp_max }
    requires { abs (to_real x5) <=. exp_max }
    ensures {
      let exact =
        log (exp (to_real x1) +. exp (to_real x2) +.
             exp (to_real x3) +. exp (to_real x4) +. exp (to_real x5))
      in
      abs (to_real r -. exact)
      <=. abs exact *. log_rel_err
          -. log (1.0 -. (5.0 *. exp_rel_err +. 4.0 *. eps))
             *. (1.0 +. log_rel_err)
          +. log_abs_err
          }
  = log_approx (exp_approx(x1) ++. exp_approx(x2) ++. exp_approx(x3)
                ++. exp_approx(x4) ++. exp_approx(x5))

let lse6 (x1 x2 x3 x4 x5 x6 : udouble) : (r : udouble)
    requires { exp_rel_err <=. 0x1p-6 }
    requires { abs (to_real x1) <=. exp_max }
    requires { abs (to_real x2) <=. exp_max }
    requires { abs (to_real x3) <=. exp_max }
    requires { abs (to_real x4) <=. exp_max }
    requires { abs (to_real x5) <=. exp_max }
    requires { abs (to_real x6) <=. exp_max }
    ensures {
      let exact =
        log (exp (to_real x1) +. exp (to_real x2) +.
             exp (to_real x3) +. exp (to_real x4) +. exp (to_real x5)
             +. exp (to_real x6) )
      in
      abs (to_real r -. exact)
      <=. abs exact *. log_rel_err
          -. log (1.0 -. (6.0 *. exp_rel_err +. 5.0 *. eps))
             *. (1.0 +. log_rel_err)
          +. log_abs_err
    }

  = log_approx (exp_approx(x1) ++. exp_approx(x2) ++. exp_approx(x3)
                ++. exp_approx(x4) ++. exp_approx(x5) ++.
                exp_approx(x6))

let lse7 (x1 x2 x3 x4 x5 x6 x7 : udouble) : (r :udouble)
    requires { exp_rel_err <=. 0x1p-3 }
    requires { abs (to_real x1) <=. exp_max }
    requires { abs (to_real x2) <=. exp_max }
    requires { abs (to_real x3) <=. exp_max }
    requires { abs (to_real x4) <=. exp_max }
    requires { abs (to_real x5) <=. exp_max }
    requires { abs (to_real x6) <=. exp_max }
    requires { abs (to_real x7) <=. exp_max }
    ensures {
      let exact =
        log (exp (to_real x1) +. exp (to_real x2) +.
             exp (to_real x3) +. exp (to_real x4) +. exp (to_real x5)
             +. exp (to_real x6) +. exp (to_real x7) )
      in
      abs (to_real r -. exact)
      <=. abs exact *. log_rel_err
          -. log (1.0 -. (7.0 *. exp_rel_err +. 6.0 *. eps))
             *. (1.0 +. log_rel_err)
          +. log_abs_err
          }
  = log_approx (exp_approx(x1) ++. exp_approx(x2) ++. exp_approx(x3)
                ++. exp_approx(x4) ++. exp_approx(x5) ++.
                exp_approx(x6) ++. exp_approx(x7))

let lse8 (x1 x2 x3 x4 x5 x6 x7 x8 : udouble) : (r :udouble)
    requires { exp_rel_err <=. 0x1p-4 }
    requires { abs (to_real x1) <=. exp_max }
    requires { abs (to_real x2) <=. exp_max }
    requires { abs (to_real x3) <=. exp_max }
    requires { abs (to_real x4) <=. exp_max }
    requires { abs (to_real x5) <=. exp_max }
    requires { abs (to_real x6) <=. exp_max }
    requires { abs (to_real x7) <=. exp_max }
    requires { abs (to_real x8) <=. exp_max }
    ensures {
      let exact =
        log (exp (to_real x1) +. exp (to_real x2) +.
             exp (to_real x3) +. exp (to_real x4) +. exp (to_real x5)
             +. exp (to_real x6) +. exp (to_real x7) +.
             exp (to_real x8) )
      in
      abs (to_real r -. exact)
      <=. abs exact *. log_rel_err
          -. log (1.0 -. (8.0 *. exp_rel_err +. 7.0 *. eps))
             *. (1.0 +. log_rel_err)
          +. log_abs_err
          }
  = log_approx (exp_approx(x1) ++. exp_approx(x2) ++. exp_approx(x3)
                ++. exp_approx(x4) ++. exp_approx(x5) ++.
                exp_approx(x6) ++. exp_approx(x7) ++. exp_approx(x8))

  let lse10 (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10: udouble) : (r : udouble)
    requires { exp_rel_err <=. 0x1p-4 }
    requires { abs (to_real x1) <=. exp_max }
    requires { abs (to_real x2) <=. exp_max }
    requires { abs (to_real x3) <=. exp_max }
    requires { abs (to_real x4) <=. exp_max }
    requires { abs (to_real x5) <=. exp_max }
    requires { abs (to_real x6) <=. exp_max }
    requires { abs (to_real x7) <=. exp_max }
    requires { abs (to_real x8) <=. exp_max }
    requires { abs (to_real x9) <=. exp_max }
    requires { abs (to_real x10) <=. exp_max }
    ensures {
      let exact =
        log (exp (to_real x1) +. exp (to_real x2) +.
             exp (to_real x3) +. exp (to_real x4) +. exp (to_real x5)
             +. exp (to_real x6) +. exp (to_real x7) +.
             exp (to_real x8) +. exp (to_real x9) +. exp (to_real x10))
      in
      abs (to_real r -. exact)
      <=. abs exact *. log_rel_err
          -. log (1.0 -. (10.0 *. exp_rel_err +. 9.0 *. eps))
             *. (1.0 +. log_rel_err)
          +. log_abs_err
          }
  = let s  = exp_approx(x1) ++. exp_approx(x2) ++. exp_approx(x3)
                ++. exp_approx(x4) ++. exp_approx(x5) ++.
                exp_approx(x6) ++. exp_approx(x7) ++. exp_approx(x8)
                ++. exp_approx(x9) ++. exp_approx(x10) in
    assert { to_real s >. 0.0 };
    log_approx s

log in base 2 and 10

  constant log2_rel_error:real
  axiom log2_rel_error_bounds : 0. <=. log2_rel_error <=. 1.
  constant log2_abs_error:real
  axiom log2_abs_error_bounds : 0. <=. log2_abs_error <=. 1.
  val function log2_approx (x:udouble) : udouble
    requires { 0. <. to_real x }
    ensures {
      abs (to_real result -. log2 (to_real x)) <=.
        abs (log2 (to_real x)) *. log2_rel_error +. log2_abs_error
    }

  constant log10_error:real
  axiom log10_error_bounds : 0. <=. log10_error <=. 1.
  val function log10_approx (x:udouble) : udouble
    requires { 0. <. to_real x }
    ensures {
      abs (to_real result -. log10 (to_real x)) <=. abs (log10 (to_real x)) *. log10_error
    }

  let example3 (x y : udouble) : (r : udouble)
    requires { 0. <. to_real x }
    requires { 0. <. to_real y }
    ensures {
      let exact = log2(to_real x +. to_real y) in
      abs (to_real r -. exact)
      <=. abs exact *. log2_rel_error
         +. (-. log2 (1.0 -. (eps))) *. (1.0 +. log2_rel_error)
         +. log2_abs_error
    }
  = log2_approx (x ++. y)

  let example4 (x y : udouble) : (r :udouble)
    requires { 0. <. to_real x }
    requires { 0. <. to_real y }
    ensures {
      let exact = log10(to_real x +. to_real y) in
      abs (to_real r -. exact)
      <=. abs exact *. log10_error
         +. ((-. log10 (1.0 -. (eps))) *. (1.0 +. log10_error))
    }
  = log10_approx (x ++. y)

end
The following table lists all the verification conditions generated and tell which prover proved which.

Why3 Proof Results for Project "exp_log"

Theory "exp_log.ExpLogSingle": fully verified

ObligationsAlt-Ergo 2.6.2CVC4 1.8CVC5 1.2.0Z3 4.13.2
VC for example1------------
split_vc
precondition------0.04---
precondition0.15---------
precondition---------0.01
precondition0.21---------
postcondition------------
assert let t3 = log (exp (to_real y)) in let t4 = log (exp (to_real x)) in let t5 = ((1.0 +. eps) +. log_rel_err) *. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err) in abs (to_real r -. (t4 +. t3)) <=. ((((log_rel_err +. log_rel_err) +. eps) *. (abs t4 +. abs t3)) +. (t5 +. t5))
asserted formula------------
assert abs (to_real r -. (log (exp (to_real x)) +. log (exp (to_real y)))) <=. ((((log_rel_err +. log_rel_err) +. eps) *. (abs (log (exp (to_real x))) +. abs (log (exp (to_real y))))) +. ((((1.0 +. eps) +. log_rel_err) *. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err)) +. (((1.0 +. eps) +. log_rel_err) *. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err))))
asserted formula------------
apply uadd_single_error_propagation with log_approx (exp_approx x),log_approx (exp_approx y)
apply premises------------
assert abs (to_real (log_approx (exp_approx x)) -. log (exp (to_real x))) <=. ((abs (log (exp (to_real x))) *. log_rel_err) +. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real (log_approx (exp_approx x)) -. log (exp (to_real x))) <=. ((log_rel_err *. abs (log (exp (to_real x)))) +. (((-. log (1.0 -. (((exp_rel_err *. exp (to_real x)) +. 0.0) /. exp (to_real x)))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_single_error_propagation with exp_approx x
apply premises------0.05---
apply premises------0.04---
apply premises------0.12---
apply premises0.17---------
apply premises------0.07---
asserted formula1.79---------
apply premises0.08---------
apply premises------------
assert abs (to_real (log_approx (exp_approx y)) -. log (exp (to_real y))) <=. ((abs (log (exp (to_real y))) *. log_rel_err) +. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real (log_approx (exp_approx y)) -. log (exp (to_real y))) <=. ((log_rel_err *. abs (log (exp (to_real y)))) +. (((-. log (1.0 -. (((exp_rel_err *. exp (to_real y)) +. 0.0) /. exp (to_real y)))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_single_error_propagation with exp_approx y
apply premises------0.05---
apply premises0.08---------
apply premises------0.14---
apply premises0.28---------
apply premises------0.07---
asserted formula1.51---------
apply premises---------0.01
apply premises0.04---------
apply premises---0.06------
apply premises0.05---------
apply premises------0.04---
apply premises0.24---------
apply premises0.17---------
apply premises------0.07---
asserted formula------0.04---
postcondition0.11---------
VC for example2------------
split_vc
precondition------0.04---
precondition---------0.01
precondition0.25---------
postcondition------------
assert let t = log (exp (to_real x) +. exp (to_real y)) in abs (to_real r -. t) <=. ((abs t *. log_rel_err) +. (((-. log (1.0 -. ((exp_rel_err +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (exp (to_real x) +. exp (to_real y))) <=. ((abs (log (exp (to_real x) +. exp (to_real y))) *. log_rel_err) +. (((-. log (1.0 -. ((exp_rel_err +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (exp (to_real x) +. exp (to_real y))) <=. ((log_rel_err *. abs (log (exp (to_real x) +. exp (to_real y)))) +. (((-. log (1.0 -. (((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x) +. exp (to_real y))) +. 0.0) /. (exp (to_real x) +. exp (to_real y))))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_single_error_propagation with exp_approx x ++. exp_approx y
apply premises------------
assert abs (to_real (exp_approx x ++. exp_approx y) -. (exp (to_real x) +. exp (to_real y))) <=. ((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x) +. exp (to_real y))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. exp_rel_err) *. 0.0)))
asserted formula------------
apply uadd_single_error_propagation with exp_approx x,exp_approx y
apply premises------0.07---
apply premises0.07---------
apply premises0.22---------
apply premises------0.14---
apply premises---------0.01
apply premises---------0.02
apply premises------0.06---
apply premises0.04---------
apply premises---------0.01
apply premises------0.05---
apply premises---------0.01
apply premises0.21---------
apply premises0.27---------
apply premises---0.08------
asserted formula1.41---------
asserted formula0.05---------
postcondition---------0.01
VC for example3------------
split_vc
precondition0.13---------
postcondition------------
assert let t = log2 (to_real x +. to_real y) in abs (to_real r -. t) <=. ((abs t *. log2_error) +. ((-. log2 (1.0 -. eps)) *. (1.0 +. log2_error)))
asserted formula------------
assert abs (to_real r -. log2 (to_real x +. to_real y)) <=. ((abs (log2 (to_real x +. to_real y)) *. log2_error) +. ((-. log2 (1.0 -. eps)) *. (1.0 +. log2_error)))
asserted formula------------
assert abs (to_real r -. log2 (to_real x +. to_real y)) <=. ((log2_error *. abs (log2 (to_real x +. to_real y))) +. (((-. log2 (1.0 -. (((eps *. abs (to_real x +. to_real y)) +. 0.0) /. (to_real x +. to_real y)))) *. (1.0 +. log2_error)) +. 0.0))
asserted formula------------
apply log2_single_error_propagation with x ++. y
apply premises------------
assert abs (to_real (x ++. y) -. (to_real x +. to_real y)) <=. (eps *. abs (to_real x +. to_real y))
asserted formula0.10---------
apply premises------0.06---
apply premises---------0.01
apply premises------0.06---
apply premises------0.05---
apply premises------0.04---
asserted formula0.06---------
asserted formula---------0.02
postcondition0.06---------
VC for example4------------
split_vc
precondition0.09---------
postcondition------------
assert let t = log10 (to_real x +. to_real y) in abs (to_real r -. t) <=. ((abs t *. log10_error) +. ((-. log10 (1.0 -. eps)) *. (1.0 +. log10_error)))
asserted formula------------
assert abs (to_real r -. log10 (to_real x +. to_real y)) <=. ((abs (log10 (to_real x +. to_real y)) *. log10_error) +. ((-. log10 (1.0 -. eps)) *. (1.0 +. log10_error)))
asserted formula------------
assert abs (to_real r -. log10 (to_real x +. to_real y)) <=. ((log10_error *. abs (log10 (to_real x +. to_real y))) +. (((-. log10 (1.0 -. (((eps *. abs (to_real x +. to_real y)) +. 0.0) /. (to_real x +. to_real y)))) *. (1.0 +. log10_error)) +. 0.0))
asserted formula------------
apply log10_single_error_propagation with x ++. y
apply premises------------
assert abs (to_real (x ++. y) -. (to_real x +. to_real y)) <=. (eps *. abs (to_real x +. to_real y))
asserted formula0.11---------
apply premises------0.04---
apply premises---0.06------
apply premises0.04---------
apply premises0.05---------
apply premises---0.08------
asserted formula0.08---------
asserted formula------0.07---
postcondition------0.06---

Theory "exp_log.ExpLogDouble": fully verified

ObligationsAlt-Ergo 2.6.2CVC4 1.8CVC5 1.2.0Z3 4.13.2
VC for exp_approx_pos1.45---------
VC for example1------------
split_vc
precondition------0.07---
precondition0.04---------
precondition0.08---------
precondition0.24---------
postcondition------------
assert let t3 = log (exp (to_real y)) in let t4 = log (exp (to_real x)) in let t5 = ((1.0 +. eps) +. log_rel_err) *. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err) in abs (to_real r -. (t4 +. t3)) <=. ((((log_rel_err +. log_rel_err) +. eps) *. (abs t4 +. abs t3)) +. (t5 +. t5))
asserted formula------------
assert abs (to_real r -. (log (exp (to_real x)) +. log (exp (to_real y)))) <=. ((((log_rel_err +. log_rel_err) +. eps) *. (abs (log (exp (to_real x))) +. abs (log (exp (to_real y))))) +. ((((1.0 +. eps) +. log_rel_err) *. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err)) +. (((1.0 +. eps) +. log_rel_err) *. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err))))
asserted formula------------
apply uadd_double_error_propagation with log_approx (exp_approx x),log_approx (exp_approx y)
apply premises------------
assert abs (to_real (log_approx (exp_approx x)) -. log (exp (to_real x))) <=. ((abs (log (exp (to_real x))) *. log_rel_err) +. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real (log_approx (exp_approx x)) -. log (exp (to_real x))) <=. ((log_rel_err *. abs (log (exp (to_real x)))) +. (((-. log (1.0 -. (((exp_rel_err *. exp (to_real x)) +. 0.0) /. exp (to_real x)))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with exp_approx x
apply premises---------0.02
apply premises------0.08---
apply premises------0.23---
apply premises0.28---------
apply premises0.07---------
asserted formula1.71---------
apply premises------0.05---
apply premises------------
assert abs (to_real (log_approx (exp_approx y)) -. log (exp (to_real y))) <=. ((abs (log (exp (to_real y))) *. log_rel_err) +. (((-. log (1.0 -. exp_rel_err)) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real (log_approx (exp_approx y)) -. log (exp (to_real y))) <=. ((log_rel_err *. abs (log (exp (to_real y)))) +. (((-. log (1.0 -. (((exp_rel_err *. exp (to_real y)) +. 0.0) /. exp (to_real y)))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with exp_approx y
apply premises---------0.02
apply premises0.07---------
apply premises0.26---------
apply premises0.22---------
apply premises0.05---------
asserted formula2.07---------
apply premises0.07---------
apply premises------0.05---
apply premises0.06---------
apply premises------0.05---
apply premises------0.05---
apply premises0.26---------
apply premises0.20---------
apply premises------0.05---
asserted formula------0.08---
postcondition------0.05---
VC for example2------------
split_vc
precondition0.09---------
precondition---------0.01
precondition0.35---------
postcondition------------
assert let t = log (exp (to_real x) +. exp (to_real y)) in abs (to_real r -. t) <=. ((abs t *. log_rel_err) +. (((-. log (1.0 -. ((exp_rel_err +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (exp (to_real x) +. exp (to_real y))) <=. ((abs (log (exp (to_real x) +. exp (to_real y))) *. log_rel_err) +. (((-. log (1.0 -. ((exp_rel_err +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (exp (to_real x) +. exp (to_real y))) <=. ((log_rel_err *. abs (log (exp (to_real x) +. exp (to_real y)))) +. (((-. log (1.0 -. (((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x) +. exp (to_real y))) +. 0.0) /. (exp (to_real x) +. exp (to_real y))))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with exp_approx x ++. exp_approx y
apply premises------------
assert abs (to_real (exp_approx x ++. exp_approx y) -. (exp (to_real x) +. exp (to_real y))) <=. ((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x) +. exp (to_real y))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. exp_rel_err) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x,exp_approx y
apply premises---------0.02
apply premises0.08---------
apply premises0.17---------
apply premises------0.21---
apply premises------0.05---
apply premises------0.07---
apply premises------0.05---
apply premises---------0.02
apply premises---0.11------
apply premises------0.07---
apply premises---------0.02
apply premises0.15---------
apply premises0.20---------
apply premises---------0.01
asserted formula1.97---------
asserted formula------0.04---
postcondition0.06---------
VC for lse4------------
split_vc
precondition------0.04---
precondition---------0.01
precondition---------0.01
precondition------0.05---
precondition1.89---------
postcondition------------
assert let t = log (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) in abs (to_real r -. t) <=. ((abs t *. log_rel_err) +. (((-. log (1.0 -. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) <=. ((abs (log (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) *. log_rel_err) +. (((-. log (1.0 -. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) <=. ((log_rel_err *. abs (log (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)))) +. (((-. log (1.0 -. (((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) +. 0.0) /. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4
apply premises------------
assert abs (to_real (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) -. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) <=. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (exp_approx x1 ++. exp_approx x2) ++. exp_approx x3,exp_approx x4
apply premises------------
assert abs (to_real ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) -. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) <=. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((exp_rel_err +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1 ++. exp_approx x2,exp_approx x3
apply premises------------
assert abs (to_real (exp_approx x1 ++. exp_approx x2) -. (exp (to_real x1) +. exp (to_real x2))) <=. ((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x1) +. exp (to_real x2))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. exp_rel_err) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1,exp_approx x2
apply premises------0.07---
apply premises------0.07---
apply premises------0.26---
apply premises------0.31---
apply premises0.06---------
apply premises------0.05---
apply premises---------0.01
apply premises------0.04---
apply premises0.06---------
apply premises---------0.02
apply premises---------0.02
apply premises0.31---------
apply premises------0.26---
apply premises---------0.05
apply premises------0.06---
apply premises---------0.01
apply premises------0.05---
apply premises0.08---------
apply premises------0.05---
apply premises0.07---------
apply premises0.35---------
apply premises------0.20---
apply premises------0.06---
apply premises------0.05---
apply premises---------0.02
apply premises------0.05---
apply premises0.06---------
apply premises------0.05---
apply premises------0.05---
apply premises0.29---------
apply premises0.36---------
apply premises---------0.01
asserted formula3.75---------
asserted formula------0.09---
postcondition------0.05---
VC for lse5------------
split_vc
precondition---------0.01
precondition------0.04---
precondition------0.04---
precondition------0.05---
precondition------0.05---
precondition5.00---------
postcondition------------
assert let t = log ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) in abs (to_real r -. t) <=. ((abs t *. log_rel_err) +. (((-. log (1.0 -. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) <=. ((abs (log ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) *. log_rel_err) +. (((-. log (1.0 -. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) <=. ((log_rel_err *. abs (log ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)))) +. (((-. log (1.0 -. (((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) +. 0.0) /. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5
apply premises------------
assert abs (to_real ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) -. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) <=. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4,exp_approx x5
apply premises------------
assert abs (to_real (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) -. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) <=. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (exp_approx x1 ++. exp_approx x2) ++. exp_approx x3,exp_approx x4
apply premises------------
assert abs (to_real ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) -. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) <=. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((exp_rel_err +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1 ++. exp_approx x2,exp_approx x3
apply premises------------
assert abs (to_real (exp_approx x1 ++. exp_approx x2) -. (exp (to_real x1) +. exp (to_real x2))) <=. ((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x1) +. exp (to_real x2))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. exp_rel_err) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1,exp_approx x2
apply premises------0.05---
apply premises------0.05---
apply premises------0.27---
apply premises------0.27---
apply premises------0.04---
apply premises------0.07---
apply premises------0.05---
apply premises------0.07---
apply premises------0.06---
apply premises------0.07---
apply premises------0.06---
apply premises0.31---------
apply premises------0.22---
apply premises0.07---------
apply premises---------0.02
apply premises---------0.02
apply premises---0.09------
apply premises------0.05---
apply premises------0.05---
apply premises------0.05---
apply premises0.28---------
apply premises------0.29---
apply premises---------0.04
apply premises0.09---------
apply premises------0.05---
apply premises0.09---------
apply premises0.07---------
apply premises------0.05---
apply premises------0.05---
apply premises0.32---------
apply premises------0.18---
apply premises---------0.03
apply premises0.08---------
apply premises------0.08---
apply premises------0.07---
apply premises------0.05---
apply premises------0.05---
apply premises------0.05---
apply premises0.26---------
apply premises0.44---------
apply premises---------0.01
asserted formula4.13---------
asserted formula------0.05---
postcondition------0.05---
VC for lse6------------
split_vc
precondition------0.05---
precondition------0.07---
precondition0.07---------
precondition------0.07---
precondition0.06---------
precondition------0.09---
precondition7.91---------
postcondition------------
assert let t = log (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) in abs (to_real r -. t) <=. ((abs t *. log_rel_err) +. (((-. log (1.0 -. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) <=. ((abs (log (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) *. log_rel_err) +. (((-. log (1.0 -. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) <=. ((log_rel_err *. abs (log (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)))) +. (((-. log (1.0 -. (((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) +. 0.0) /. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6
apply premises------------
assert abs (to_real (((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) -. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) <=. ((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5,exp_approx x6
apply premises------------
assert abs (to_real ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) -. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) <=. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4,exp_approx x5
apply premises------------
assert abs (to_real (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) -. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) <=. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (exp_approx x1 ++. exp_approx x2) ++. exp_approx x3,exp_approx x4
apply premises------------
assert abs (to_real ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) -. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) <=. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((exp_rel_err +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1 ++. exp_approx x2,exp_approx x3
apply premises------------
assert abs (to_real (exp_approx x1 ++. exp_approx x2) -. (exp (to_real x1) +. exp (to_real x2))) <=. ((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x1) +. exp (to_real x2))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. exp_rel_err) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1,exp_approx x2
apply premises------0.05---
apply premises------0.05---
apply premises------0.26---
apply premises0.26---------
apply premises---------0.02
apply premises---0.11------
apply premises------0.07---
apply premises---------0.02
apply premises---------0.02
apply premises------0.05---
apply premises---------0.02
apply premises0.30---------
apply premises------0.24---
apply premises0.08---------
apply premises------0.05---
apply premises------0.05---
apply premises------0.08---
apply premises------0.07---
apply premises------0.05---
apply premises0.07---------
apply premises0.34---------
apply premises------0.31---
apply premises---------0.05
apply premises---------0.02
apply premises---------0.02
apply premises------0.08---
apply premises0.07---------
apply premises0.10---------
apply premises------0.07---
apply premises0.41---------
apply premises------0.20---
apply premises---------0.04
apply premises------0.06---
apply premises---------0.02
apply premises------0.05---
apply premises------0.05---
apply premises------0.05---
apply premises------0.05---
apply premises0.39---------
apply premises------0.33---
apply premises---------0.04
apply premises0.08---------
apply premises------0.07---
apply premises------0.08---
apply premises------0.06---
apply premises------0.07---
apply premises------0.06---
apply premises0.28---------
apply premises0.51---------
apply premises------0.07---
asserted formula3.71---------
asserted formula------0.05---
postcondition------0.05---
VC for lse7------------
split_vc
precondition------0.04---
precondition0.08---------
precondition------0.05---
precondition------0.09---
precondition---------0.01
precondition------0.05---
precondition------0.04---
precondition5.31---------
postcondition------------
assert let t = log ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) in abs (to_real r -. t) <=. ((abs t *. log_rel_err) +. (((-. log (1.0 -. ((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) <=. ((abs (log ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) *. log_rel_err) +. (((-. log (1.0 -. ((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) <=. ((log_rel_err *. abs (log ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)))) +. (((-. log (1.0 -. (((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) +. 0.0) /. ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with (((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7
apply premises------------
assert abs (to_real ((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) -. ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) <=. ((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6,exp_approx x7
apply premises------------
assert abs (to_real (((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) -. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) <=. ((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5,exp_approx x6
apply premises------------
assert abs (to_real ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) -. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) <=. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4,exp_approx x5
apply premises------------
assert abs (to_real (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) -. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) <=. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (exp_approx x1 ++. exp_approx x2) ++. exp_approx x3,exp_approx x4
apply premises------------
assert abs (to_real ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) -. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) <=. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((exp_rel_err +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1 ++. exp_approx x2,exp_approx x3
apply premises------------
assert abs (to_real (exp_approx x1 ++. exp_approx x2) -. (exp (to_real x1) +. exp (to_real x2))) <=. ((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x1) +. exp (to_real x2))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. exp_rel_err) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1,exp_approx x2
apply premises------0.05---
apply premises------0.05---
apply premises------0.31---
apply premises------0.21---
apply premises---------0.01
apply premises------0.06---
apply premises---------0.01
apply premises------0.04---
apply premises------0.05---
apply premises------0.05---
apply premises------0.05---
apply premises0.46---------
apply premises------0.24---
apply premises---------0.06
apply premises------0.08---
apply premises------0.05---
apply premises---------0.02
apply premises------0.06---
apply premises------0.05---
apply premises---------0.01
apply premises0.32---------
apply premises------0.21---
apply premises---------0.05
apply premises------0.05---
apply premises---------0.01
apply premises------0.05---
apply premises------0.04---
apply premises------0.05---
apply premises0.06---------
apply premises0.36---------
apply premises------0.21---
apply premises---------0.06
apply premises------0.07---
apply premises---------0.02
apply premises------0.06---
apply premises0.07---------
apply premises------0.07---
apply premises------0.05---
apply premises0.56---------
apply premises------0.30---
apply premises0.10---------
apply premises------0.07---
apply premises------0.05---
apply premises---------0.02
apply premises------0.05---
apply premises------0.05---
apply premises------0.05---
apply premises0.43---------
apply premises------0.22---
apply premises------0.09---
apply premises---------0.01
apply premises------0.06---
apply premises---0.10------
apply premises------0.06---
apply premises------0.05---
apply premises------0.05---
apply premises0.27---------
apply premises0.38---------
apply premises---------0.01
asserted formula6.05---------
asserted formula------0.05---
postcondition------0.07---
VC for lse8------------
split_vc
precondition0.08---------
precondition------0.05---
precondition0.09---------
precondition------0.05---
precondition------0.05---
precondition0.07---------
precondition------0.09---
precondition0.09---------
precondition7.87---------
postcondition------------
assert let t = log (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) in abs (to_real r -. t) <=. ((abs t *. log_rel_err) +. (((-. log (1.0 -. ((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))) <=. ((abs (log (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))) *. log_rel_err) +. (((-. log (1.0 -. ((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))) <=. ((log_rel_err *. abs (log (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)))) +. (((-. log (1.0 -. (((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))) +. 0.0) /. (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with ((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) ++. exp_approx x8
apply premises------------
assert abs (to_real (((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) ++. exp_approx x8) -. (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))) <=. ((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7,exp_approx x8
apply premises------------
assert abs (to_real ((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) -. ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) <=. ((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6,exp_approx x7
apply premises------------
assert abs (to_real (((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) -. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) <=. ((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5,exp_approx x6
apply premises------------
assert abs (to_real ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) -. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) <=. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4,exp_approx x5
apply premises------------
assert abs (to_real (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) -. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) <=. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (exp_approx x1 ++. exp_approx x2) ++. exp_approx x3,exp_approx x4
apply premises------------
assert abs (to_real ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) -. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) <=. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((exp_rel_err +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1 ++. exp_approx x2,exp_approx x3
apply premises------------
assert abs (to_real (exp_approx x1 ++. exp_approx x2) -. (exp (to_real x1) +. exp (to_real x2))) <=. ((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x1) +. exp (to_real x2))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. exp_rel_err) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1,exp_approx x2
apply premises------0.07---
apply premises------0.05---
apply premises------0.24---
apply premises------0.23---
apply premises------0.06---
apply premises---0.09------
apply premises------0.07---
apply premises------0.07---
apply premises------0.05---
apply premises---------0.01
apply premises------0.05---
apply premises0.37---------
apply premises------0.25---
apply premises---------0.05
apply premises------0.06---
apply premises------0.06---
apply premises---------0.02
apply premises------0.06---
apply premises------0.05---
apply premises------0.04---
apply premises0.39---------
apply premises------0.23---
apply premises------0.09---
apply premises0.08---------
apply premises------0.06---
apply premises------0.07---
apply premises---------0.01
apply premises---------0.02
apply premises------0.07---
apply premises0.49---------
apply premises------0.26---
apply premises---------0.06
apply premises------0.09---
apply premises------0.08---
apply premises------0.06---
apply premises---------0.01
apply premises------0.05---
apply premises---------0.02
apply premises0.60---------
apply premises------0.30---
apply premises---------0.04
apply premises------0.08---
apply premises------0.06---
apply premises------0.08---
apply premises------0.07---
apply premises------0.08---
apply premises------0.05---
apply premises---------0.55
apply premises------0.35---
apply premises---------0.06
apply premises---------0.02
apply premises0.07---------
apply premises------0.07---
apply premises------0.08---
apply premises---------0.02
apply premises---0.10------
apply premises0.88---------
apply premises------0.34---
apply premises---------0.04
apply premises---------0.02
apply premises------0.07---
apply premises---------0.02
apply premises0.08---------
apply premises------0.07---
apply premises0.09---------
apply premises0.43---------
apply premises0.45---------
apply premises------0.05---
asserted formula5.14---------
asserted formula------0.06---
postcondition------0.07---
VC for lse10------------
split_vc
precondition------0.07---
precondition0.06---------
precondition------0.05---
precondition------0.05---
precondition------0.04---
precondition0.06---------
precondition---------0.02
precondition------0.04---
precondition------0.05---
precondition0.06---------
assertion14.33---------
precondition---0.09------
postcondition------------
assert let t = log (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10)) in abs (to_real r -. t) <=. ((abs t *. log_rel_err) +. (((-. log (1.0 -. ((((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10))) <=. ((abs (log (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10))) *. log_rel_err) +. (((-. log (1.0 -. ((((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
assert abs (to_real r -. log (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10))) <=. ((log_rel_err *. abs (log (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10)))) +. (((-. log (1.0 -. (((((((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10))) +. 0.0) /. (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10))))) *. (1.0 +. log_rel_err)) +. log_abs_err))
asserted formula------------
apply log_double_error_propagation with s
apply premises------------
assert abs (to_real s -. (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10))) <=. ((((((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9)) +. exp (to_real x10))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) ++. exp_approx x8) ++. exp_approx x9,exp_approx x10
apply premises------------
assert abs (to_real ((((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) ++. exp_approx x8) ++. exp_approx x9) -. ((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9))) <=. ((((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8)) +. exp (to_real x9))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) ++. exp_approx x8,exp_approx x9
apply premises------------
assert abs (to_real (((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) ++. exp_approx x8) -. (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))) <=. ((((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7)) +. exp (to_real x8))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7,exp_approx x8
apply premises------------
assert abs (to_real ((((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) ++. exp_approx x7) -. ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) <=. ((((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6)) +. exp (to_real x7))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6,exp_approx x7
apply premises------------
assert abs (to_real (((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) ++. exp_approx x6) -. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) <=. ((((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5)) +. exp (to_real x6))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5,exp_approx x6
apply premises------------
assert abs (to_real ((((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) ++. exp_approx x5) -. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) <=. ((((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4)) +. exp (to_real x5))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4,exp_approx x5
apply premises------------
assert abs (to_real (((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) ++. exp_approx x4) -. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) <=. ((((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. (((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3)) +. exp (to_real x4))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with (exp_approx x1 ++. exp_approx x2) ++. exp_approx x3,exp_approx x4
apply premises------------
assert abs (to_real ((exp_approx x1 ++. exp_approx x2) ++. exp_approx x3) -. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) <=. ((((((exp_rel_err +. exp_rel_err) +. eps) +. exp_rel_err) +. eps) *. ((exp (to_real x1) +. exp (to_real x2)) +. exp (to_real x3))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. ((exp_rel_err +. exp_rel_err) +. eps)) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1 ++. exp_approx x2,exp_approx x3
apply premises------------
assert abs (to_real (exp_approx x1 ++. exp_approx x2) -. (exp (to_real x1) +. exp (to_real x2))) <=. ((((exp_rel_err +. exp_rel_err) +. eps) *. (exp (to_real x1) +. exp (to_real x2))) +. ((((1.0 +. eps) +. exp_rel_err) *. 0.0) +. (((1.0 +. eps) +. exp_rel_err) *. 0.0)))
asserted formula------------
apply uadd_double_error_propagation with exp_approx x1,exp_approx x2
apply premises------0.07---
apply premises------0.07---
apply premises------0.29---
apply premises---0.45------
apply premises------0.08---
apply premises------0.09---
apply premises---------0.02
apply premises---------0.02
apply premises------0.09---
apply premises------0.07---
apply premises---------0.02
apply premises0.54---------
apply premises------0.28---
apply premises0.09---------
apply premises------0.08---
apply premises------0.09---
apply premises------0.08---
apply premises------0.08---
apply premises0.09---------
apply premises------0.08---
apply premises0.74---------
apply premises------0.41---
apply premises---------0.06
apply premises---------0.02
apply premises------0.08---
apply premises---------0.02
apply premises------0.06---
apply premises---------0.01
apply premises------0.06---
apply premises0.65---------
apply premises------0.28---
apply premises------0.08---
apply premises---------0.01
apply premises------0.07---
apply premises0.09---------
apply premises------0.06---
apply premises------0.06---
apply premises---------0.02
apply premises0.68---------
apply premises------0.33---
apply premises---------0.05
apply premises---------0.01
apply premises------0.06---
apply premises0.08---------
apply premises---------0.02
apply premises0.12---------
apply premises------0.08---
apply premises0.80---------
apply premises------0.28---
apply premises------0.07---
apply premises---------0.02
apply premises------0.06---
apply premises---------0.02
apply premises------0.07---
apply premises------0.07---
apply premises------0.05---
apply premises1.08---------
apply premises------0.38---
apply premises------0.12---
apply premises------0.06---
apply premises---------0.02
apply premises0.12---------
apply premises---------0.02
apply premises------0.06---
apply premises------0.05---
apply premises1.36---------
apply premises------0.28---
apply premises------0.09---
apply premises------0.06---
apply premises0.10---------
apply premises0.11---------
apply premises------0.09---
apply premises------0.09---
apply premises---------0.02
apply premises---------1.36
apply premises------0.42---
apply premises---------0.06
apply premises------0.07---
apply premises------0.06---
apply premises------0.09---
apply premises---------0.02
apply premises---------0.01
apply premises------0.10---
apply premises0.45---------
apply premises0.78---------
apply premises------0.09---
asserted formula6.72---------
asserted formula------0.08---
postcondition------0.07---
VC for example3------------
split_vc
precondition0.09---------
postcondition------------
assert let t = log2 (to_real x +. to_real y) in abs (to_real r -. t) <=. ((abs t *. log2_rel_error) +. (((-. log2 (1.0 -. eps)) *. (1.0 +. log2_rel_error)) +. log2_abs_error))
asserted formula------------
assert abs (to_real r -. log2 (to_real x +. to_real y)) <=. ((abs (log2 (to_real x +. to_real y)) *. log2_rel_error) +. (((-. log2 (1.0 -. eps)) *. (1.0 +. log2_rel_error)) +. log2_abs_error))
asserted formula------------
assert abs (to_real r -. log2 (to_real x +. to_real y)) <=. ((log2_rel_error *. abs (log2 (to_real x +. to_real y))) +. (((-. log2 (1.0 -. (((eps *. abs (to_real x +. to_real y)) +. 0.0) /. (to_real x +. to_real y)))) *. (1.0 +. log2_rel_error)) +. log2_abs_error))
asserted formula------------
apply log2_double_error_propagation with x ++. y
apply premises------------
assert abs (to_real (x ++. y) -. (to_real x +. to_real y)) <=. (eps *. abs (to_real x +. to_real y))
asserted formula0.28---------
apply premises------0.08---
apply premises------0.04---
apply premises0.07---------
apply premises0.06---------
apply premises------0.04---
asserted formula0.06---------
asserted formula------0.06---
postcondition---------0.01
VC for example4------------
split_vc
precondition0.14---------
postcondition------------
assert let t = log10 (to_real x +. to_real y) in abs (to_real r -. t) <=. ((abs t *. log10_error) +. ((-. log10 (1.0 -. eps)) *. (1.0 +. log10_error)))
asserted formula------------
assert abs (to_real r -. log10 (to_real x +. to_real y)) <=. ((abs (log10 (to_real x +. to_real y)) *. log10_error) +. ((-. log10 (1.0 -. eps)) *. (1.0 +. log10_error)))
asserted formula------------
assert abs (to_real r -. log10 (to_real x +. to_real y)) <=. ((log10_error *. abs (log10 (to_real x +. to_real y))) +. (((-. log10 (1.0 -. (((eps *. abs (to_real x +. to_real y)) +. 0.0) /. (to_real x +. to_real y)))) *. (1.0 +. log10_error)) +. 0.0))
asserted formula------------
apply log10_double_error_propagation with x ++. y
apply premises------------
assert abs (to_real (x ++. y) -. (to_real x +. to_real y)) <=. (eps *. abs (to_real x +. to_real y))
asserted formula0.18---------
apply premises0.07---------
apply premises0.07---------
apply premises------0.08---
apply premises------0.05---
apply premises0.07---------
asserted formula0.08---------
asserted formula------0.08---
postcondition0.06---------