(FPCore (x y z)
:precision binary64
(+
x
(/
(*
y
(+
(* (+ (* z 0.0692910599291889) 0.4917317610505968) z)
0.279195317918525))
(+ (* (+ z 6.012459259764103) z) 3.350343815022304))))
↓
(FPCore (x y z)
:precision binary64
(if (<= z -33000000000000.0)
(+ x (/ y (+ 14.431876219268936 (/ -15.646356830292042 z))))
(if (<= z 11000000.0)
(fma
(/
(fma z (fma z 0.0692910599291889 0.4917317610505968) 0.279195317918525)
(fma z (+ z 6.012459259764103) 3.350343815022304))
y
x)
(+ x (/ y 14.431876219268936)))))
(+.f64 x (/.f64 y (/.f64 (fma.f64 (+.f64 z 6012459259764103/1000000000000000) z 104698244219447/31250000000000) (fma.f64 (fma.f64 z 692910599291889/10000000000000000 307332350656623/625000000000000) z 11167812716741/40000000000000)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 y (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000)) (fma.f64 (fma.f64 z 692910599291889/10000000000000000 307332350656623/625000000000000) z 11167812716741/40000000000000)))): 0 points increase in error, 5 points decrease in error
(+.f64 x (/.f64 y (/.f64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000) (fma.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000)) z 11167812716741/40000000000000)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 y (/.f64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000) z) 11167812716741/40000000000000))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y (+.f64 (*.f64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000) z) 11167812716741/40000000000000)) (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000)))): 5 points increase in error, 0 points decrease in error
Taylor expanded in z around inf 0.0
\[\leadsto x + \frac{y}{\color{blue}{14.431876219268936 - 15.646356830292042 \cdot \frac{1}{z}}}
\]
Simplified0.0
\[\leadsto x + \frac{y}{\color{blue}{14.431876219268936 - \frac{15.646356830292042}{z}}}
\]
Proof
(+.f64 x (/.f64 y (-.f64 10000000000000000/692910599291889 (/.f64 2504069538682520235663395798110/160041699537014921582740396107 z)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 y (-.f64 10000000000000000/692910599291889 (/.f64 (Rewrite<= metadata-eval (*.f64 2504069538682520235663395798110/160041699537014921582740396107 1)) z)))): 3 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 y (-.f64 10000000000000000/692910599291889 (Rewrite<= associate-*r/_binary64 (*.f64 2504069538682520235663395798110/160041699537014921582740396107 (/.f64 1 z)))))): 0 points increase in error, 3 points decrease in error
if -3.3e13 < z < 1.1e7
Initial program 0.3
\[x + \frac{y \cdot \left(\left(z \cdot 0.0692910599291889 + 0.4917317610505968\right) \cdot z + 0.279195317918525\right)}{\left(z + 6.012459259764103\right) \cdot z + 3.350343815022304}
\]
Simplified0.1
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(z, \mathsf{fma}\left(z, 0.0692910599291889, 0.4917317610505968\right), 0.279195317918525\right)}{\mathsf{fma}\left(z, z + 6.012459259764103, 3.350343815022304\right)}, y, x\right)}
\]
Proof
(+.f64 x (/.f64 y (/.f64 (fma.f64 (+.f64 z 6012459259764103/1000000000000000) z 104698244219447/31250000000000) (fma.f64 (fma.f64 z 692910599291889/10000000000000000 307332350656623/625000000000000) z 11167812716741/40000000000000)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 y (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000)) (fma.f64 (fma.f64 z 692910599291889/10000000000000000 307332350656623/625000000000000) z 11167812716741/40000000000000)))): 0 points increase in error, 5 points decrease in error
(+.f64 x (/.f64 y (/.f64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000) (fma.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000)) z 11167812716741/40000000000000)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 y (/.f64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000) z) 11167812716741/40000000000000))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y (+.f64 (*.f64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000) z) 11167812716741/40000000000000)) (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000)))): 5 points increase in error, 0 points decrease in error
if 1.1e7 < z
Initial program 40.7
\[x + \frac{y \cdot \left(\left(z \cdot 0.0692910599291889 + 0.4917317610505968\right) \cdot z + 0.279195317918525\right)}{\left(z + 6.012459259764103\right) \cdot z + 3.350343815022304}
\]
(+.f64 x (/.f64 y (/.f64 (fma.f64 (+.f64 z 6012459259764103/1000000000000000) z 104698244219447/31250000000000) (fma.f64 (fma.f64 z 692910599291889/10000000000000000 307332350656623/625000000000000) z 11167812716741/40000000000000)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 y (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000)) (fma.f64 (fma.f64 z 692910599291889/10000000000000000 307332350656623/625000000000000) z 11167812716741/40000000000000)))): 0 points increase in error, 5 points decrease in error
(+.f64 x (/.f64 y (/.f64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000) (fma.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000)) z 11167812716741/40000000000000)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 y (/.f64 (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000) z) 11167812716741/40000000000000))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y (+.f64 (*.f64 (+.f64 (*.f64 z 692910599291889/10000000000000000) 307332350656623/625000000000000) z) 11167812716741/40000000000000)) (+.f64 (*.f64 (+.f64 z 6012459259764103/1000000000000000) z) 104698244219447/31250000000000)))): 5 points increase in error, 0 points decrease in error
Taylor expanded in z around inf 0.2
\[\leadsto x + \frac{y}{\color{blue}{14.431876219268936}}
\]