1. Split input into 2 regimes

2. if z < -7.20000000000000016e202 or 6.9999999999999997e75 < z

   1. Initial program 59.2%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg59.2%

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

      2. +-commutative59.2%

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

      3. neg-sub059.2%

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

      4. associate-+l-59.2%

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

      5. sub0-neg59.2%

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

      6. neg-mul-159.2%

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

      7. sub-neg59.2%

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

      8. +-commutative59.2%

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

      9. neg-sub059.2%

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

      10. associate-+l-59.2%

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

      11. sub0-neg59.2%

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

      12. neg-mul-159.2%

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

      13. times-frac59.2%

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

      14. metadata-eval59.2%

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

      15. *-lft-identity59.2%

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

      16. *-commutative59.2%

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

   3. Simplified59.2%

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

   4. Taylor expanded in y around inf 48.9%

      \[\leadsto \color{blue}{\frac{y \cdot z}{a \cdot z - t}} \]
   5. Step-by-step derivation

      1. associate-/l*64.2%

         \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   6. Simplified64.2%

      \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   7. Taylor expanded in a around 0 86.5%

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

      1. mul-1-neg86.5%

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

      2. unsub-neg86.5%

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

   9. Simplified86.5%

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

   if -7.20000000000000016e202 < z < 6.9999999999999997e75

   1. Initial program 98.3%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
3. Recombined 2 regimes into one program.

4. Final simplification95.0%

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

1. Split input into 3 regimes

2. if z < -1.01999999999999995e143 or -5.40000000000000003e109 < z < -9.19999999999999993e-14 or 1.65e10 < z < 8.99999999999999953e120 or 3.00000000000000016e178 < z

   1. Initial program 75.0%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg75.0%

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

      2. +-commutative75.0%

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

      3. neg-sub075.0%

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

      4. associate-+l-75.0%

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

      5. sub0-neg75.0%

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

      6. neg-mul-175.0%

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

      7. sub-neg75.0%

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

      8. +-commutative75.0%

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

      9. neg-sub075.0%

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

      10. associate-+l-75.0%

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

      11. sub0-neg75.0%

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

      12. neg-mul-175.0%

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

      13. times-frac75.0%

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

      14. metadata-eval75.0%

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

      15. *-lft-identity75.0%

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

      16. *-commutative75.0%

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

   3. Simplified75.0%

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

   4. Taylor expanded in y around inf 60.7%

      \[\leadsto \color{blue}{\frac{y \cdot z}{a \cdot z - t}} \]
   5. Step-by-step derivation

      1. associate-/l*71.8%

         \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   6. Simplified71.8%

      \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   7. Taylor expanded in a around 0 84.3%

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

      1. mul-1-neg84.3%

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

      2. unsub-neg84.3%

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

   9. Simplified84.3%

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

   if -1.01999999999999995e143 < z < -5.40000000000000003e109 or -9.19999999999999993e-14 < z < 1.65e10

   1. Initial program 99.8%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg99.8%

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

      2. +-commutative99.8%

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

      3. neg-sub099.8%

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

      4. associate-+l-99.8%

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

      5. sub0-neg99.8%

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

      6. neg-mul-199.8%

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

      7. sub-neg99.8%

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

      8. +-commutative99.8%

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

      9. neg-sub099.8%

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

      10. associate-+l-99.8%

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

      11. sub0-neg99.8%

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

      12. neg-mul-199.8%

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

      13. times-frac99.8%

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

      14. metadata-eval99.8%

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

      15. *-lft-identity99.8%

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

      16. *-commutative99.8%

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

   3. Simplified99.8%

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

   4. Taylor expanded in y around 0 77.5%

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

      1. neg-mul-177.5%

         \[\leadsto \frac{\color{blue}{-x}}{z \cdot a - t} \]

   6. Simplified77.5%

      \[\leadsto \frac{\color{blue}{-x}}{z \cdot a - t} \]

   if 8.99999999999999953e120 < z < 3.00000000000000016e178

   1. Initial program 53.1%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg53.1%

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

      2. +-commutative53.1%

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

      3. neg-sub053.1%

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

      4. associate-+l-53.1%

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

      5. sub0-neg53.1%

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

      6. neg-mul-153.1%

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

      7. sub-neg53.1%

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

      8. +-commutative53.1%

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

      9. neg-sub053.1%

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

      10. associate-+l-53.1%

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

      11. sub0-neg53.1%

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

      12. neg-mul-153.1%

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

      13. times-frac53.1%

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

      14. metadata-eval53.1%

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

      15. *-lft-identity53.1%

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

      16. *-commutative53.1%

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

   3. Simplified53.1%

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

   4. Taylor expanded in a around inf 50.8%

      \[\leadsto \color{blue}{\left(\frac{y}{a} + \frac{t \cdot \left(y \cdot z - x\right)}{{a}^{2} \cdot {z}^{2}}\right) - \frac{x}{a \cdot z}} \]
   5. Step-by-step derivation

      1. +-commutative50.8%

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

      2. associate--l+50.8%

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

      3. associate-/l*59.9%

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

      4. *-commutative59.9%

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

      5. unpow259.9%

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

      6. unpow259.9%

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

      7. swap-sqr59.8%

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

      8. unpow259.8%

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

      9. associate-/r/59.8%

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

      10. *-commutative59.8%

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

      11. *-commutative59.8%

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

      12. *-commutative59.8%

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

      13. associate-/r*75.1%

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

   6. Simplified75.1%

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

   7. Taylor expanded in t around 0 76.5%

      \[\leadsto \color{blue}{\frac{y}{a} - \frac{x}{a \cdot z}} \]
   8. Step-by-step derivation

      1. associate-/l/91.8%

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

      2. div-sub91.7%

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

   9. Simplified91.7%

      \[\leadsto \color{blue}{\frac{y - \frac{x}{z}}{a}} \]
