Original	26.5
Target	0.4
Herbie	13.6

Derivation

Split input into 3 regimes
if c < -1.586349612154054e+218
1. Initial program 43.7
  \[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}\]
2. Using strategy rm
3. Applied add-sqr-sqrt43.7
  \[\leadsto \frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{c \cdot c + d \cdot d} \cdot \sqrt{c \cdot c + d \cdot d}}}\]
4. Applied associate-/r*43.7
  \[\leadsto \color{blue}{\frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot c + d \cdot d}}}\]
5. Using strategy rm
6. Applied *-commutative43.7
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot c + \color{blue}{d \cdot d}}}\]
7. Applied add-sqr-sqrt62.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot \color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}\]
8. Applied add-sqr-sqrt62.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} \cdot \left(\sqrt{c} \cdot \sqrt{c}\right) + d \cdot d}}\]
9. Applied unswap-sqr62.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right) \cdot \left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}\]
10. Applied hypot-def62.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\color{blue}{\sqrt{\left(\sqrt{c} \cdot \sqrt{c}\right)^2 + d^2}^*}}\]
11. Simplified43.7
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{c}^2 + d^2}^*}\]
12. Taylor expanded around -inf 11.1
  \[\leadsto \frac{\color{blue}{-1 \cdot b}}{\sqrt{c^2 + d^2}^*}\]
13. Simplified11.1
  \[\leadsto \frac{\color{blue}{-b}}{\sqrt{c^2 + d^2}^*}\]
if -1.586349612154054e+218 < c < 6.788602011952196e+137
1. Initial program 21.4
  \[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}\]
2. Using strategy rm
3. Applied add-sqr-sqrt21.4
  \[\leadsto \frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{c \cdot c + d \cdot d} \cdot \sqrt{c \cdot c + d \cdot d}}}\]
4. Applied associate-/r*21.3
  \[\leadsto \color{blue}{\frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot c + d \cdot d}}}\]
5. Using strategy rm
6. Applied *-commutative21.3
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot c + \color{blue}{d \cdot d}}}\]
7. Applied add-sqr-sqrt42.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot \color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}\]
8. Applied add-sqr-sqrt42.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} \cdot \left(\sqrt{c} \cdot \sqrt{c}\right) + d \cdot d}}\]
9. Applied unswap-sqr42.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right) \cdot \left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}\]
10. Applied hypot-def42.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\color{blue}{\sqrt{\left(\sqrt{c} \cdot \sqrt{c}\right)^2 + d^2}^*}}\]
11. Simplified21.3
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{c}^2 + d^2}^*}\]
12. Using strategy rm
13. Applied *-commutative21.3
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + \color{blue}{d \cdot d}}}}{\sqrt{c^2 + d^2}^*}\]
14. Applied add-sqr-sqrt42.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot \color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}}{\sqrt{c^2 + d^2}^*}\]
15. Applied add-sqr-sqrt42.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} \cdot \left(\sqrt{c} \cdot \sqrt{c}\right) + d \cdot d}}}{\sqrt{c^2 + d^2}^*}\]
16. Applied swap-sqr42.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right) \cdot \left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}}{\sqrt{c^2 + d^2}^*}\]
17. Applied hypot-def39.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{\left(\sqrt{c} \cdot \sqrt{c}\right)^2 + d^2}^*}}}{\sqrt{c^2 + d^2}^*}\]
18. Simplified13.3
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{\color{blue}{c}^2 + d^2}^*}}{\sqrt{c^2 + d^2}^*}\]
19. Using strategy rm
20. Applied div-inv13.4
  \[\leadsto \frac{\color{blue}{\left(b \cdot c - a \cdot d\right) \cdot \frac{1}{\sqrt{c^2 + d^2}^*}}}{\sqrt{c^2 + d^2}^*}\]
if 6.788602011952196e+137 < c
1. Initial program 44.0
  \[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}\]
2. Using strategy rm
3. Applied add-sqr-sqrt44.0
  \[\leadsto \frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{c \cdot c + d \cdot d} \cdot \sqrt{c \cdot c + d \cdot d}}}\]
4. Applied associate-/r*44.0
  \[\leadsto \color{blue}{\frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot c + d \cdot d}}}\]
5. Using strategy rm
6. Applied *-commutative44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot c + \color{blue}{d \cdot d}}}\]
7. Applied add-sqr-sqrt44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{c \cdot \color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}\]
8. Applied add-sqr-sqrt44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} \cdot \left(\sqrt{c} \cdot \sqrt{c}\right) + d \cdot d}}\]
9. Applied unswap-sqr44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right) \cdot \left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}\]
10. Applied hypot-def44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\color{blue}{\sqrt{\left(\sqrt{c} \cdot \sqrt{c}\right)^2 + d^2}^*}}\]
11. Simplified44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + d \cdot d}}}{\sqrt{\color{blue}{c}^2 + d^2}^*}\]
12. Using strategy rm
13. Applied *-commutative44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot c + \color{blue}{d \cdot d}}}}{\sqrt{c^2 + d^2}^*}\]
14. Applied add-sqr-sqrt44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{c \cdot \color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}}{\sqrt{c^2 + d^2}^*}\]
15. Applied add-sqr-sqrt44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right)} \cdot \left(\sqrt{c} \cdot \sqrt{c}\right) + d \cdot d}}}{\sqrt{c^2 + d^2}^*}\]
16. Applied swap-sqr44.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{\color{blue}{\left(\sqrt{c} \cdot \sqrt{c}\right) \cdot \left(\sqrt{c} \cdot \sqrt{c}\right)} + d \cdot d}}}{\sqrt{c^2 + d^2}^*}\]
17. Applied hypot-def28.0
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\color{blue}{\sqrt{\left(\sqrt{c} \cdot \sqrt{c}\right)^2 + d^2}^*}}}{\sqrt{c^2 + d^2}^*}\]
18. Simplified27.9
  \[\leadsto \frac{\frac{b \cdot c - a \cdot d}{\sqrt{\color{blue}{c}^2 + d^2}^*}}{\sqrt{c^2 + d^2}^*}\]
19. Taylor expanded around inf 16.1
  \[\leadsto \frac{\color{blue}{b}}{\sqrt{c^2 + d^2}^*}\]
Recombined 3 regimes into one program.
Final simplification13.6
\[\leadsto \begin{array}{l} \mathbf{if}\;c \le -1.586349612154054 \cdot 10^{+218}:\\ \;\;\;\;\frac{-b}{\sqrt{c^2 + d^2}^*}\\ \mathbf{elif}\;c \le 6.788602011952196 \cdot 10^{+137}:\\ \;\;\;\;\frac{\left(b \cdot c - d \cdot a\right) \cdot \frac{1}{\sqrt{c^2 + d^2}^*}}{\sqrt{c^2 + d^2}^*}\\ \mathbf{else}:\\ \;\;\;\;\frac{b}{\sqrt{c^2 + d^2}^*}\\ \end{array}\]

Error

Target

Derivation

`if c < -1.586349612154054e+218`

`if -1.586349612154054e+218 < c < 6.788602011952196e+137`

`if 6.788602011952196e+137 < c`

Reproduce