Radioactive exchange between two surfaces

1. Split input into 2 regimes

2. if x < 1.7599999999999999e149

   1. Initial program 93.5%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow93.4%

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

      2. sqr-pow93.2%

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

      3. difference-of-squares97.4%

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

      4. metadata-eval97.4%

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

      5. pow297.4%

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

      6. metadata-eval97.4%

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

      7. pow297.4%

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

      8. metadata-eval97.4%

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

      9. pow297.4%

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

      10. metadata-eval97.4%

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

      11. pow297.4%

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

   3. Applied egg-rr97.4%

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

   if 1.7599999999999999e149 < x

   1. Initial program 67.5%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow67.5%

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

      2. sqr-pow67.5%

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

      3. difference-of-squares80.0%

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

      4. metadata-eval80.0%

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

      5. pow280.0%

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

      6. metadata-eval80.0%

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

      7. pow280.0%

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

      8. metadata-eval80.0%

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

      9. pow280.0%

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

      10. metadata-eval80.0%

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

      11. pow280.0%

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

   3. Applied egg-rr80.0%

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

   4. Taylor expanded in x around inf 92.5%

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

      1. unpow292.5%

         \[\leadsto \left(x \cdot x + y \cdot y\right) \cdot \color{blue}{\left(x \cdot x\right)} \]

   6. Simplified92.5%

      \[\leadsto \left(x \cdot x + y \cdot y\right) \cdot \color{blue}{\left(x \cdot x\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification96.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 1.76 \cdot 10^{+149}:\\ \;\;\;\;\left(x \cdot x + y \cdot y\right) \cdot \left(x \cdot x - y \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot x\right) \cdot \left(x \cdot x + y \cdot y\right)\\ \end{array} \]

1. Split input into 3 regimes

2. if y < -2.6000000000000002e163

   1. Initial program 67.9%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow67.9%

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

      2. sqr-pow67.9%

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

      3. difference-of-squares75.0%

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

      4. metadata-eval75.0%

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

      5. pow275.0%

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

      6. metadata-eval75.0%

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

      7. pow275.0%

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

      8. metadata-eval75.0%

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

      9. pow275.0%

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

      10. metadata-eval75.0%

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

      11. pow275.0%

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

   3. Applied egg-rr75.0%

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

   4. Taylor expanded in x around 0 75.0%

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

      1. unpow275.0%

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

   6. Simplified75.0%

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

   7. Taylor expanded in x around 0 89.3%

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

      1. unpow289.3%

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

      2. mul-1-neg89.3%

         \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(-y \cdot y\right)} \]

      3. distribute-rgt-neg-out89.3%

         \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(y \cdot \left(-y\right)\right)} \]

   9. Simplified89.3%

      \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(y \cdot \left(-y\right)\right)} \]

   if -2.6000000000000002e163 < y < -5.8000000000000001e61 or 6.0000000000000001e-32 < y

   1. Initial program 81.8%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow81.8%

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

      2. sqr-pow81.7%

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

      3. difference-of-squares93.8%

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

      4. metadata-eval93.8%

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

      5. pow293.8%

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

      6. metadata-eval93.8%

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

      7. pow293.8%

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

      8. metadata-eval93.8%

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

      9. pow293.8%

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

      10. metadata-eval93.8%

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

      11. pow293.8%

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

   3. Applied egg-rr93.8%

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

   4. Taylor expanded in x around 0 90.5%

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

      1. unpow290.5%

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

   6. Simplified90.5%

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

   if -5.8000000000000001e61 < y < 6.0000000000000001e-32

   1. Initial program 100.0%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow99.7%

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

      2. sqr-pow99.6%

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

      3. difference-of-squares99.6%

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

      4. metadata-eval99.6%

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

      5. pow299.6%

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

      6. metadata-eval99.6%

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

      7. pow299.6%

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

      8. metadata-eval99.6%

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

      9. pow299.6%

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

      10. metadata-eval99.6%

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

      11. pow299.6%

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

   3. Applied egg-rr99.6%

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

   4. Taylor expanded in x around inf 90.6%

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

      1. unpow290.6%

         \[\leadsto \left(x \cdot x + y \cdot y\right) \cdot \color{blue}{\left(x \cdot x\right)} \]

   6. Simplified90.6%

      \[\leadsto \left(x \cdot x + y \cdot y\right) \cdot \color{blue}{\left(x \cdot x\right)} \]
3. Recombined 3 regimes into one program.

