Original	25.5
Target	0.6
Herbie	4.9

Derivation

Split input into 2 regimes
if d < -4.3758223753918956e+105 or 1.9046995812260706e+98 < d
1. Initial program 38.6
  \[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}\]
2. Initial simplification38.6
  \[\leadsto \frac{b \cdot c - a \cdot d}{(d \cdot d + \left(c \cdot c\right))_*}\]
3. Using strategy rm
4. Applied add-sqr-sqrt38.6
  \[\leadsto \frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*} \cdot \sqrt{(d \cdot d + \left(c \cdot c\right))_*}}}\]
5. Applied *-un-lft-identity38.6
  \[\leadsto \frac{\color{blue}{1 \cdot \left(b \cdot c - a \cdot d\right)}}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*} \cdot \sqrt{(d \cdot d + \left(c \cdot c\right))_*}}\]
6. Applied times-frac38.6
  \[\leadsto \color{blue}{\frac{1}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*}} \cdot \frac{b \cdot c - a \cdot d}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*}}}\]
7. Simplified38.6
  \[\leadsto \color{blue}{\frac{1}{\sqrt{d^2 + c^2}^*}} \cdot \frac{b \cdot c - a \cdot d}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*}}\]
8. Simplified25.3
  \[\leadsto \frac{1}{\sqrt{d^2 + c^2}^*} \cdot \color{blue}{\frac{b \cdot c - a \cdot d}{\sqrt{d^2 + c^2}^*}}\]
9. Using strategy rm
10. Applied associate-*l/25.3
  \[\leadsto \color{blue}{\frac{1 \cdot \frac{b \cdot c - a \cdot d}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*}}\]
11. Simplified25.3
  \[\leadsto \frac{\color{blue}{\frac{c \cdot b - a \cdot d}{\sqrt{d^2 + c^2}^*}}}{\sqrt{d^2 + c^2}^*}\]
12. Using strategy rm
13. Applied div-sub25.3
  \[\leadsto \frac{\color{blue}{\frac{c \cdot b}{\sqrt{d^2 + c^2}^*} - \frac{a \cdot d}{\sqrt{d^2 + c^2}^*}}}{\sqrt{d^2 + c^2}^*}\]
14. Applied div-sub25.3
  \[\leadsto \color{blue}{\frac{\frac{c \cdot b}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*} - \frac{\frac{a \cdot d}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*}}\]
15. Using strategy rm
16. Applied *-un-lft-identity25.3
  \[\leadsto \frac{\frac{c \cdot b}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*} - \frac{\frac{a \cdot d}{\color{blue}{1 \cdot \sqrt{d^2 + c^2}^*}}}{\sqrt{d^2 + c^2}^*}\]
17. Applied times-frac7.8
  \[\leadsto \frac{\frac{c \cdot b}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*} - \frac{\color{blue}{\frac{a}{1} \cdot \frac{d}{\sqrt{d^2 + c^2}^*}}}{\sqrt{d^2 + c^2}^*}\]
18. Simplified7.8
  \[\leadsto \frac{\frac{c \cdot b}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*} - \frac{\color{blue}{a} \cdot \frac{d}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*}\]
if -4.3758223753918956e+105 < d < 1.9046995812260706e+98
1. Initial program 18.0
  \[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}\]
2. Initial simplification18.0
  \[\leadsto \frac{b \cdot c - a \cdot d}{(d \cdot d + \left(c \cdot c\right))_*}\]
3. Using strategy rm
4. Applied add-sqr-sqrt18.0
  \[\leadsto \frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*} \cdot \sqrt{(d \cdot d + \left(c \cdot c\right))_*}}}\]
5. Applied *-un-lft-identity18.0
  \[\leadsto \frac{\color{blue}{1 \cdot \left(b \cdot c - a \cdot d\right)}}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*} \cdot \sqrt{(d \cdot d + \left(c \cdot c\right))_*}}\]
6. Applied times-frac18.1
  \[\leadsto \color{blue}{\frac{1}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*}} \cdot \frac{b \cdot c - a \cdot d}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*}}}\]
7. Simplified18.1
  \[\leadsto \color{blue}{\frac{1}{\sqrt{d^2 + c^2}^*}} \cdot \frac{b \cdot c - a \cdot d}{\sqrt{(d \cdot d + \left(c \cdot c\right))_*}}\]
8. Simplified11.2
  \[\leadsto \frac{1}{\sqrt{d^2 + c^2}^*} \cdot \color{blue}{\frac{b \cdot c - a \cdot d}{\sqrt{d^2 + c^2}^*}}\]
9. Using strategy rm
10. Applied associate-*l/11.1
  \[\leadsto \color{blue}{\frac{1 \cdot \frac{b \cdot c - a \cdot d}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*}}\]
11. Simplified11.1
  \[\leadsto \frac{\color{blue}{\frac{c \cdot b - a \cdot d}{\sqrt{d^2 + c^2}^*}}}{\sqrt{d^2 + c^2}^*}\]
12. Using strategy rm
13. Applied div-sub11.1
  \[\leadsto \frac{\color{blue}{\frac{c \cdot b}{\sqrt{d^2 + c^2}^*} - \frac{a \cdot d}{\sqrt{d^2 + c^2}^*}}}{\sqrt{d^2 + c^2}^*}\]
14. Applied div-sub11.1
  \[\leadsto \color{blue}{\frac{\frac{c \cdot b}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*} - \frac{\frac{a \cdot d}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*}}\]
15. Using strategy rm
16. Applied associate-/l*3.2
  \[\leadsto \frac{\color{blue}{\frac{c}{\frac{\sqrt{d^2 + c^2}^*}{b}}}}{\sqrt{d^2 + c^2}^*} - \frac{\frac{a \cdot d}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*}\]
Recombined 2 regimes into one program.
Final simplification4.9
\[\leadsto \begin{array}{l} \mathbf{if}\;d \le -4.3758223753918956 \cdot 10^{+105} \lor \neg \left(d \le 1.9046995812260706 \cdot 10^{+98}\right):\\ \;\;\;\;\frac{\frac{c \cdot b}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*} - \frac{a \cdot \frac{d}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{c}{\frac{\sqrt{d^2 + c^2}^*}{b}}}{\sqrt{d^2 + c^2}^*} - \frac{\frac{a \cdot d}{\sqrt{d^2 + c^2}^*}}{\sqrt{d^2 + c^2}^*}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if d < -4.3758223753918956e+105 or 1.9046995812260706e+98 < d`

`if -4.3758223753918956e+105 < d < 1.9046995812260706e+98`

Runtime

In
Out