1. Initial program 79.1%

   \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]
2. Step-by-step derivation

   1. sub-neg79.1%

      \[\leadsto \color{blue}{x + \left(-\frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\right)} \]

   2. associate-/l*87.6%

      \[\leadsto x + \left(-\color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\right) \]

   3. *-commutative87.6%

      \[\leadsto x + \left(-\frac{\color{blue}{2 \cdot y}}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}\right) \]

   4. associate-/l*87.6%

      \[\leadsto x + \left(-\color{blue}{\frac{2}{\frac{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}{y}}}\right) \]

   5. distribute-neg-frac87.6%

      \[\leadsto x + \color{blue}{\frac{-2}{\frac{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}{y}}} \]

   6. metadata-eval87.6%

      \[\leadsto x + \frac{\color{blue}{-2}}{\frac{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}{y}} \]

   7. associate-/l/79.0%

      \[\leadsto x + \frac{-2}{\color{blue}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{y \cdot z}}} \]

   8. div-sub71.5%

      \[\leadsto x + \frac{-2}{\color{blue}{\frac{\left(z \cdot 2\right) \cdot z}{y \cdot z} - \frac{y \cdot t}{y \cdot z}}} \]

   9. times-frac87.4%

      \[\leadsto x + \frac{-2}{\color{blue}{\frac{z \cdot 2}{y} \cdot \frac{z}{z}} - \frac{y \cdot t}{y \cdot z}} \]

   10. *-inverses87.4%

       \[\leadsto x + \frac{-2}{\frac{z \cdot 2}{y} \cdot \color{blue}{1} - \frac{y \cdot t}{y \cdot z}} \]

   11. *-rgt-identity87.4%

       \[\leadsto x + \frac{-2}{\color{blue}{\frac{z \cdot 2}{y}} - \frac{y \cdot t}{y \cdot z}} \]

   12. *-commutative87.4%

       \[\leadsto x + \frac{-2}{\frac{\color{blue}{2 \cdot z}}{y} - \frac{y \cdot t}{y \cdot z}} \]

   13. associate-*l/87.4%

       \[\leadsto x + \frac{-2}{\color{blue}{\frac{2}{y} \cdot z} - \frac{y \cdot t}{y \cdot z}} \]

   14. *-commutative87.4%

       \[\leadsto x + \frac{-2}{\color{blue}{z \cdot \frac{2}{y}} - \frac{y \cdot t}{y \cdot z}} \]

   15. times-frac99.9%

       \[\leadsto x + \frac{-2}{z \cdot \frac{2}{y} - \color{blue}{\frac{y}{y} \cdot \frac{t}{z}}} \]

   16. *-inverses99.9%

       \[\leadsto x + \frac{-2}{z \cdot \frac{2}{y} - \color{blue}{1} \cdot \frac{t}{z}} \]

   17. *-lft-identity99.9%

       \[\leadsto x + \frac{-2}{z \cdot \frac{2}{y} - \color{blue}{\frac{t}{z}}} \]

3. Simplified99.9%

   \[\leadsto \color{blue}{x + \frac{-2}{z \cdot \frac{2}{y} - \frac{t}{z}}} \]

4. Final simplification99.9%

   \[\leadsto x + \frac{-2}{z \cdot \frac{2}{y} - \frac{t}{z}} \]

1. Split input into 2 regimes