3. Recombined 3 regimes into one program.

4. Final simplification81.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -1.02 \cdot 10^{+143}:\\ \;\;\;\;\frac{y}{a - \frac{t}{z}}\\ \mathbf{elif}\;z \leq -5.4 \cdot 10^{+109}:\\ \;\;\;\;\frac{-x}{z \cdot a - t}\\ \mathbf{elif}\;z \leq -9.2 \cdot 10^{-14}:\\ \;\;\;\;\frac{y}{a - \frac{t}{z}}\\ \mathbf{elif}\;z \leq 16500000000:\\ \;\;\;\;\frac{-x}{z \cdot a - t}\\ \mathbf{elif}\;z \leq 9 \cdot 10^{+120} \lor \neg \left(z \leq 3 \cdot 10^{+178}\right):\\ \;\;\;\;\frac{y}{a - \frac{t}{z}}\\ \mathbf{else}:\\ \;\;\;\;\frac{y - \frac{x}{z}}{a}\\ \end{array} \]

1. Split input into 3 regimes

2. if z < -6.19999999999999987e-37 or 4.8e10 < z

   1. Initial program 75.4%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg75.4%

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

      2. +-commutative75.4%

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

      3. neg-sub075.4%

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

      4. associate-+l-75.4%

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

      5. sub0-neg75.4%

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

      6. neg-mul-175.4%

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

      7. sub-neg75.4%

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

      8. +-commutative75.4%

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

      9. neg-sub075.4%

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

      10. associate-+l-75.4%

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

      11. sub0-neg75.4%

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

      12. neg-mul-175.4%

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

      13. times-frac75.4%

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

      14. metadata-eval75.4%

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

      15. *-lft-identity75.4%

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

      16. *-commutative75.4%

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

   3. Simplified75.4%

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

   4. Taylor expanded in y around inf 55.2%

      \[\leadsto \color{blue}{\frac{y \cdot z}{a \cdot z - t}} \]
   5. Step-by-step derivation

      1. associate-/l*65.0%

         \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   6. Simplified65.0%

      \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   7. Taylor expanded in a around 0 77.2%

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

      1. mul-1-neg77.2%

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

      2. unsub-neg77.2%

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

   9. Simplified77.2%

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

   if -6.19999999999999987e-37 < z < -2.2000000000000001e-137

   1. Initial program 99.8%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg99.8%

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

      2. +-commutative99.8%

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

      3. neg-sub099.8%

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

      4. associate-+l-99.8%

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

      5. sub0-neg99.8%

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

      6. neg-mul-199.8%

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

      7. sub-neg99.8%

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

      8. +-commutative99.8%

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

      9. neg-sub099.8%

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

      10. associate-+l-99.8%

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

      11. sub0-neg99.8%

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

      12. neg-mul-199.8%

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

      13. times-frac99.8%

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

      14. metadata-eval99.8%

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

      15. *-lft-identity99.8%

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

      16. *-commutative99.8%

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

   3. Simplified99.8%

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

   4. Taylor expanded in a around inf 68.4%

      \[\leadsto \color{blue}{\left(\frac{y}{a} + \frac{t \cdot \left(y \cdot z - x\right)}{{a}^{2} \cdot {z}^{2}}\right) - \frac{x}{a \cdot z}} \]
   5. Step-by-step derivation

      1. +-commutative68.4%

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

      2. associate--l+68.4%

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

      3. associate-/l*65.1%

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

      4. *-commutative65.1%

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

      5. unpow265.1%

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

      6. unpow265.1%

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

      7. swap-sqr65.1%

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

      8. unpow265.1%

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

      9. associate-/r/68.4%

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

      10. *-commutative68.4%

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

      11. *-commutative68.4%

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

      12. *-commutative68.4%

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

      13. associate-/r*64.6%

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

   6. Simplified64.6%

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

   7. Taylor expanded in t around 0 72.6%

      \[\leadsto \color{blue}{\frac{y}{a} - \frac{x}{a \cdot z}} \]
   8. Step-by-step derivation

      1. associate-/l/68.8%

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

      2. div-sub68.8%

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

   9. Simplified68.8%

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

   if -2.2000000000000001e-137 < z < 4.8e10

   1. Initial program 99.8%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg99.8%

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

      2. +-commutative99.8%

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

      3. neg-sub099.8%

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

      4. associate-+l-99.8%

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

      5. sub0-neg99.8%

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

      6. neg-mul-199.8%

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

      7. sub-neg99.8%

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

      8. +-commutative99.8%

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

      9. neg-sub099.8%

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

      10. associate-+l-99.8%

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

      11. sub0-neg99.8%

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

      12. neg-mul-199.8%

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

      13. times-frac99.8%

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

      14. metadata-eval99.8%

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

      15. *-lft-identity99.8%

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

      16. *-commutative99.8%

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

   3. Simplified99.8%

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

   4. Taylor expanded in a around 0 69.2%

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

      1. associate-*r/69.2%

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

      2. neg-mul-169.2%

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

      3. neg-sub069.2%

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

      4. sub-neg69.2%

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

      5. +-commutative69.2%

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

      6. associate--r+69.2%

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

      7. neg-sub069.2%

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

      8. remove-double-neg69.2%

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

      9. *-commutative69.2%

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

   6. Simplified69.2%

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

