Disney BSSRDF, PDF of scattering profile

Percentage Accurate: 99.6% → 99.6%
Time: 16.2s
Alternatives: 5
Speedup: 1.0×

Specification

?
\[\left(0 \leq s \land s \leq 256\right) \land \left(10^{-6} < r \land r < 1000000\right)\]
\[\begin{array}{l} \\ \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \end{array} \]
(FPCore (s r)
 :precision binary32
 (+
  (/ (* 0.25 (exp (/ (- r) s))) (* (* (* 2.0 (PI)) s) r))
  (/ (* 0.75 (exp (/ (- r) (* 3.0 s)))) (* (* (* 6.0 (PI)) s) r))))
\begin{array}{l}

\\
\frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r}
\end{array}

Sampling outcomes in binary32 precision:

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 5 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 99.6% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \end{array} \]
(FPCore (s r)
 :precision binary32
 (+
  (/ (* 0.25 (exp (/ (- r) s))) (* (* (* 2.0 (PI)) s) r))
  (/ (* 0.75 (exp (/ (- r) (* 3.0 s)))) (* (* (* 6.0 (PI)) s) r))))
\begin{array}{l}

\\
\frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r}
\end{array}

Alternative 1: 99.6% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(s + s\right) \cdot \mathsf{PI}\left(\right)\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \end{array} \]
(FPCore (s r)
 :precision binary32
 (+
  (/ (* 0.25 (exp (/ (- r) s))) (* (* (+ s s) (PI)) r))
  (/ (* 0.75 (exp (/ (- r) (* 3.0 s)))) (* (* s r) (* 6.0 (PI))))))
\begin{array}{l}