4. Final simplification90.4%

   \[\leadsto \begin{array}{l} \mathbf{if}\;y \leq -2.6 \cdot 10^{+163}:\\ \;\;\;\;\left(y \cdot y\right) \cdot \left(y \cdot \left(-y\right)\right)\\ \mathbf{elif}\;y \leq -5.8 \cdot 10^{+61} \lor \neg \left(y \leq 6 \cdot 10^{-32}\right):\\ \;\;\;\;\left(y \cdot y\right) \cdot \left(x \cdot x - y \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot x\right) \cdot \left(x \cdot x + y \cdot y\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if x < 1e152

   1. Initial program 93.6%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow93.4%

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

      2. sqr-pow93.3%

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

      3. difference-of-squares97.4%

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

      4. metadata-eval97.4%

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

      5. pow297.4%

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

      6. metadata-eval97.4%

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

      7. pow297.4%

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

      8. metadata-eval97.4%

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

      9. pow297.4%

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

      10. metadata-eval97.4%

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

      11. pow297.4%

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

   3. Applied egg-rr97.4%

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

   4. Taylor expanded in x around 0 68.6%

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

      1. unpow268.6%

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

   6. Simplified68.6%

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

   if 1e152 < x

   1. Initial program 65.8%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow65.8%

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

      2. sqr-pow65.8%

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

      3. difference-of-squares78.9%

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

      4. metadata-eval78.9%

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

      5. pow278.9%

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

      6. metadata-eval78.9%

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

      7. pow278.9%

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

      8. metadata-eval78.9%

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

      9. pow278.9%

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

      10. metadata-eval78.9%

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

      11. pow278.9%

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

   3. Applied egg-rr78.9%

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

   4. Taylor expanded in x around 0 65.8%

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

      1. unpow265.8%

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

   6. Simplified65.8%

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

   7. Taylor expanded in y around 0 78.9%

      \[\leadsto \color{blue}{{y}^{2} \cdot {x}^{2}} \]
   8. Step-by-step derivation

      1. unpow278.9%

         \[\leadsto \color{blue}{\left(y \cdot y\right)} \cdot {x}^{2} \]

      2. unpow278.9%

         \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(x \cdot x\right)} \]

   9. Simplified78.9%

      \[\leadsto \color{blue}{\left(y \cdot y\right) \cdot \left(x \cdot x\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 10^{+152}:\\ \;\;\;\;\left(y \cdot y\right) \cdot \left(x \cdot x - y \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot x\right) \cdot \left(y \cdot y\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if x < -1.25e113 or 3.89999999999999985e164 < x

   1. Initial program 70.4%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow70.4%

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

      2. sqr-pow70.4%

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

      3. difference-of-squares84.5%

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

      4. metadata-eval84.5%

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

      5. pow284.5%

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

      6. metadata-eval84.5%

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

      7. pow284.5%

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

      8. metadata-eval84.5%

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

      9. pow284.5%

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

      10. metadata-eval84.5%

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

      11. pow284.5%

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

   3. Applied egg-rr84.5%

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

   4. Taylor expanded in x around 0 59.4%

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

      1. unpow259.4%

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

   6. Simplified59.4%

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

   7. Taylor expanded in y around 0 66.4%

      \[\leadsto \color{blue}{{y}^{2} \cdot {x}^{2}} \]
   8. Step-by-step derivation

      1. unpow266.4%

         \[\leadsto \color{blue}{\left(y \cdot y\right)} \cdot {x}^{2} \]

      2. unpow266.4%

         \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(x \cdot x\right)} \]

   9. Simplified66.4%

      \[\leadsto \color{blue}{\left(y \cdot y\right) \cdot \left(x \cdot x\right)} \]

   if -1.25e113 < x < 3.89999999999999985e164

   1. Initial program 96.8%

      \[{x}^{4} - {y}^{4} \]
   2. Step-by-step derivation

      1. sqr-pow96.6%

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

      2. sqr-pow96.4%

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

      3. difference-of-squares98.6%

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

      4. metadata-eval98.6%

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

      5. pow298.6%

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

      6. metadata-eval98.6%

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

      7. pow298.6%

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

      8. metadata-eval98.6%

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

      9. pow298.6%

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

      10. metadata-eval98.6%

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

      11. pow298.6%

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

   3. Applied egg-rr98.6%

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

   4. Taylor expanded in x around 0 71.6%

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

      1. unpow271.6%

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

   6. Simplified71.6%

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

   7. Taylor expanded in x around 0 71.6%

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

      1. unpow271.6%

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

      2. mul-1-neg71.6%

         \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(-y \cdot y\right)} \]

      3. distribute-rgt-neg-out71.6%

         \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(y \cdot \left(-y\right)\right)} \]

   9. Simplified71.6%

      \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(y \cdot \left(-y\right)\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification70.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.25 \cdot 10^{+113} \lor \neg \left(x \leq 3.9 \cdot 10^{+164}\right):\\ \;\;\;\;\left(x \cdot x\right) \cdot \left(y \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;\left(y \cdot y\right) \cdot \left(y \cdot \left(-y\right)\right)\\ \end{array} \]

1. Initial program 89.5%

   \[{x}^{4} - {y}^{4} \]
2. Step-by-step derivation

   1. sqr-pow89.3%

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

   2. sqr-pow89.2%

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

   3. difference-of-squares94.7%

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

   4. metadata-eval94.7%

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

   5. pow294.7%

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

   6. metadata-eval94.7%

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

   7. pow294.7%

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

   8. metadata-eval94.7%

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

   9. pow294.7%

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

   10. metadata-eval94.7%

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

   11. pow294.7%

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

3. Applied egg-rr94.7%

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

4. Taylor expanded in x around 0 68.2%

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

   1. unpow268.2%

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

6. Simplified68.2%

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

7. Taylor expanded in y around 0 32.0%

   \[\leadsto \color{blue}{{y}^{2} \cdot {x}^{2}} \]
8. Step-by-step derivation

   1. unpow232.0%

      \[\leadsto \color{blue}{\left(y \cdot y\right)} \cdot {x}^{2} \]

   2. unpow232.0%

      \[\leadsto \left(y \cdot y\right) \cdot \color{blue}{\left(x \cdot x\right)} \]

9. Simplified32.0%

   \[\leadsto \color{blue}{\left(y \cdot y\right) \cdot \left(x \cdot x\right)} \]

10. Final simplification32.0%

    \[\leadsto \left(x \cdot x\right) \cdot \left(y \cdot y\right) \]

herbie shell --seed 2023166 
(FPCore (x y)
  :name "Radioactive exchange between two surfaces"
  :precision binary64
  (- (pow x 4.0) (pow y 4.0)))