4. Final simplification73.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -6.2 \cdot 10^{-37}:\\ \;\;\;\;\frac{y}{a - \frac{t}{z}}\\ \mathbf{elif}\;z \leq -2.2 \cdot 10^{-137}:\\ \;\;\;\;\frac{y - \frac{x}{z}}{a}\\ \mathbf{elif}\;z \leq 48000000000:\\ \;\;\;\;\frac{x - z \cdot y}{t}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{a - \frac{t}{z}}\\ \end{array} \]

1. Split input into 2 regimes

2. if z < -1.3e22 or -3.5e-126 < z < -2.2000000000000001e-137 or 7.0000000000000002e32 < z

   1. Initial program 74.4%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg74.4%

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

      2. +-commutative74.4%

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

      3. neg-sub074.4%

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

      4. associate-+l-74.4%

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

      5. sub0-neg74.4%

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

      6. neg-mul-174.4%

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

      7. sub-neg74.4%

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

      8. +-commutative74.4%

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

      9. neg-sub074.4%

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

      10. associate-+l-74.4%

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

      11. sub0-neg74.4%

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

      12. neg-mul-174.4%

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

      13. times-frac74.4%

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

      14. metadata-eval74.4%

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

      15. *-lft-identity74.4%

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

      16. *-commutative74.4%

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

   3. Simplified74.4%

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

   4. Taylor expanded in z around inf 53.6%

      \[\leadsto \color{blue}{\frac{y}{a}} \]

   if -1.3e22 < z < -3.5e-126 or -2.2000000000000001e-137 < z < 7.0000000000000002e32

   1. Initial program 99.8%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg99.8%

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

      2. +-commutative99.8%

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

      3. neg-sub099.8%

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

      4. associate-+l-99.8%

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

      5. sub0-neg99.8%

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

      6. neg-mul-199.8%

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

      7. sub-neg99.8%

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

      8. +-commutative99.8%

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

      9. neg-sub099.8%

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

      10. associate-+l-99.8%

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

      11. sub0-neg99.8%

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

      12. neg-mul-199.8%

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

      13. times-frac99.8%

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

      14. metadata-eval99.8%

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

      15. *-lft-identity99.8%

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

      16. *-commutative99.8%

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

   3. Simplified99.8%

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

   4. Taylor expanded in z around 0 50.8%

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