2. if z < -8.4e-7 or 0.044999999999999998 < z

   1. Initial program 72.8%

      \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]
   2. Step-by-step derivation

      1. sub-neg72.8%

         \[\leadsto \color{blue}{x + \left(-\frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\right)} \]

      2. associate-/l*87.1%

         \[\leadsto x + \left(-\color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\right) \]

      3. distribute-neg-frac87.1%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}} \]

      4. associate-/r/87.1%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z} \]

      5. distribute-rgt-neg-in87.1%

         \[\leadsto x + \frac{\color{blue}{y \cdot \left(-2\right)}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      6. metadata-eval87.1%

         \[\leadsto x + \frac{y \cdot \color{blue}{-2}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      7. associate-*l*87.1%

         \[\leadsto x + \frac{y \cdot -2}{\color{blue}{z \cdot \left(2 \cdot z\right)} - y \cdot t} \cdot z \]

   3. Simplified87.1%

      \[\leadsto \color{blue}{x + \frac{y \cdot -2}{z \cdot \left(2 \cdot z\right) - y \cdot t} \cdot z} \]

   4. Taylor expanded in y around 0 92.8%

      \[\leadsto \color{blue}{-1 \cdot \frac{y}{z} + x} \]
   5. Step-by-step derivation

      1. +-commutative92.8%

         \[\leadsto \color{blue}{x + -1 \cdot \frac{y}{z}} \]

      2. mul-1-neg92.8%

         \[\leadsto x + \color{blue}{\left(-\frac{y}{z}\right)} \]

      3. sub-neg92.8%

         \[\leadsto \color{blue}{x - \frac{y}{z}} \]

   6. Simplified92.8%

      \[\leadsto \color{blue}{x - \frac{y}{z}} \]

   if -8.4e-7 < z < 0.044999999999999998

   1. Initial program 85.9%

      \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]
   2. Step-by-step derivation

      1. sub-neg85.9%

         \[\leadsto \color{blue}{x + \left(-\frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\right)} \]

      2. associate-/l*88.2%

         \[\leadsto x + \left(-\color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\right) \]

      3. distribute-neg-frac88.2%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}} \]

      4. associate-/r/88.9%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z} \]

      5. distribute-rgt-neg-in88.9%

         \[\leadsto x + \frac{\color{blue}{y \cdot \left(-2\right)}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      6. metadata-eval88.9%

         \[\leadsto x + \frac{y \cdot \color{blue}{-2}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      7. associate-*l*88.9%

         \[\leadsto x + \frac{y \cdot -2}{\color{blue}{z \cdot \left(2 \cdot z\right)} - y \cdot t} \cdot z \]

   3. Simplified88.9%

      \[\leadsto \color{blue}{x + \frac{y \cdot -2}{z \cdot \left(2 \cdot z\right) - y \cdot t} \cdot z} \]

   4. Taylor expanded in y around inf 92.0%

      \[\leadsto x + \color{blue}{\frac{2}{t}} \cdot z \]
3. Recombined 2 regimes into one program.

4. Final simplification92.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -8.4 \cdot 10^{-7} \lor \neg \left(z \leq 0.045\right):\\ \;\;\;\;x - \frac{y}{z}\\ \mathbf{else}:\\ \;\;\;\;x + z \cdot \frac{2}{t}\\ \end{array} \]

1. Split input into 2 regimes

2. if z < -1.1399999999999999e-10 or 2.09999999999999989e-13 < z

   1. Initial program 72.8%

      \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]
   2. Step-by-step derivation

      1. sub-neg72.8%

         \[\leadsto \color{blue}{x + \left(-\frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\right)} \]

      2. associate-/l*87.1%

         \[\leadsto x + \left(-\color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\right) \]

      3. distribute-neg-frac87.1%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}} \]

      4. associate-/r/87.1%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z} \]

      5. distribute-rgt-neg-in87.1%

         \[\leadsto x + \frac{\color{blue}{y \cdot \left(-2\right)}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      6. metadata-eval87.1%

         \[\leadsto x + \frac{y \cdot \color{blue}{-2}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      7. associate-*l*87.1%

         \[\leadsto x + \frac{y \cdot -2}{\color{blue}{z \cdot \left(2 \cdot z\right)} - y \cdot t} \cdot z \]

   3. Simplified87.1%

      \[\leadsto \color{blue}{x + \frac{y \cdot -2}{z \cdot \left(2 \cdot z\right) - y \cdot t} \cdot z} \]

   4. Taylor expanded in y around 0 92.8%

      \[\leadsto \color{blue}{-1 \cdot \frac{y}{z} + x} \]
   5. Step-by-step derivation

      1. +-commutative92.8%

         \[\leadsto \color{blue}{x + -1 \cdot \frac{y}{z}} \]

      2. mul-1-neg92.8%

         \[\leadsto x + \color{blue}{\left(-\frac{y}{z}\right)} \]

      3. sub-neg92.8%

         \[\leadsto \color{blue}{x - \frac{y}{z}} \]

   6. Simplified92.8%

      \[\leadsto \color{blue}{x - \frac{y}{z}} \]

   if -1.1399999999999999e-10 < z < 2.09999999999999989e-13

   1. Initial program 85.9%

      \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]
   2. Step-by-step derivation

      1. *-commutative85.9%

         \[\leadsto x - \frac{\color{blue}{z \cdot \left(y \cdot 2\right)}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]

      2. associate-/l*89.0%

         \[\leadsto x - \color{blue}{\frac{z}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{y \cdot 2}}} \]

      3. div-sub89.0%

         \[\leadsto x - \frac{z}{\color{blue}{\frac{\left(z \cdot 2\right) \cdot z}{y \cdot 2} - \frac{y \cdot t}{y \cdot 2}}} \]

      4. sub-neg89.0%

         \[\leadsto x - \frac{z}{\color{blue}{\frac{\left(z \cdot 2\right) \cdot z}{y \cdot 2} + \left(-\frac{y \cdot t}{y \cdot 2}\right)}} \]

      5. *-commutative89.0%

         \[\leadsto x - \frac{z}{\frac{\color{blue}{\left(2 \cdot z\right)} \cdot z}{y \cdot 2} + \left(-\frac{y \cdot t}{y \cdot 2}\right)} \]

      6. associate-*l*89.0%

         \[\leadsto x - \frac{z}{\frac{\color{blue}{2 \cdot \left(z \cdot z\right)}}{y \cdot 2} + \left(-\frac{y \cdot t}{y \cdot 2}\right)} \]

      7. *-commutative89.0%

         \[\leadsto x - \frac{z}{\frac{2 \cdot \left(z \cdot z\right)}{\color{blue}{2 \cdot y}} + \left(-\frac{y \cdot t}{y \cdot 2}\right)} \]

      8. times-frac89.0%

         \[\leadsto x - \frac{z}{\color{blue}{\frac{2}{2} \cdot \frac{z \cdot z}{y}} + \left(-\frac{y \cdot t}{y \cdot 2}\right)} \]

      9. metadata-eval89.0%

         \[\leadsto x - \frac{z}{\color{blue}{1} \cdot \frac{z \cdot z}{y} + \left(-\frac{y \cdot t}{y \cdot 2}\right)} \]

      10. *-lft-identity89.0%

          \[\leadsto x - \frac{z}{\color{blue}{\frac{z \cdot z}{y}} + \left(-\frac{y \cdot t}{y \cdot 2}\right)} \]

      11. associate-*r/93.9%

          \[\leadsto x - \frac{z}{\color{blue}{z \cdot \frac{z}{y}} + \left(-\frac{y \cdot t}{y \cdot 2}\right)} \]

      12. fma-def93.9%

          \[\leadsto x - \frac{z}{\color{blue}{\mathsf{fma}\left(z, \frac{z}{y}, -\frac{y \cdot t}{y \cdot 2}\right)}} \]

      13. associate-/r*93.9%

          \[\leadsto x - \frac{z}{\mathsf{fma}\left(z, \frac{z}{y}, -\color{blue}{\frac{\frac{y \cdot t}{y}}{2}}\right)} \]

      14. distribute-neg-frac93.9%

          \[\leadsto x - \frac{z}{\mathsf{fma}\left(z, \frac{z}{y}, \color{blue}{\frac{-\frac{y \cdot t}{y}}{2}}\right)} \]

      15. *-commutative93.9%

          \[\leadsto x - \frac{z}{\mathsf{fma}\left(z, \frac{z}{y}, \frac{-\frac{\color{blue}{t \cdot y}}{y}}{2}\right)} \]

      16. associate-/l*100.0%

          \[\leadsto x - \frac{z}{\mathsf{fma}\left(z, \frac{z}{y}, \frac{-\color{blue}{\frac{t}{\frac{y}{y}}}}{2}\right)} \]

      17. *-inverses100.0%

          \[\leadsto x - \frac{z}{\mathsf{fma}\left(z, \frac{z}{y}, \frac{-\frac{t}{\color{blue}{1}}}{2}\right)} \]

      18. /-rgt-identity100.0%

          \[\leadsto x - \frac{z}{\mathsf{fma}\left(z, \frac{z}{y}, \frac{-\color{blue}{t}}{2}\right)} \]

   3. Simplified100.0%

      \[\leadsto \color{blue}{x - \frac{z}{\mathsf{fma}\left(z, \frac{z}{y}, \frac{-t}{2}\right)}} \]

   4. Taylor expanded in z around 0 92.1%

      \[\leadsto x - \frac{z}{\color{blue}{-0.5 \cdot t}} \]
3. Recombined 2 regimes into one program.

4. Final simplification92.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -1.14 \cdot 10^{-10} \lor \neg \left(z \leq 2.1 \cdot 10^{-13}\right):\\ \;\;\;\;x - \frac{y}{z}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{z}{t \cdot -0.5}\\ \end{array} \]

1. Split input into 2 regimes

2. if z < -3.45e6 or 0.94999999999999996 < z

   1. Initial program 71.8%

      \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]
   2. Step-by-step derivation

      1. sub-neg71.8%

         \[\leadsto \color{blue}{x + \left(-\frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\right)} \]

      2. associate-/l*86.6%

         \[\leadsto x + \left(-\color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\right) \]

      3. distribute-neg-frac86.6%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}} \]

      4. associate-/r/86.6%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z} \]

      5. distribute-rgt-neg-in86.6%

         \[\leadsto x + \frac{\color{blue}{y \cdot \left(-2\right)}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      6. metadata-eval86.6%

         \[\leadsto x + \frac{y \cdot \color{blue}{-2}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      7. associate-*l*86.6%

         \[\leadsto x + \frac{y \cdot -2}{\color{blue}{z \cdot \left(2 \cdot z\right)} - y \cdot t} \cdot z \]

   3. Simplified86.6%

      \[\leadsto \color{blue}{x + \frac{y \cdot -2}{z \cdot \left(2 \cdot z\right) - y \cdot t} \cdot z} \]

   4. Taylor expanded in y around 0 93.2%

      \[\leadsto \color{blue}{-1 \cdot \frac{y}{z} + x} \]
   5. Step-by-step derivation

      1. +-commutative93.2%

         \[\leadsto \color{blue}{x + -1 \cdot \frac{y}{z}} \]

      2. mul-1-neg93.2%

         \[\leadsto x + \color{blue}{\left(-\frac{y}{z}\right)} \]

      3. sub-neg93.2%

         \[\leadsto \color{blue}{x - \frac{y}{z}} \]

   6. Simplified93.2%

      \[\leadsto \color{blue}{x - \frac{y}{z}} \]

   if -3.45e6 < z < 0.94999999999999996

   1. Initial program 86.4%

      \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]
   2. Step-by-step derivation

      1. sub-neg86.4%

         \[\leadsto \color{blue}{x + \left(-\frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\right)} \]

      2. associate-/l*88.6%

         \[\leadsto x + \left(-\color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\right) \]

      3. distribute-neg-frac88.6%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}} \]

      4. associate-/r/89.3%

         \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z} \]

      5. distribute-rgt-neg-in89.3%

         \[\leadsto x + \frac{\color{blue}{y \cdot \left(-2\right)}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      6. metadata-eval89.3%

         \[\leadsto x + \frac{y \cdot \color{blue}{-2}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

      7. associate-*l*89.3%

         \[\leadsto x + \frac{y \cdot -2}{\color{blue}{z \cdot \left(2 \cdot z\right)} - y \cdot t} \cdot z \]

   3. Simplified89.3%

      \[\leadsto \color{blue}{x + \frac{y \cdot -2}{z \cdot \left(2 \cdot z\right) - y \cdot t} \cdot z} \]

   4. Taylor expanded in x around inf 71.9%

      \[\leadsto \color{blue}{x} \]
3. Recombined 2 regimes into one program.

4. Final simplification82.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -3450000 \lor \neg \left(z \leq 0.95\right):\\ \;\;\;\;x - \frac{y}{z}\\ \mathbf{else}:\\ \;\;\;\;x\\ \end{array} \]

1. Initial program 79.1%

   \[x - \frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t} \]
2. Step-by-step derivation

   1. sub-neg79.1%

      \[\leadsto \color{blue}{x + \left(-\frac{\left(y \cdot 2\right) \cdot z}{\left(z \cdot 2\right) \cdot z - y \cdot t}\right)} \]

   2. associate-/l*87.6%

      \[\leadsto x + \left(-\color{blue}{\frac{y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}}\right) \]

   3. distribute-neg-frac87.6%

      \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\frac{\left(z \cdot 2\right) \cdot z - y \cdot t}{z}}} \]

   4. associate-/r/88.0%

      \[\leadsto x + \color{blue}{\frac{-y \cdot 2}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z} \]

   5. distribute-rgt-neg-in88.0%

      \[\leadsto x + \frac{\color{blue}{y \cdot \left(-2\right)}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

   6. metadata-eval88.0%

      \[\leadsto x + \frac{y \cdot \color{blue}{-2}}{\left(z \cdot 2\right) \cdot z - y \cdot t} \cdot z \]

   7. associate-*l*88.0%

      \[\leadsto x + \frac{y \cdot -2}{\color{blue}{z \cdot \left(2 \cdot z\right)} - y \cdot t} \cdot z \]

3. Simplified88.0%

   \[\leadsto \color{blue}{x + \frac{y \cdot -2}{z \cdot \left(2 \cdot z\right) - y \cdot t} \cdot z} \]

4. Taylor expanded in x around inf 74.5%

   \[\leadsto \color{blue}{x} \]

5. Final simplification74.5%

   \[\leadsto x \]

herbie shell --seed 2023166 
(FPCore (x y z t)
  :name "Numeric.AD.Rank1.Halley:findZero from ad-4.2.4"
  :precision binary64

  :herbie-target
  (- x (/ 1.0 (- (/ z y) (/ (/ t 2.0) z))))

  (- x (/ (* (* y 2.0) z) (- (* (* z 2.0) z) (* y t)))))