?

Average Error: 0.0 → 0.0
Time: 1.0min
Precision: binary64
Cost: 7232

?

\[\left(\left(\left(\left(\left(\left(-1.79 \cdot 10^{+308} \leq xn \land xn \leq 1.79 \cdot 10^{+308}\right) \land \left(-1.79 \cdot 10^{+308} \leq uxnprev \land uxnprev \leq 1.79 \cdot 10^{+308}\right)\right) \land \left(-1.79 \cdot 10^{+308} \leq yn \land yn \leq 1.79 \cdot 10^{+308}\right)\right) \land \left(-1.79 \cdot 10^{+308} \leq uy \land uy \leq 1.79 \cdot 10^{+308}\right)\right) \land \left(-1.79 \cdot 10^{+308} \leq x0 \land x0 \leq 1.79 \cdot 10^{+308}\right)\right) \land \left(-1.79 \cdot 10^{+308} \leq y0 \land y0 \leq 1.79 \cdot 10^{+308}\right)\right) \land \left(-1.79 \cdot 10^{+308} \leq uyn \land uyn \leq 1.79 \cdot 10^{+308}\right)\]
\[\left(xn - uxnprev\right) \cdot \left(yn - uy\right) - \left(x0 - uxnprev\right) \cdot \left(y0 - uyn\right) \]
↓
\[\mathsf{fma}\left(y0 - uyn, uxnprev - x0, \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right) \]
(FPCore (xn uxnprev yn uy x0 y0 uyn)
 :precision binary64
 (- (* (- xn uxnprev) (- yn uy)) (* (- x0 uxnprev) (- y0 uyn))))
↓
(FPCore (xn uxnprev yn uy x0 y0 uyn)
 :precision binary64
 (fma (- y0 uyn) (- uxnprev x0) (* (- xn uxnprev) (- yn uy))))
double code(double xn, double uxnprev, double yn, double uy, double x0, double y0, double uyn) {
	return ((xn - uxnprev) * (yn - uy)) - ((x0 - uxnprev) * (y0 - uyn));
}
↓
double code(double xn, double uxnprev, double yn, double uy, double x0, double y0, double uyn) {
	return fma((y0 - uyn), (uxnprev - x0), ((xn - uxnprev) * (yn - uy)));
}

function code(xn, uxnprev, yn, uy, x0, y0, uyn)
	return Float64(Float64(Float64(xn - uxnprev) * Float64(yn - uy)) - Float64(Float64(x0 - uxnprev) * Float64(y0 - uyn)))
end
↓
function code(xn, uxnprev, yn, uy, x0, y0, uyn)
	return fma(Float64(y0 - uyn), Float64(uxnprev - x0), Float64(Float64(xn - uxnprev) * Float64(yn - uy)))
end