4. Final simplification52.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -1.3 \cdot 10^{+22} \lor \neg \left(z \leq -3.5 \cdot 10^{-126}\right) \land \left(z \leq -2.2 \cdot 10^{-137} \lor \neg \left(z \leq 7 \cdot 10^{+32}\right)\right):\\ \;\;\;\;\frac{y}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{t}\\ \end{array} \]

1. Split input into 2 regimes

2. if z < -1.25000000000000001e-151 or 5.5999999999999998e-89 < z

   1. Initial program 81.7%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg81.7%

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

      2. +-commutative81.7%

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

      3. neg-sub081.7%

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

      4. associate-+l-81.7%

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

      5. sub0-neg81.7%

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

      6. neg-mul-181.7%

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

      7. sub-neg81.7%

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

      8. +-commutative81.7%

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

      9. neg-sub081.7%

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

      10. associate-+l-81.7%

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

      11. sub0-neg81.7%

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

      12. neg-mul-181.7%

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

      13. times-frac81.7%

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

      14. metadata-eval81.7%

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

      15. *-lft-identity81.7%

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

      16. *-commutative81.7%

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

   3. Simplified81.7%

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

   4. Taylor expanded in y around inf 51.3%

      \[\leadsto \color{blue}{\frac{y \cdot z}{a \cdot z - t}} \]
   5. Step-by-step derivation

      1. associate-/l*58.5%

         \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   6. Simplified58.5%

      \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   7. Taylor expanded in a around 0 67.6%

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

      1. mul-1-neg67.6%

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

      2. unsub-neg67.6%

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

   9. Simplified67.6%

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

   if -1.25000000000000001e-151 < z < 5.5999999999999998e-89

   1. Initial program 99.9%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg99.9%

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

      2. +-commutative99.9%

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

      3. neg-sub099.9%

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

      4. associate-+l-99.9%

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

      5. sub0-neg99.9%

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

      6. neg-mul-199.9%

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

      7. sub-neg99.9%

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

      8. +-commutative99.9%

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

      9. neg-sub099.9%

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

      10. associate-+l-99.9%

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

      11. sub0-neg99.9%

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

      12. neg-mul-199.9%

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

      13. times-frac99.9%

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

      14. metadata-eval99.9%

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

      15. *-lft-identity99.9%

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

      16. *-commutative99.9%

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

   3. Simplified99.9%

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

   4. Taylor expanded in z around 0 59.5%

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

