
(FPCore (m v) :precision binary64 (* (- (/ (* m (- 1.0 m)) v) 1.0) (- 1.0 m)))
double code(double m, double v) {
return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
code = (((m * (1.0d0 - m)) / v) - 1.0d0) * (1.0d0 - m)
end function
public static double code(double m, double v) {
return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
}
def code(m, v): return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m)
function code(m, v) return Float64(Float64(Float64(Float64(m * Float64(1.0 - m)) / v) - 1.0) * Float64(1.0 - m)) end
function tmp = code(m, v) tmp = (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m); end
code[m_, v_] := N[(N[(N[(N[(m * N[(1.0 - m), $MachinePrecision]), $MachinePrecision] / v), $MachinePrecision] - 1.0), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right)
\end{array}
Sampling outcomes in binary64 precision:
Herbie found 10 alternatives:
| Alternative | Accuracy | Speedup |
|---|
(FPCore (m v) :precision binary64 (* (- (/ (* m (- 1.0 m)) v) 1.0) (- 1.0 m)))
double code(double m, double v) {
return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
code = (((m * (1.0d0 - m)) / v) - 1.0d0) * (1.0d0 - m)
end function
public static double code(double m, double v) {
return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m);
}
def code(m, v): return (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m)
function code(m, v) return Float64(Float64(Float64(Float64(m * Float64(1.0 - m)) / v) - 1.0) * Float64(1.0 - m)) end
function tmp = code(m, v) tmp = (((m * (1.0 - m)) / v) - 1.0) * (1.0 - m); end
code[m_, v_] := N[(N[(N[(N[(m * N[(1.0 - m), $MachinePrecision]), $MachinePrecision] / v), $MachinePrecision] - 1.0), $MachinePrecision] * N[(1.0 - m), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right)
\end{array}
(FPCore (m v) :precision binary64 (* (- 1.0 m) (+ (/ (* m (- 1.0 m)) v) -1.0)))
double code(double m, double v) {
return (1.0 - m) * (((m * (1.0 - m)) / v) + -1.0);
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
code = (1.0d0 - m) * (((m * (1.0d0 - m)) / v) + (-1.0d0))
end function
public static double code(double m, double v) {
return (1.0 - m) * (((m * (1.0 - m)) / v) + -1.0);
}
def code(m, v): return (1.0 - m) * (((m * (1.0 - m)) / v) + -1.0)
function code(m, v) return Float64(Float64(1.0 - m) * Float64(Float64(Float64(m * Float64(1.0 - m)) / v) + -1.0)) end
function tmp = code(m, v) tmp = (1.0 - m) * (((m * (1.0 - m)) / v) + -1.0); end
code[m_, v_] := N[(N[(1.0 - m), $MachinePrecision] * N[(N[(N[(m * N[(1.0 - m), $MachinePrecision]), $MachinePrecision] / v), $MachinePrecision] + -1.0), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
\left(1 - m\right) \cdot \left(\frac{m \cdot \left(1 - m\right)}{v} + -1\right)
\end{array}
Initial program 100.0%
Final simplification100.0%
(FPCore (m v) :precision binary64 (if (<= m 1.0) (+ (/ m (/ v (- 1.0 m))) (+ m -1.0)) (* (- 1.0 m) (- -1.0 (* m (/ m v))))))
double code(double m, double v) {
double tmp;
if (m <= 1.0) {
tmp = (m / (v / (1.0 - m))) + (m + -1.0);
} else {
tmp = (1.0 - m) * (-1.0 - (m * (m / v)));
}
return tmp;
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
real(8) :: tmp
if (m <= 1.0d0) then
tmp = (m / (v / (1.0d0 - m))) + (m + (-1.0d0))
else
tmp = (1.0d0 - m) * ((-1.0d0) - (m * (m / v)))
end if
code = tmp
end function
public static double code(double m, double v) {
double tmp;
if (m <= 1.0) {
tmp = (m / (v / (1.0 - m))) + (m + -1.0);
} else {
tmp = (1.0 - m) * (-1.0 - (m * (m / v)));
}
return tmp;
}
def code(m, v): tmp = 0 if m <= 1.0: tmp = (m / (v / (1.0 - m))) + (m + -1.0) else: tmp = (1.0 - m) * (-1.0 - (m * (m / v))) return tmp
function code(m, v) tmp = 0.0 if (m <= 1.0) tmp = Float64(Float64(m / Float64(v / Float64(1.0 - m))) + Float64(m + -1.0)); else tmp = Float64(Float64(1.0 - m) * Float64(-1.0 - Float64(m * Float64(m / v)))); end return tmp end
function tmp_2 = code(m, v) tmp = 0.0; if (m <= 1.0) tmp = (m / (v / (1.0 - m))) + (m + -1.0); else tmp = (1.0 - m) * (-1.0 - (m * (m / v))); end tmp_2 = tmp; end
code[m_, v_] := If[LessEqual[m, 1.0], N[(N[(m / N[(v / N[(1.0 - m), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(m + -1.0), $MachinePrecision]), $MachinePrecision], N[(N[(1.0 - m), $MachinePrecision] * N[(-1.0 - N[(m * N[(m / v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;m \leq 1:\\
\;\;\;\;\frac{m}{\frac{v}{1 - m}} + \left(m + -1\right)\\
\mathbf{else}:\\
\;\;\;\;\left(1 - m\right) \cdot \left(-1 - m \cdot \frac{m}{v}\right)\\
\end{array}
\end{array}
if m < 1Initial program 99.9%
Taylor expanded in m around 0 96.3%
*-commutative96.3%
sub-neg96.3%
metadata-eval96.3%
distribute-lft-in96.3%
*-commutative96.3%
neg-mul-196.3%
Applied egg-rr96.3%
Taylor expanded in v around 0 96.3%
sub-neg96.3%
+-commutative96.3%
metadata-eval96.3%
associate-+l+96.3%
associate-/l*96.3%
+-commutative96.3%
Simplified96.3%
if 1 < m Initial program 100.0%
*-commutative100.0%
sub-neg100.0%
associate-/l*100.0%
metadata-eval100.0%
Simplified100.0%
Taylor expanded in m around inf 98.5%
associate-*r/98.5%
neg-mul-198.5%
Simplified98.5%
frac-2neg98.5%
remove-double-neg98.5%
associate-/r/98.5%
Applied egg-rr98.5%
Final simplification97.3%
(FPCore (m v) :precision binary64 (* (- 1.0 m) (+ (* (- 1.0 m) (/ m v)) -1.0)))
double code(double m, double v) {
return (1.0 - m) * (((1.0 - m) * (m / v)) + -1.0);
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
code = (1.0d0 - m) * (((1.0d0 - m) * (m / v)) + (-1.0d0))
end function
public static double code(double m, double v) {
return (1.0 - m) * (((1.0 - m) * (m / v)) + -1.0);
}
def code(m, v): return (1.0 - m) * (((1.0 - m) * (m / v)) + -1.0)
function code(m, v) return Float64(Float64(1.0 - m) * Float64(Float64(Float64(1.0 - m) * Float64(m / v)) + -1.0)) end
function tmp = code(m, v) tmp = (1.0 - m) * (((1.0 - m) * (m / v)) + -1.0); end
code[m_, v_] := N[(N[(1.0 - m), $MachinePrecision] * N[(N[(N[(1.0 - m), $MachinePrecision] * N[(m / v), $MachinePrecision]), $MachinePrecision] + -1.0), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
\left(1 - m\right) \cdot \left(\left(1 - m\right) \cdot \frac{m}{v} + -1\right)
\end{array}
Initial program 100.0%
*-commutative100.0%
sub-neg100.0%
associate-*l/100.0%
metadata-eval100.0%
Simplified100.0%
Final simplification100.0%
(FPCore (m v) :precision binary64 (if (<= v 4.6e-152) (* (- 1.0 m) (/ m v)) (+ m -1.0)))
double code(double m, double v) {
double tmp;
if (v <= 4.6e-152) {
tmp = (1.0 - m) * (m / v);
} else {
tmp = m + -1.0;
}
return tmp;
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
real(8) :: tmp
if (v <= 4.6d-152) then
tmp = (1.0d0 - m) * (m / v)
else
tmp = m + (-1.0d0)
end if
code = tmp
end function
public static double code(double m, double v) {
double tmp;
if (v <= 4.6e-152) {
tmp = (1.0 - m) * (m / v);
} else {
tmp = m + -1.0;
}
return tmp;
}
def code(m, v): tmp = 0 if v <= 4.6e-152: tmp = (1.0 - m) * (m / v) else: tmp = m + -1.0 return tmp
function code(m, v) tmp = 0.0 if (v <= 4.6e-152) tmp = Float64(Float64(1.0 - m) * Float64(m / v)); else tmp = Float64(m + -1.0); end return tmp end
function tmp_2 = code(m, v) tmp = 0.0; if (v <= 4.6e-152) tmp = (1.0 - m) * (m / v); else tmp = m + -1.0; end tmp_2 = tmp; end
code[m_, v_] := If[LessEqual[v, 4.6e-152], N[(N[(1.0 - m), $MachinePrecision] * N[(m / v), $MachinePrecision]), $MachinePrecision], N[(m + -1.0), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;v \leq 4.6 \cdot 10^{-152}:\\
\;\;\;\;\left(1 - m\right) \cdot \frac{m}{v}\\
\mathbf{else}:\\
\;\;\;\;m + -1\\
\end{array}
\end{array}
if v < 4.6000000000000003e-152Initial program 100.0%
Taylor expanded in m around 0 55.2%
*-commutative55.2%
sub-neg55.2%
metadata-eval55.2%
distribute-lft-in55.2%
*-commutative55.2%
neg-mul-155.2%
Applied egg-rr55.2%
Taylor expanded in v around 0 55.2%
sub-neg55.2%
+-commutative55.2%
metadata-eval55.2%
associate-+l+55.2%
associate-/l*55.2%
+-commutative55.2%
Simplified55.2%
Taylor expanded in v around 0 45.0%
associate-*l/45.0%
*-commutative45.0%
Simplified45.0%
if 4.6000000000000003e-152 < v Initial program 99.9%
*-commutative99.9%
sub-neg99.9%
associate-*l/99.9%
metadata-eval99.9%
Simplified99.9%
Taylor expanded in v around inf 43.0%
neg-mul-143.0%
neg-sub043.0%
associate--r-43.0%
metadata-eval43.0%
Simplified43.0%
Final simplification44.0%
(FPCore (m v) :precision binary64 (if (<= m 2.9e-223) -1.0 (* (/ m v) (+ m 1.0))))
double code(double m, double v) {
double tmp;
if (m <= 2.9e-223) {
tmp = -1.0;
} else {
tmp = (m / v) * (m + 1.0);
}
return tmp;
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
real(8) :: tmp
if (m <= 2.9d-223) then
tmp = -1.0d0
else
tmp = (m / v) * (m + 1.0d0)
end if
code = tmp
end function
public static double code(double m, double v) {
double tmp;
if (m <= 2.9e-223) {
tmp = -1.0;
} else {
tmp = (m / v) * (m + 1.0);
}
return tmp;
}
def code(m, v): tmp = 0 if m <= 2.9e-223: tmp = -1.0 else: tmp = (m / v) * (m + 1.0) return tmp
function code(m, v) tmp = 0.0 if (m <= 2.9e-223) tmp = -1.0; else tmp = Float64(Float64(m / v) * Float64(m + 1.0)); end return tmp end
function tmp_2 = code(m, v) tmp = 0.0; if (m <= 2.9e-223) tmp = -1.0; else tmp = (m / v) * (m + 1.0); end tmp_2 = tmp; end
code[m_, v_] := If[LessEqual[m, 2.9e-223], -1.0, N[(N[(m / v), $MachinePrecision] * N[(m + 1.0), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;m \leq 2.9 \cdot 10^{-223}:\\
\;\;\;\;-1\\
\mathbf{else}:\\
\;\;\;\;\frac{m}{v} \cdot \left(m + 1\right)\\
\end{array}
\end{array}
if m < 2.9e-223Initial program 100.0%
*-commutative100.0%
sub-neg100.0%
associate-*l/100.0%
metadata-eval100.0%
Simplified100.0%
Taylor expanded in m around 0 83.0%
if 2.9e-223 < m Initial program 99.9%
Taylor expanded in m around 0 44.4%
*-commutative44.4%
sub-neg44.4%
metadata-eval44.4%
distribute-lft-in44.4%
*-commutative44.4%
neg-mul-144.4%
Applied egg-rr44.4%
unsub-neg44.4%
*-commutative44.4%
*-un-lft-identity44.4%
distribute-rgt-out--44.4%
sub-neg44.4%
+-commutative44.4%
add-sqr-sqrt0.0%
sqrt-unprod87.0%
sqr-neg87.0%
sqrt-unprod87.0%
add-sqr-sqrt87.0%
Applied egg-rr87.0%
Taylor expanded in v around 0 72.1%
+-commutative72.1%
associate-*l/72.1%
Simplified72.1%
Final simplification73.8%
(FPCore (m v) :precision binary64 (if (<= m 2.4) (+ -1.0 (* m (/ 1.0 v))) (* (/ m v) (+ m 1.0))))
double code(double m, double v) {
double tmp;
if (m <= 2.4) {
tmp = -1.0 + (m * (1.0 / v));
} else {
tmp = (m / v) * (m + 1.0);
}
return tmp;
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
real(8) :: tmp
if (m <= 2.4d0) then
tmp = (-1.0d0) + (m * (1.0d0 / v))
else
tmp = (m / v) * (m + 1.0d0)
end if
code = tmp
end function
public static double code(double m, double v) {
double tmp;
if (m <= 2.4) {
tmp = -1.0 + (m * (1.0 / v));
} else {
tmp = (m / v) * (m + 1.0);
}
return tmp;
}
def code(m, v): tmp = 0 if m <= 2.4: tmp = -1.0 + (m * (1.0 / v)) else: tmp = (m / v) * (m + 1.0) return tmp
function code(m, v) tmp = 0.0 if (m <= 2.4) tmp = Float64(-1.0 + Float64(m * Float64(1.0 / v))); else tmp = Float64(Float64(m / v) * Float64(m + 1.0)); end return tmp end
function tmp_2 = code(m, v) tmp = 0.0; if (m <= 2.4) tmp = -1.0 + (m * (1.0 / v)); else tmp = (m / v) * (m + 1.0); end tmp_2 = tmp; end
code[m_, v_] := If[LessEqual[m, 2.4], N[(-1.0 + N[(m * N[(1.0 / v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(m / v), $MachinePrecision] * N[(m + 1.0), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;m \leq 2.4:\\
\;\;\;\;-1 + m \cdot \frac{1}{v}\\
\mathbf{else}:\\
\;\;\;\;\frac{m}{v} \cdot \left(m + 1\right)\\
\end{array}
\end{array}
if m < 2.39999999999999991Initial program 99.9%
*-commutative99.9%
sub-neg99.9%
associate-*l/99.9%
metadata-eval99.9%
Simplified99.9%
Taylor expanded in m around 0 95.9%
Taylor expanded in v around 0 95.9%
if 2.39999999999999991 < m Initial program 100.0%
Taylor expanded in m around 0 0.0%
*-commutative0.0%
sub-neg0.0%
metadata-eval0.0%
distribute-lft-in0.0%
*-commutative0.0%
neg-mul-10.0%
Applied egg-rr0.0%
unsub-neg0.0%
*-commutative0.0%
*-un-lft-identity0.0%
distribute-rgt-out--0.0%
sub-neg0.0%
+-commutative0.0%
add-sqr-sqrt0.0%
sqrt-unprod80.3%
sqr-neg80.3%
sqrt-unprod80.3%
add-sqr-sqrt80.3%
Applied egg-rr80.3%
Taylor expanded in v around 0 80.3%
+-commutative80.3%
associate-*l/80.3%
Simplified80.3%
Final simplification88.9%
(FPCore (m v) :precision binary64 (if (<= m 2.4) (+ -1.0 (+ m (/ m v))) (* (/ m v) (+ m 1.0))))
double code(double m, double v) {
double tmp;
if (m <= 2.4) {
tmp = -1.0 + (m + (m / v));
} else {
tmp = (m / v) * (m + 1.0);
}
return tmp;
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
real(8) :: tmp
if (m <= 2.4d0) then
tmp = (-1.0d0) + (m + (m / v))
else
tmp = (m / v) * (m + 1.0d0)
end if
code = tmp
end function
public static double code(double m, double v) {
double tmp;
if (m <= 2.4) {
tmp = -1.0 + (m + (m / v));
} else {
tmp = (m / v) * (m + 1.0);
}
return tmp;
}
def code(m, v): tmp = 0 if m <= 2.4: tmp = -1.0 + (m + (m / v)) else: tmp = (m / v) * (m + 1.0) return tmp
function code(m, v) tmp = 0.0 if (m <= 2.4) tmp = Float64(-1.0 + Float64(m + Float64(m / v))); else tmp = Float64(Float64(m / v) * Float64(m + 1.0)); end return tmp end
function tmp_2 = code(m, v) tmp = 0.0; if (m <= 2.4) tmp = -1.0 + (m + (m / v)); else tmp = (m / v) * (m + 1.0); end tmp_2 = tmp; end
code[m_, v_] := If[LessEqual[m, 2.4], N[(-1.0 + N[(m + N[(m / v), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(m / v), $MachinePrecision] * N[(m + 1.0), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
\\
\begin{array}{l}
\mathbf{if}\;m \leq 2.4:\\
\;\;\;\;-1 + \left(m + \frac{m}{v}\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{m}{v} \cdot \left(m + 1\right)\\
\end{array}
\end{array}
if m < 2.39999999999999991Initial program 99.9%
*-commutative99.9%
sub-neg99.9%
associate-*l/99.9%
metadata-eval99.9%
Simplified99.9%
Taylor expanded in m around 0 95.9%
+-commutative95.9%
distribute-lft-in95.9%
div-inv96.2%
*-rgt-identity96.2%
Applied egg-rr96.2%
if 2.39999999999999991 < m Initial program 100.0%
Taylor expanded in m around 0 0.0%
*-commutative0.0%
sub-neg0.0%
metadata-eval0.0%
distribute-lft-in0.0%
*-commutative0.0%
neg-mul-10.0%
Applied egg-rr0.0%
unsub-neg0.0%
*-commutative0.0%
*-un-lft-identity0.0%
distribute-rgt-out--0.0%
sub-neg0.0%
+-commutative0.0%
add-sqr-sqrt0.0%
sqrt-unprod80.3%
sqr-neg80.3%
sqrt-unprod80.3%
add-sqr-sqrt80.3%
Applied egg-rr80.3%
Taylor expanded in v around 0 80.3%
+-commutative80.3%
associate-*l/80.3%
Simplified80.3%
Final simplification89.0%
(FPCore (m v) :precision binary64 (* (+ m 1.0) (+ (/ m v) -1.0)))
double code(double m, double v) {
return (m + 1.0) * ((m / v) + -1.0);
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
code = (m + 1.0d0) * ((m / v) + (-1.0d0))
end function
public static double code(double m, double v) {
return (m + 1.0) * ((m / v) + -1.0);
}
def code(m, v): return (m + 1.0) * ((m / v) + -1.0)
function code(m, v) return Float64(Float64(m + 1.0) * Float64(Float64(m / v) + -1.0)) end
function tmp = code(m, v) tmp = (m + 1.0) * ((m / v) + -1.0); end
code[m_, v_] := N[(N[(m + 1.0), $MachinePrecision] * N[(N[(m / v), $MachinePrecision] + -1.0), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}
\\
\left(m + 1\right) \cdot \left(\frac{m}{v} + -1\right)
\end{array}
Initial program 100.0%
Taylor expanded in m around 0 53.0%
*-commutative53.0%
sub-neg53.0%
metadata-eval53.0%
distribute-lft-in53.0%
*-commutative53.0%
neg-mul-153.0%
Applied egg-rr53.0%
unsub-neg53.0%
*-commutative53.0%
*-un-lft-identity53.0%
distribute-rgt-out--53.0%
sub-neg53.0%
+-commutative53.0%
add-sqr-sqrt0.0%
sqrt-unprod89.0%
sqr-neg89.0%
sqrt-unprod89.0%
add-sqr-sqrt89.0%
Applied egg-rr89.0%
Final simplification89.0%
(FPCore (m v) :precision binary64 (+ m -1.0))
double code(double m, double v) {
return m + -1.0;
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
code = m + (-1.0d0)
end function
public static double code(double m, double v) {
return m + -1.0;
}
def code(m, v): return m + -1.0
function code(m, v) return Float64(m + -1.0) end
function tmp = code(m, v) tmp = m + -1.0; end
code[m_, v_] := N[(m + -1.0), $MachinePrecision]
\begin{array}{l}
\\
m + -1
\end{array}
Initial program 100.0%
*-commutative100.0%
sub-neg100.0%
associate-*l/100.0%
metadata-eval100.0%
Simplified100.0%
Taylor expanded in v around inf 26.1%
neg-mul-126.1%
neg-sub026.1%
associate--r-26.1%
metadata-eval26.1%
Simplified26.1%
Final simplification26.1%
(FPCore (m v) :precision binary64 -1.0)
double code(double m, double v) {
return -1.0;
}
real(8) function code(m, v)
real(8), intent (in) :: m
real(8), intent (in) :: v
code = -1.0d0
end function
public static double code(double m, double v) {
return -1.0;
}
def code(m, v): return -1.0
function code(m, v) return -1.0 end
function tmp = code(m, v) tmp = -1.0; end
code[m_, v_] := -1.0
\begin{array}{l}
\\
-1
\end{array}
Initial program 100.0%
*-commutative100.0%
sub-neg100.0%
associate-*l/100.0%
metadata-eval100.0%
Simplified100.0%
Taylor expanded in m around 0 23.9%
Final simplification23.9%
herbie shell --seed 2023320
(FPCore (m v)
:name "b parameter of renormalized beta distribution"
:precision binary64
:pre (and (and (< 0.0 m) (< 0.0 v)) (< v 0.25))
(* (- (/ (* m (- 1.0 m)) v) 1.0) (- 1.0 m)))