code[xn_, uxnprev_, yn_, uy_, x0_, y0_, uyn_] := N[(N[(N[(xn - uxnprev), $MachinePrecision] * N[(yn - uy), $MachinePrecision]), $MachinePrecision] - N[(N[(x0 - uxnprev), $MachinePrecision] * N[(y0 - uyn), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
↓
code[xn_, uxnprev_, yn_, uy_, x0_, y0_, uyn_] := N[(N[(y0 - uyn), $MachinePrecision] * N[(uxnprev - x0), $MachinePrecision] + N[(N[(xn - uxnprev), $MachinePrecision] * N[(yn - uy), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

\left(xn - uxnprev\right) \cdot \left(yn - uy\right) - \left(x0 - uxnprev\right) \cdot \left(y0 - uyn\right)
↓
\mathsf{fma}\left(y0 - uyn, uxnprev - x0, \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right)

Error?

Derivation?

  1. Initial program 0.0

    \[\left(xn - uxnprev\right) \cdot \left(yn - uy\right) - \left(x0 - uxnprev\right) \cdot \left(y0 - uyn\right) \]

  2. Simplified0.0

    \[\leadsto \color{blue}{\mathsf{fma}\left(y0 - uyn, uxnprev - x0, \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right)} \]
    Proof

    [Start]0.0

    \[ \left(xn - uxnprev\right) \cdot \left(yn - uy\right) - \left(x0 - uxnprev\right) \cdot \left(y0 - uyn\right) \]

    cancel-sign-sub-inv [=>]0.0

    \[ \color{blue}{\left(xn - uxnprev\right) \cdot \left(yn - uy\right) + \left(-\left(x0 - uxnprev\right)\right) \cdot \left(y0 - uyn\right)} \]

    +-commutative [=>]0.0

    \[ \color{blue}{\left(-\left(x0 - uxnprev\right)\right) \cdot \left(y0 - uyn\right) + \left(xn - uxnprev\right) \cdot \left(yn - uy\right)} \]

    *-commutative [=>]0.0

    \[ \color{blue}{\left(y0 - uyn\right) \cdot \left(-\left(x0 - uxnprev\right)\right)} + \left(xn - uxnprev\right) \cdot \left(yn - uy\right) \]

    fma-def [=>]0.0

    \[ \color{blue}{\mathsf{fma}\left(y0 - uyn, -\left(x0 - uxnprev\right), \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right)} \]

    sub-neg [=>]0.0

    \[ \mathsf{fma}\left(y0 - uyn, -\color{blue}{\left(x0 + \left(-uxnprev\right)\right)}, \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right) \]

    distribute-neg-in [=>]0.0

    \[ \mathsf{fma}\left(y0 - uyn, \color{blue}{\left(-x0\right) + \left(-\left(-uxnprev\right)\right)}, \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right) \]

    +-commutative [=>]0.0

    \[ \mathsf{fma}\left(y0 - uyn, \color{blue}{\left(-\left(-uxnprev\right)\right) + \left(-x0\right)}, \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right) \]

    remove-double-neg [=>]0.0

    \[ \mathsf{fma}\left(y0 - uyn, \color{blue}{uxnprev} + \left(-x0\right), \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right) \]

    sub-neg [<=]0.0

    \[ \mathsf{fma}\left(y0 - uyn, \color{blue}{uxnprev - x0}, \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right) \]

  3. Final simplification0.0

    \[\leadsto \mathsf{fma}\left(y0 - uyn, uxnprev - x0, \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\right) \]

Alternatives

Alternative 1
Error33.9
Cost1896
\[\begin{array}{l} t_0 := uxnprev \cdot \left(\left(y0 + \left(uy - yn\right)\right) - uyn\right)\\ t_1 := x0 \cdot \left(uyn - y0\right)\\ t_2 := xn \cdot \left(yn - uy\right)\\ \mathbf{if}\;x0 \leq -8 \cdot 10^{-15}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;x0 \leq -3.3 \cdot 10^{-192}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x0 \leq -1.25 \cdot 10^{-216}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;x0 \leq -3 \cdot 10^{-273}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x0 \leq -5.7 \cdot 10^{-301}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;x0 \leq 5.4 \cdot 10^{-229}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x0 \leq 4.5 \cdot 10^{-193}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;x0 \leq 4.2 \cdot 10^{-108}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x0 \leq 6.1 \cdot 10^{-21}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;x0 \leq 0.175:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x0 \leq 1.26 \cdot 10^{+85}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 2
Error12.5
Cost1626
\[\begin{array}{l} t_0 := \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\\ \mathbf{if}\;uy \leq -6.3 \cdot 10^{+145}:\\ \;\;\;\;t_0 - uyn \cdot uxnprev\\ \mathbf{elif}\;uy \leq -8.2 \cdot 10^{+102} \lor \neg \left(uy \leq -8 \cdot 10^{+18}\right) \land \left(uy \leq 6.2 \cdot 10^{-138} \lor \neg \left(uy \leq 5.1 \cdot 10^{+17}\right) \land uy \leq 7 \cdot 10^{+101}\right):\\ \;\;\;\;\left(xn - uxnprev\right) \cdot yn + \left(y0 - uyn\right) \cdot \left(uxnprev - x0\right)\\ \mathbf{else}:\\ \;\;\;\;t_0 + \left(y0 - uyn\right) \cdot uxnprev\\ \end{array} \]
Alternative 3
Error11.6
Cost1625
\[\begin{array}{l} t_0 := \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\\ t_1 := \left(xn - uxnprev\right) \cdot yn + \left(y0 - uyn\right) \cdot \left(uxnprev - x0\right)\\ \mathbf{if}\;y0 \leq -1.12 \cdot 10^{+173}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;y0 \leq -2.5 \cdot 10^{+19}:\\ \;\;\;\;t_0 + \left(y0 - uyn\right) \cdot uxnprev\\ \mathbf{elif}\;y0 \leq -4.3 \cdot 10^{-100}:\\ \;\;\;\;xn \cdot \left(yn - uy\right) + x0 \cdot \left(uyn - y0\right)\\ \mathbf{elif}\;y0 \leq 1.05 \cdot 10^{+38} \lor \neg \left(y0 \leq 4.2 \cdot 10^{+82}\right) \land y0 \leq 3.1 \cdot 10^{+122}:\\ \;\;\;\;t_0 + uyn \cdot \left(x0 - uxnprev\right)\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 4
Error40.2
Cost1508
\[\begin{array}{l} t_0 := x0 \cdot \left(uyn - y0\right)\\ t_1 := uy \cdot \left(uxnprev - xn\right)\\ \mathbf{if}\;uy \leq -2.95 \cdot 10^{+144}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;uy \leq -1.6 \cdot 10^{+103}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq -3.4 \cdot 10^{+29}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;uy \leq -8 \cdot 10^{-168}:\\ \;\;\;\;uyn \cdot \left(x0 - uxnprev\right)\\ \mathbf{elif}\;uy \leq -3 \cdot 10^{-253}:\\ \;\;\;\;\left(xn - uxnprev\right) \cdot yn\\ \mathbf{elif}\;uy \leq 6.8 \cdot 10^{-263}:\\ \;\;\;\;y0 \cdot \left(uxnprev - x0\right)\\ \mathbf{elif}\;uy \leq 3.1 \cdot 10^{-138}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq 7.6 \cdot 10^{+16}:\\ \;\;\;\;xn \cdot \left(yn - uy\right)\\ \mathbf{elif}\;uy \leq 2.05 \cdot 10^{+102}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 5
Error25.8
Cost1496
\[\begin{array}{l} t_0 := uxnprev \cdot \left(\left(y0 + \left(uy - yn\right)\right) - uyn\right)\\ t_1 := \left(xn - uxnprev\right) \cdot yn\\ t_2 := t_1 - xn \cdot uy\\ t_3 := t_1 + x0 \cdot \left(uyn - y0\right)\\ \mathbf{if}\;x0 \leq -2.5 \cdot 10^{-106}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;x0 \leq -1.1 \cdot 10^{-270}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x0 \leq 1.7 \cdot 10^{-299}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;x0 \leq 2.3 \cdot 10^{-232}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x0 \leq 5.4 \cdot 10^{-192}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;x0 \leq 1.6 \cdot 10^{-99}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;t_3\\ \end{array} \]
Alternative 6
Error17.3
Cost1496
\[\begin{array}{l} t_0 := x0 \cdot \left(uyn - y0\right)\\ t_1 := \left(xn - uxnprev\right) \cdot \left(yn - uy\right)\\ t_2 := t_1 + y0 \cdot uxnprev\\ t_3 := t_1 - uyn \cdot uxnprev\\ t_4 := xn \cdot \left(yn - uy\right) + t_0\\ \mathbf{if}\;x0 \leq -6.8 \cdot 10^{-15}:\\ \;\;\;\;t_4\\ \mathbf{elif}\;x0 \leq -1.4 \cdot 10^{-98}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;x0 \leq -2.22 \cdot 10^{-100}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;x0 \leq -3.8 \cdot 10^{-154}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;x0 \leq -1.1 \cdot 10^{-307}:\\ \;\;\;\;t_3\\ \mathbf{elif}\;x0 \leq 1.3 \cdot 10^{-70}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_4\\ \end{array} \]
Alternative 7
Error39.4
Cost1376
\[\begin{array}{l} t_0 := uy \cdot \left(uxnprev - xn\right)\\ t_1 := x0 \cdot \left(uyn - y0\right)\\ t_2 := \left(xn - uxnprev\right) \cdot yn\\ \mathbf{if}\;uy \leq -5.3 \cdot 10^{+144}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq -2.7 \cdot 10^{+104}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;uy \leq -1.6 \cdot 10^{+29}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq -1.1 \cdot 10^{-167}:\\ \;\;\;\;uyn \cdot \left(x0 - uxnprev\right)\\ \mathbf{elif}\;uy \leq -3 \cdot 10^{-253}:\\ \;\;\;\;t_2\\ \mathbf{elif}\;uy \leq 2.5 \cdot 10^{-263}:\\ \;\;\;\;y0 \cdot \left(uxnprev - x0\right)\\ \mathbf{elif}\;uy \leq 2.6 \cdot 10^{-164}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;uy \leq 3.5 \cdot 10^{-18}:\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 8
Error39.7
Cost1244
\[\begin{array}{l} t_0 := x0 \cdot \left(uyn - y0\right)\\ t_1 := uy \cdot \left(uxnprev - xn\right)\\ \mathbf{if}\;uy \leq -2.95 \cdot 10^{+144}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;uy \leq -1.1 \cdot 10^{+105}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq -1.1 \cdot 10^{+27}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;uy \leq -1.4 \cdot 10^{-182}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq 5.3 \cdot 10^{-263}:\\ \;\;\;\;y0 \cdot \left(uxnprev - x0\right)\\ \mathbf{elif}\;uy \leq 6.2 \cdot 10^{-138}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq 1.15 \cdot 10^{-18}:\\ \;\;\;\;xn \cdot yn\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 9
Error40.3
Cost1244
\[\begin{array}{l} t_0 := x0 \cdot \left(uyn - y0\right)\\ t_1 := uy \cdot \left(uxnprev - xn\right)\\ \mathbf{if}\;uy \leq -5.2 \cdot 10^{+149}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;uy \leq -1.9 \cdot 10^{+105}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq -1.95 \cdot 10^{+29}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;uy \leq -4.9 \cdot 10^{-200}:\\ \;\;\;\;uyn \cdot \left(x0 - uxnprev\right)\\ \mathbf{elif}\;uy \leq 2.6 \cdot 10^{-263}:\\ \;\;\;\;y0 \cdot \left(uxnprev - x0\right)\\ \mathbf{elif}\;uy \leq 5.4 \cdot 10^{-138}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq 2.7 \cdot 10^{-18}:\\ \;\;\;\;xn \cdot yn\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
Alternative 10
Error21.2
Cost1234
\[\begin{array}{l} \mathbf{if}\;uyn \leq -1.25 \cdot 10^{+189} \lor \neg \left(uyn \leq -3.65 \cdot 10^{+25} \lor \neg \left(uyn \leq -5.6 \cdot 10^{-21}\right) \land uyn \leq 8.8 \cdot 10^{+89}\right):\\ \;\;\;\;\left(xn - uxnprev\right) \cdot yn + uyn \cdot \left(x0 - uxnprev\right)\\ \mathbf{else}:\\ \;\;\;\;\left(xn - uxnprev\right) \cdot \left(yn - uy\right) + y0 \cdot uxnprev\\ \end{array} \]
Alternative 11
Error0.0
Cost1216
\[\left(xn - uxnprev\right) \cdot yn + \left(uy \cdot \left(uxnprev - xn\right) + \left(y0 - uyn\right) \cdot \left(uxnprev - x0\right)\right) \]
Alternative 12
Error12.1
Cost1097
\[\begin{array}{l} \mathbf{if}\;x0 \leq -1.22 \cdot 10^{-14} \lor \neg \left(x0 \leq 0.3\right):\\ \;\;\;\;xn \cdot \left(yn - uy\right) + x0 \cdot \left(uyn - y0\right)\\ \mathbf{else}:\\ \;\;\;\;\left(xn - uxnprev\right) \cdot \left(yn - uy\right) + \left(y0 - uyn\right) \cdot uxnprev\\ \end{array} \]
Alternative 13
Error29.1
Cost972
\[\begin{array}{l} t_0 := uxnprev \cdot \left(\left(y0 + \left(uy - yn\right)\right) - uyn\right)\\ \mathbf{if}\;uxnprev \leq -2.1 \cdot 10^{-79}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uxnprev \leq -1.4 \cdot 10^{-233}:\\ \;\;\;\;x0 \cdot \left(uyn - y0\right)\\ \mathbf{elif}\;uxnprev \leq 5.2 \cdot 10^{-82}:\\ \;\;\;\;\left(xn - uxnprev\right) \cdot yn - xn \cdot uy\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 14
Error15.9
Cost969
\[\begin{array}{l} \mathbf{if}\;uxnprev \leq -2.05 \cdot 10^{-57} \lor \neg \left(uxnprev \leq 3900000000\right):\\ \;\;\;\;uxnprev \cdot \left(\left(y0 + \left(uy - yn\right)\right) - uyn\right)\\ \mathbf{else}:\\ \;\;\;\;xn \cdot \left(yn - uy\right) + x0 \cdot \left(uyn - y0\right)\\ \end{array} \]
Alternative 15
Error0.0
Cost960
\[\left(xn - uxnprev\right) \cdot \left(yn - uy\right) + \left(y0 - uyn\right) \cdot \left(uxnprev - x0\right) \]
Alternative 16
Error41.0
Cost848
\[\begin{array}{l} t_0 := uy \cdot \left(uxnprev - xn\right)\\ \mathbf{if}\;uy \leq -1.05 \cdot 10^{-31}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq -3.9 \cdot 10^{-132}:\\ \;\;\;\;uxnprev \cdot \left(-uyn\right)\\ \mathbf{elif}\;uy \leq 9.8 \cdot 10^{-160}:\\ \;\;\;\;y0 \cdot \left(uxnprev - x0\right)\\ \mathbf{elif}\;uy \leq 8 \cdot 10^{-18}:\\ \;\;\;\;xn \cdot yn\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 17
Error51.7
Cost720
\[\begin{array}{l} \mathbf{if}\;y0 \leq -4.2 \cdot 10^{+98}:\\ \;\;\;\;y0 \cdot uxnprev\\ \mathbf{elif}\;y0 \leq -1.16 \cdot 10^{-290}:\\ \;\;\;\;xn \cdot yn\\ \mathbf{elif}\;y0 \leq 1.5 \cdot 10^{-220}:\\ \;\;\;\;uxnprev \cdot \left(-uyn\right)\\ \mathbf{elif}\;y0 \leq 1.95 \cdot 10^{+39}:\\ \;\;\;\;xn \cdot yn\\ \mathbf{else}:\\ \;\;\;\;y0 \cdot uxnprev\\ \end{array} \]
Alternative 18
Error43.2
Cost716
\[\begin{array}{l} t_0 := uy \cdot \left(uxnprev - xn\right)\\ \mathbf{if}\;uy \leq -6 \cdot 10^{-33}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;uy \leq -1.2 \cdot 10^{-170}:\\ \;\;\;\;uxnprev \cdot \left(-uyn\right)\\ \mathbf{elif}\;uy \leq 5.6 \cdot 10^{-19}:\\ \;\;\;\;xn \cdot yn\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 19
Error51.3
Cost456
\[\begin{array}{l} \mathbf{if}\;y0 \leq -9.8 \cdot 10^{+104}:\\ \;\;\;\;y0 \cdot uxnprev\\ \mathbf{elif}\;y0 \leq 2.6 \cdot 10^{+42}:\\ \;\;\;\;xn \cdot yn\\ \mathbf{else}:\\ \;\;\;\;y0 \cdot uxnprev\\ \end{array} \]
Alternative 20
Error53.2
Cost192
\[xn \cdot yn \]

Error

Reproduce?

herbie shell --seed 1 
(FPCore (xn uxnprev yn uy x0 y0 uyn)
  :name "(xn - uxnprev) * (yn - uy) - (x0 - uxnprev)*(y0 - uyn)"
  :precision binary64
  :pre (and (and (and (and (and (and (and (<= -1.79e+308 xn) (<= xn 1.79e+308)) (and (<= -1.79e+308 uxnprev) (<= uxnprev 1.79e+308))) (and (<= -1.79e+308 yn) (<= yn 1.79e+308))) (and (<= -1.79e+308 uy) (<= uy 1.79e+308))) (and (<= -1.79e+308 x0) (<= x0 1.79e+308))) (and (<= -1.79e+308 y0) (<= y0 1.79e+308))) (and (<= -1.79e+308 uyn) (<= uyn 1.79e+308)))
  (- (* (- xn uxnprev) (- yn uy)) (* (- x0 uxnprev) (- y0 uyn))))