4. Final simplification65.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -1.25 \cdot 10^{-151} \lor \neg \left(z \leq 5.6 \cdot 10^{-89}\right):\\ \;\;\;\;\frac{y}{a - \frac{t}{z}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x}{t}\\ \end{array} \]

1. Split input into 2 regimes

2. if z < -1.25000000000000001e-151 or 2.2e9 < z

   1. Initial program 79.6%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg79.6%

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

      2. +-commutative79.6%

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

      3. neg-sub079.6%

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

      4. associate-+l-79.6%

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

      5. sub0-neg79.6%

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

      6. neg-mul-179.6%

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

      7. sub-neg79.6%

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

      8. +-commutative79.6%

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

      9. neg-sub079.6%

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

      10. associate-+l-79.6%

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

      11. sub0-neg79.6%

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

      12. neg-mul-179.6%

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

      13. times-frac79.6%

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

      14. metadata-eval79.6%

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

      15. *-lft-identity79.6%

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

      16. *-commutative79.6%

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

   3. Simplified79.6%

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

   4. Taylor expanded in y around inf 53.6%

      \[\leadsto \color{blue}{\frac{y \cdot z}{a \cdot z - t}} \]
   5. Step-by-step derivation

      1. associate-/l*61.7%

         \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   6. Simplified61.7%

      \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   7. Taylor expanded in a around 0 71.9%

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

      1. mul-1-neg71.9%

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

      2. unsub-neg71.9%

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

   9. Simplified71.9%

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

   if -1.25000000000000001e-151 < z < 2.2e9

   1. Initial program 99.8%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg99.8%

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

      2. +-commutative99.8%

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

      3. neg-sub099.8%

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

      4. associate-+l-99.8%

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

      5. sub0-neg99.8%

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

      6. neg-mul-199.8%

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

      7. sub-neg99.8%

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

      8. +-commutative99.8%

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

      9. neg-sub099.8%

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

      10. associate-+l-99.8%

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

      11. sub0-neg99.8%

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

      12. neg-mul-199.8%

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

      13. times-frac99.8%

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

      14. metadata-eval99.8%

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

      15. *-lft-identity99.8%

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

      16. *-commutative99.8%

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

   3. Simplified99.8%

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

   4. Taylor expanded in a around 0 69.5%

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

      1. associate-*r/69.5%

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

      2. neg-mul-169.5%

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

      3. neg-sub069.5%

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

      4. sub-neg69.5%

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

      5. +-commutative69.5%

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

      6. associate--r+69.5%

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

      7. neg-sub069.5%

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

      8. remove-double-neg69.5%

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

      9. *-commutative69.5%

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

   6. Simplified69.5%

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

4. Final simplification71.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -1.25 \cdot 10^{-151} \lor \neg \left(z \leq 2200000000\right):\\ \;\;\;\;\frac{y}{a - \frac{t}{z}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x - z \cdot y}{t}\\ \end{array} \]

1. Split input into 3 regimes