\\
\frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(s + s\right) \cdot \mathsf{PI}\left(\right)\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)}
\end{array}
Derivation
  1. Initial program 99.6%

    \[\frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-literalN/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(\color{blue}{6} \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
    2. lift-PI.f32N/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot s\right) \cdot r} \]
    3. lift-*.f32N/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\color{blue}{\left(6 \cdot \mathsf{PI}\left(\right)\right)} \cdot s\right) \cdot r} \]
    4. lift-varN/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{s}\right) \cdot r} \]
    5. lift-*.f32N/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right)} \cdot r} \]
    6. lift-varN/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot \color{blue}{r}} \]
    7. lift-*.f32N/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r}} \]
    8. lower-*.f32N/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(s \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)}} \]
    9. lower-*.f32N/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(s \cdot r\right)} \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \]
    10. lift-varN/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\color{blue}{s} \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \]
    11. lift-varN/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot \color{blue}{r}\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \]
    12. lift-*.f32N/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \color{blue}{\left(6 \cdot \mathsf{PI}\left(\right)\right)}} \]
    13. lift-literalN/A

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \left(\color{blue}{6} \cdot \mathsf{PI}\left(\right)\right)} \]
    14. lift-PI.f3299.6

      \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \left(6 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \]
  4. Applied rewrites99.6%

    \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(s \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)}} \]
  5. Taylor expanded in s around 0

    \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\color{blue}{\left(2 \cdot \left(s \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \]
  6. Step-by-step derivation
    1. Applied rewrites99.6%

      \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\color{blue}{\left(\left(s + s\right) \cdot \mathsf{PI}\left(\right)\right)} \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \]
    2. Add Preprocessing

    Alternative 2: 99.6% accurate, 1.0× speedup?

    \[\begin{array}{l} \\ \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(s + s\right) \cdot \mathsf{PI}\left(\right)\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \end{array} \]
    (FPCore (s r)
     :precision binary32
     (+
      (/ (* 0.25 (exp (/ (- r) s))) (* (* (+ s s) (PI)) r))
      (/ (* 0.75 (exp (/ (- r) (* 3.0 s)))) (* (* (* 6.0 (PI)) s) r))))
    \begin{array}{l}
    
    \\
    \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(s + s\right) \cdot \mathsf{PI}\left(\right)\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r}
    \end{array}
    
    Derivation
    1. Initial program 99.6%

      \[\frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
    2. Add Preprocessing
    3. Taylor expanded in s around 0

      \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\color{blue}{\left(2 \cdot \left(s \cdot \mathsf{PI}\left(\right)\right)\right)} \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
    4. Step-by-step derivation
      1. Applied rewrites99.6%

        \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\color{blue}{\left(\left(s + s\right) \cdot \mathsf{PI}\left(\right)\right)} \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
      2. Final simplification99.6%

        \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(s + s\right) \cdot \mathsf{PI}\left(\right)\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
      3. Add Preprocessing

      Alternative 3: 99.6% accurate, 1.0× speedup?

      \[\begin{array}{l} \\ \frac{\frac{\mathsf{fma}\left(0.75, \frac{e^{\frac{-r}{3 \cdot s}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot 0.25\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \end{array} \]
      (FPCore (s r)
       :precision binary32
       (/
        (/
         (fma
          0.75
          (/ (exp (/ (- r) (* 3.0 s))) 6.0)
          (* (/ (exp (/ (- r) s)) 2.0) 0.25))
         (PI))
        (* s r)))
      \begin{array}{l}
      
      \\
      \frac{\frac{\mathsf{fma}\left(0.75, \frac{e^{\frac{-r}{3 \cdot s}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot 0.25\right)}{\mathsf{PI}\left(\right)}}{s \cdot r}
      \end{array}
      
      Derivation
      1. Initial program 99.6%

        \[\frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-literalN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(\color{blue}{6} \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
        2. lift-PI.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot s\right) \cdot r} \]
        3. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\color{blue}{\left(6 \cdot \mathsf{PI}\left(\right)\right)} \cdot s\right) \cdot r} \]
        4. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{s}\right) \cdot r} \]
        5. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right)} \cdot r} \]
        6. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot \color{blue}{r}} \]
        7. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r}} \]
        8. lower-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(s \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)}} \]
        9. lower-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(s \cdot r\right)} \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \]
        10. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\color{blue}{s} \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \]
        11. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot \color{blue}{r}\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)} \]
        12. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \color{blue}{\left(6 \cdot \mathsf{PI}\left(\right)\right)}} \]
        13. lift-literalN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \left(\color{blue}{6} \cdot \mathsf{PI}\left(\right)\right)} \]
        14. lift-PI.f3299.6

          \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(s \cdot r\right) \cdot \left(6 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right)} \]
      4. Applied rewrites99.6%

        \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(s \cdot r\right) \cdot \left(6 \cdot \mathsf{PI}\left(\right)\right)}} \]
      5. Applied rewrites98.6%

        \[\leadsto \color{blue}{\frac{\frac{\mathsf{fma}\left(0.75, \frac{\sqrt[3]{e^{\frac{-r}{s}}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot 0.25\right)}{\mathsf{PI}\left(\right)}}{s \cdot r}} \]
      6. Applied rewrites99.5%

        \[\leadsto \frac{\frac{\mathsf{fma}\left(0.75, \frac{\color{blue}{e^{\frac{\frac{-r}{s}}{3}}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot 0.25\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
      7. Step-by-step derivation
        1. lift-varN/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{\frac{-\color{blue}{r}}{s}}{3}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        2. lift-neg.f32N/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{\frac{\color{blue}{\mathsf{neg}\left(r\right)}}{s}}{3}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        3. lift-varN/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{\frac{\mathsf{neg}\left(r\right)}{\color{blue}{s}}}{3}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        4. lift-/.f32N/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{\color{blue}{\frac{\mathsf{neg}\left(r\right)}{s}}}{3}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        5. lift-literalN/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{\frac{\mathsf{neg}\left(r\right)}{s}}{\color{blue}{3}}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        6. lift-/.f32N/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\color{blue}{\frac{\frac{\mathsf{neg}\left(r\right)}{s}}{3}}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        7. lift-/.f32N/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\color{blue}{\frac{\mathsf{neg}\left(r\right)}{3 \cdot s}}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        8. lift-neg.f32N/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{\color{blue}{-r}}{3 \cdot s}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        9. lift-varN/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{-\color{blue}{r}}{3 \cdot s}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        10. lift-*.f32N/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{-r}{\color{blue}{3 \cdot s}}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        11. lift-literalN/A

          \[\leadsto \frac{\frac{\mathsf{fma}\left(\frac{3}{4}, \frac{e^{\frac{-r}{\color{blue}{3} \cdot s}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot \frac{1}{4}\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
        12. lift-var99.5

          \[\leadsto \frac{\frac{\mathsf{fma}\left(0.75, \frac{e^{\frac{-r}{3 \cdot \color{blue}{s}}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot 0.25\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
      8. Applied rewrites99.5%

        \[\leadsto \frac{\frac{\mathsf{fma}\left(0.75, \frac{e^{\color{blue}{\frac{-r}{3 \cdot s}}}}{6}, \frac{e^{\frac{-r}{s}}}{2} \cdot 0.25\right)}{\mathsf{PI}\left(\right)}}{s \cdot r} \]
      9. Add Preprocessing

      Alternative 4: 93.0% accurate, 1.0× speedup?

      \[\begin{array}{l} \\ \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \end{array} \]
      (FPCore (s r)
       :precision binary32
       (+
        (/ (* 0.25 (exp (/ (- r) s))) (* (+ (PI) (PI)) r))
        (/ (* 0.75 (exp (/ (- r) (* 3.0 s)))) (* (* r 6.0) (* (PI) s)))))
      \begin{array}{l}
      
      \\
      \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)}
      \end{array}
      
      Derivation
      1. Initial program 99.6%

        \[\frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-literalN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(\color{blue}{6} \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
        2. lift-PI.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot s\right) \cdot r} \]
        3. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\color{blue}{\left(6 \cdot \mathsf{PI}\left(\right)\right)} \cdot s\right) \cdot r} \]
        4. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{s}\right) \cdot r} \]
        5. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right)} \cdot r} \]
        6. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot \color{blue}{r}} \]
        7. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r}} \]
        8. lower-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)}} \]
        9. lower-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(r \cdot 6\right)} \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        10. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\color{blue}{r} \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        11. lift-literalN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot \color{blue}{6}\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        12. lower-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot s\right)}} \]
        13. lift-PI.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\color{blue}{\mathsf{PI}\left(\right)} \cdot s\right)} \]
        14. lift-var99.6

          \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{s}\right)} \]
      4. Applied rewrites99.6%

        \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)}} \]
      5. Step-by-step derivation
        1. lift-literalN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(\color{blue}{2} \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        2. lift-PI.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        3. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right)} \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        4. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{s}\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        5. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right)} \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
      6. Applied rewrites93.5%

        \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\color{blue}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)} \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
      7. Add Preprocessing

      Alternative 5: 92.9% accurate, 1.0× speedup?

      \[\begin{array}{l} \\ e^{\frac{-r}{s}} \cdot \frac{0.25}{2 \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \end{array} \]
      (FPCore (s r)
       :precision binary32
       (+
        (* (exp (/ (- r) s)) (/ 0.25 (* 2.0 r)))
        (/ (* 0.75 (exp (/ (- r) (* 3.0 s)))) (* (* r 6.0) (* (PI) s)))))
      \begin{array}{l}
      
      \\
      e^{\frac{-r}{s}} \cdot \frac{0.25}{2 \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)}
      \end{array}
      
      Derivation
      1. Initial program 99.6%

        \[\frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-literalN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(\color{blue}{6} \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} \]
        2. lift-PI.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot s\right) \cdot r} \]
        3. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\color{blue}{\left(6 \cdot \mathsf{PI}\left(\right)\right)} \cdot s\right) \cdot r} \]
        4. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{s}\right) \cdot r} \]
        5. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right)} \cdot r} \]
        6. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot \color{blue}{r}} \]
        7. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(\left(6 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r}} \]
        8. lower-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)}} \]
        9. lower-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(r \cdot 6\right)} \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        10. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(\color{blue}{r} \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        11. lift-literalN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot \color{blue}{6}\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        12. lower-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \color{blue}{\left(\mathsf{PI}\left(\right) \cdot s\right)}} \]
        13. lift-PI.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\color{blue}{\mathsf{PI}\left(\right)} \cdot s\right)} \]
        14. lift-var99.6

          \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot \color{blue}{s}\right)} \]
      4. Applied rewrites99.6%

        \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\color{blue}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)}} \]
      5. Step-by-step derivation
        1. lift-literalN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(\color{blue}{2} \cdot \mathsf{PI}\left(\right)\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        2. lift-PI.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \color{blue}{\mathsf{PI}\left(\right)}\right) \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        3. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\color{blue}{\left(2 \cdot \mathsf{PI}\left(\right)\right)} \cdot s\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        4. lift-varN/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot \color{blue}{s}\right) \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
        5. lift-*.f32N/A

          \[\leadsto \frac{\frac{1}{4} \cdot e^{\frac{-r}{s}}}{\color{blue}{\left(\left(2 \cdot \mathsf{PI}\left(\right)\right) \cdot s\right)} \cdot r} + \frac{\frac{3}{4} \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
      6. Applied rewrites93.5%

        \[\leadsto \frac{0.25 \cdot e^{\frac{-r}{s}}}{\color{blue}{\left(\mathsf{PI}\left(\right) + \mathsf{PI}\left(\right)\right)} \cdot r} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
      7. Applied rewrites93.5%

        \[\leadsto \color{blue}{e^{\frac{-r}{s}} \cdot \frac{0.25}{2 \cdot r}} + \frac{0.75 \cdot e^{\frac{-r}{3 \cdot s}}}{\left(r \cdot 6\right) \cdot \left(\mathsf{PI}\left(\right) \cdot s\right)} \]
      8. Add Preprocessing

      Reproduce

      ?
      herbie shell --seed 2025021 
      (FPCore (s r)
        :name "Disney BSSRDF, PDF of scattering profile"
        :precision binary32
        :pre (and (and (<= 0.0 s) (<= s 256.0)) (and (< 1e-6 r) (< r 1000000.0)))
        (+ (/ (* 0.25 (exp (/ (- r) s))) (* (* (* 2.0 (PI)) s) r)) (/ (* 0.75 (exp (/ (- r) (* 3.0 s)))) (* (* (* 6.0 (PI)) s) r))))