2. if z < -9.80000000000000042e231 or 2.7499999999999998e34 < z

   1. Initial program 63.3%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg63.3%

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

      2. +-commutative63.3%

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

      3. neg-sub063.3%

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

      4. associate-+l-63.3%

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

      5. sub0-neg63.3%

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

      6. neg-mul-163.3%

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

      7. sub-neg63.3%

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

      8. +-commutative63.3%

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

      9. neg-sub063.3%

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

      10. associate-+l-63.3%

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

      11. sub0-neg63.3%

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

      12. neg-mul-163.3%

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

      13. times-frac63.3%

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

      14. metadata-eval63.3%

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

      15. *-lft-identity63.3%

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

      16. *-commutative63.3%

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

   3. Simplified63.3%

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

   4. Taylor expanded in z around inf 66.9%

      \[\leadsto \color{blue}{\frac{y}{a}} \]

   if -9.80000000000000042e231 < z < -1.21999999999999996e-29

   1. Initial program 89.2%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg89.2%

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

      2. +-commutative89.2%

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

      3. neg-sub089.2%

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

      4. associate-+l-89.2%

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

      5. sub0-neg89.2%

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

      6. neg-mul-189.2%

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

      7. sub-neg89.2%

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

      8. +-commutative89.2%

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

      9. neg-sub089.2%

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

      10. associate-+l-89.2%

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

      11. sub0-neg89.2%

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

      12. neg-mul-189.2%

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

      13. times-frac89.2%

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

      14. metadata-eval89.2%

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

      15. *-lft-identity89.2%

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

      16. *-commutative89.2%

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

   3. Simplified89.2%

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

   4. Taylor expanded in y around inf 56.1%

      \[\leadsto \color{blue}{\frac{y \cdot z}{a \cdot z - t}} \]
   5. Step-by-step derivation

      1. *-commutative56.1%

         \[\leadsto \frac{y \cdot z}{\color{blue}{z \cdot a} - t} \]

      2. associate-*r/64.9%

         \[\leadsto \color{blue}{y \cdot \frac{z}{z \cdot a - t}} \]

      3. *-commutative64.9%

         \[\leadsto y \cdot \frac{z}{\color{blue}{a \cdot z} - t} \]

      4. fma-neg64.9%

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

   6. Simplified64.9%

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

   7. Taylor expanded in z around 0 43.7%

      \[\leadsto y \cdot \color{blue}{\left(-1 \cdot \frac{z}{t}\right)} \]
   8. Step-by-step derivation

      1. associate-*r/43.7%

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

      2. neg-mul-143.7%

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

   9. Simplified43.7%

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

   if -1.21999999999999996e-29 < z < 2.7499999999999998e34

   1. Initial program 99.8%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg99.8%

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

      2. +-commutative99.8%

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

      3. neg-sub099.8%

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

      4. associate-+l-99.8%

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

      5. sub0-neg99.8%

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

      6. neg-mul-199.8%

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

      7. sub-neg99.8%

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

      8. +-commutative99.8%

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

      9. neg-sub099.8%

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

      10. associate-+l-99.8%

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

      11. sub0-neg99.8%

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

      12. neg-mul-199.8%

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

      13. times-frac99.8%

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

      14. metadata-eval99.8%

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

      15. *-lft-identity99.8%

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

      16. *-commutative99.8%

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

   3. Simplified99.8%

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

   4. Taylor expanded in z around 0 49.4%

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

4. Final simplification53.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -9.8 \cdot 10^{+231}:\\ \;\;\;\;\frac{y}{a}\\ \mathbf{elif}\;z \leq -1.22 \cdot 10^{-29}:\\ \;\;\;\;y \cdot \frac{-z}{t}\\ \mathbf{elif}\;z \leq 2.75 \cdot 10^{+34}:\\ \;\;\;\;\frac{x}{t}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{a}\\ \end{array} \]

1. Split input into 3 regimes

2. if z < -9.80000000000000042e231 or 1.99999999999999988e39 < z

   1. Initial program 63.3%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg63.3%

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

      2. +-commutative63.3%

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

      3. neg-sub063.3%

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

      4. associate-+l-63.3%

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

      5. sub0-neg63.3%

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

      6. neg-mul-163.3%

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

      7. sub-neg63.3%

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

      8. +-commutative63.3%

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

      9. neg-sub063.3%

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

      10. associate-+l-63.3%

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

      11. sub0-neg63.3%

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

      12. neg-mul-163.3%

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

      13. times-frac63.3%

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

      14. metadata-eval63.3%

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

      15. *-lft-identity63.3%

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

      16. *-commutative63.3%

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

   3. Simplified63.3%

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

   4. Taylor expanded in z around inf 66.9%

      \[\leadsto \color{blue}{\frac{y}{a}} \]

   if -9.80000000000000042e231 < z < -2.2999999999999998e-22

   1. Initial program 89.2%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg89.2%

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

      2. +-commutative89.2%

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

      3. neg-sub089.2%

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

      4. associate-+l-89.2%

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

      5. sub0-neg89.2%

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

      6. neg-mul-189.2%

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

      7. sub-neg89.2%

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

      8. +-commutative89.2%

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

      9. neg-sub089.2%

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

      10. associate-+l-89.2%

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

      11. sub0-neg89.2%

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

      12. neg-mul-189.2%

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

      13. times-frac89.2%

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

      14. metadata-eval89.2%

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

      15. *-lft-identity89.2%

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

      16. *-commutative89.2%

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

   3. Simplified89.2%

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

   4. Taylor expanded in y around inf 56.1%

      \[\leadsto \color{blue}{\frac{y \cdot z}{a \cdot z - t}} \]
   5. Step-by-step derivation

      1. associate-/l*64.8%

         \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   6. Simplified64.8%

      \[\leadsto \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}} \]

   7. Taylor expanded in a around 0 43.7%

      \[\leadsto \frac{y}{\color{blue}{-1 \cdot \frac{t}{z}}} \]
   8. Step-by-step derivation

      1. associate-*r/43.7%

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

      2. neg-mul-143.7%

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

   9. Simplified43.7%

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

   if -2.2999999999999998e-22 < z < 1.99999999999999988e39

   1. Initial program 99.8%

      \[\frac{x - y \cdot z}{t - a \cdot z} \]
   2. Step-by-step derivation

      1. sub-neg99.8%

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

      2. +-commutative99.8%

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

      3. neg-sub099.8%

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

      4. associate-+l-99.8%

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

      5. sub0-neg99.8%

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

      6. neg-mul-199.8%

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

      7. sub-neg99.8%

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

      8. +-commutative99.8%

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

      9. neg-sub099.8%

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

      10. associate-+l-99.8%

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

      11. sub0-neg99.8%

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

      12. neg-mul-199.8%

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

      13. times-frac99.8%

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

      14. metadata-eval99.8%

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

      15. *-lft-identity99.8%

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

      16. *-commutative99.8%

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

   3. Simplified99.8%

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

   4. Taylor expanded in z around 0 49.4%

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

4. Final simplification53.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -9.8 \cdot 10^{+231}:\\ \;\;\;\;\frac{y}{a}\\ \mathbf{elif}\;z \leq -2.3 \cdot 10^{-22}:\\ \;\;\;\;\frac{y}{\frac{-t}{z}}\\ \mathbf{elif}\;z \leq 2 \cdot 10^{+39}:\\ \;\;\;\;\frac{x}{t}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{a}\\ \end{array} \]

1. Initial program 87.4%

   \[\frac{x - y \cdot z}{t - a \cdot z} \]
2. Step-by-step derivation

   1. sub-neg87.4%

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

   2. +-commutative87.4%

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

   3. neg-sub087.4%

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

   4. associate-+l-87.4%

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

   5. sub0-neg87.4%

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

   6. neg-mul-187.4%

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

   7. sub-neg87.4%

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

   8. +-commutative87.4%

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

   9. neg-sub087.4%

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

   10. associate-+l-87.4%

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

   11. sub0-neg87.4%

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

   12. neg-mul-187.4%

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

   13. times-frac87.4%

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

   14. metadata-eval87.4%

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

   15. *-lft-identity87.4%

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

   16. *-commutative87.4%

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

3. Simplified87.4%

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

4. Taylor expanded in z around 0 33.2%

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

5. Final simplification33.2%

   \[\leadsto \frac{x}{t} \]

herbie shell --seed 2023166 
(FPCore (x y z t a)
  :name "Diagrams.Solve.Tridiagonal:solveTriDiagonal from diagrams-solve-0.1, A"
  :precision binary64

  :herbie-target
  (if (< z -32113435955957344.0) (- (/ x (- t (* a z))) (/ y (- (/ t z) a))) (if (< z 3.5139522372978296e-86) (* (- x (* y z)) (/ 1.0 (- t (* a z)))) (- (/ x (- t (* a z))) (/ y (- (/ t z) a)))))

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