quadp (p42, positive)

Average Accuracy: 46.7% → 85.1%

Time: 20.6s

Precision: binary64

Cost: 20684

Math

\[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

↓

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-8711228593176025}{43556142965880123323311949751266331066368}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{2247116418577895}{22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, -2\right), \mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{5311379928167671}{1062275985633534197379176413104937254659186235454063846398888276400807119721704485478325004530458571337778658972493002030693158675305414478819039957533174703887662541670786438063456256}\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{hypot.f64}\left(b, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, -4\right)\right), \mathsf{sqrt.f64}\left(a\right)\right)\right), b\right), \frac{1}{2}\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), 99999999999999998278261272554585856747747644714015897553975120217811154108416\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(c, a\right)\right)\right)\right), b\right), \mathsf{*.f64}\left(a, 2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{/.f64}\left(b, a\right)\right)\\ \end{array} \]

FPCore

(FPCore (a b c)
 :precision binary64
 (/.f64
  (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 a c)))))
  (*.f64 2 a)))

↓

(FPCore (a b c)
 :precision binary64
 (if (<=.f64
      (neg.f64 b)
      -8711228593176025/43556142965880123323311949751266331066368)
   (/.f64 (neg.f64 c) b)
   (if (<=.f64
        (neg.f64 b)
        2247116418577895/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)
     (/.f64
      (*.f64 c -2)
      (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 a (*.f64 c -4))))))
     (if (<=.f64
          (neg.f64 b)
          5311379928167671/1062275985633534197379176413104937254659186235454063846398888276400807119721704485478325004530458571337778658972493002030693158675305414478819039957533174703887662541670786438063456256)
       (/.f64
        1
        (/.f64
         a
         (*.f64
          (-.f64 (hypot.f64 b (*.f64 (sqrt.f64 (*.f64 c -4)) (sqrt.f64 a))) b)
          1/2)))
       (if (<=.f64
            (neg.f64 b)
            99999999999999998278261272554585856747747644714015897553975120217811154108416)
         (/.f64
          (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 4 (*.f64 c a)))) b)
          (*.f64 a 2))
         (-.f64 (/.f64 c b) (/.f64 b a)))))))

Target

Original	46.7%
Target	66.9%
Herbie	85.1%

\[\begin{array}{l} \mathbf{if}\;\mathsf{<.f64}\left(b, 0\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(c, \mathsf{*.f64}\left(a, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right)\right)\right)\\ \end{array} \]

Derivation

1. Split input into 5 regimes

2. if (neg.f64 b) < -2.00000000000000008e-25

   1. Initial program 14.5%

      \[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

   2. Simplified 14.5%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right)} \]
      Proof

      [Start] 14.5	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
      /-rgt-identity [<=] 14.5	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(2, a\right), 1\right)}\right) \]
      metadata-eval [<=] 14.5	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(2, a\right), \color{blue}{\mathsf{neg.f64}\left(-1\right)}\right)\right) \]
      associate-/l* [<=] 14.5	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{neg.f64}\left(-1\right)\right), \mathsf{*.f64}\left(2, a\right)\right)} \]
      associate-*r/ [<=] 14.5	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right)} \]
      +-commutative [=>] 14.5	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), \mathsf{neg.f64}\left(b\right)\right)}, \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      unsub-neg [=>] 14.5	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), b\right)}, \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      fma-neg [=>] 14.5	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(b, b, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)}\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      *-commutative [=>] 14.5	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, c\right), 4\right)}\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      distribute-rgt-neg-in [=>] 14.5	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, c\right), \mathsf{neg.f64}\left(4\right)\right)}\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      associate-*l* [=>] 14.5	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \color{blue}{\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, \mathsf{neg.f64}\left(4\right)\right)\right)}\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      metadata-eval [=>] 14.5	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, \color{blue}{-4}\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      associate-/r* [=>] 14.5	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), 2\right), a\right)}\right) \]
      metadata-eval [=>] 14.5	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(\color{blue}{1}, 2\right), a\right)\right) \]
      metadata-eval [=>] 14.5	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\color{blue}{\frac{1}{2}}, a\right)\right) \]

   3. Taylor expanded in b around inf 88.7%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(c, b\right)\right)} \]

   4. Simplified 88.7%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right)} \]
      Proof

      [Start] 88.7	\[ \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(c, b\right)\right) \]
      associate-*r/ [=>] 88.7	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, c\right), b\right)} \]
      mul-1-neg [=>] 88.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{neg.f64}\left(c\right)}, b\right) \]

   if -2.00000000000000008e-25 < (neg.f64 b) < 1.0000000000000001e-292

   1. Initial program 63.9%

      \[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

   2. Simplified 63.8%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right)} \]
      Proof

      [Start] 63.9	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
      /-rgt-identity [<=] 63.9	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(2, a\right), 1\right)}\right) \]
      metadata-eval [<=] 63.9	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(2, a\right), \color{blue}{\mathsf{neg.f64}\left(-1\right)}\right)\right) \]
      associate-/l* [<=] 63.9	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{neg.f64}\left(-1\right)\right), \mathsf{*.f64}\left(2, a\right)\right)} \]
      associate-*r/ [<=] 63.8	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right)} \]
      +-commutative [=>] 63.8	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), \mathsf{neg.f64}\left(b\right)\right)}, \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      unsub-neg [=>] 63.8	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), b\right)}, \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      fma-neg [=>] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(b, b, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)}\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      *-commutative [=>] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, c\right), 4\right)}\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      distribute-rgt-neg-in [=>] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, c\right), \mathsf{neg.f64}\left(4\right)\right)}\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      associate-*l* [=>] 63.7	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \color{blue}{\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, \mathsf{neg.f64}\left(4\right)\right)\right)}\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      metadata-eval [=>] 63.7	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, \color{blue}{-4}\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      associate-/r* [=>] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), 2\right), a\right)}\right) \]
      metadata-eval [=>] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(\color{blue}{1}, 2\right), a\right)\right) \]
      metadata-eval [=>] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\color{blue}{\frac{1}{2}}, a\right)\right) \]

   3. Applied egg-rr 63.8%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)}\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right) \]
      Proof

      [Start] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right) \]
      fma-udef [=>] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)}\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right) \]

   4. Applied egg-rr 57.0%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, 2\right), \mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 63.8	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right) \]
      *-commutative [=>] 63.8	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, a\right), \mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)} \]
      clear-num [=>] 63.7	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \frac{1}{2}\right)\right)}, \mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right) \]
      flip-- [=>] 63.6	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \frac{1}{2}\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)}\right) \]
      frac-times [=>] 53.5	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right), \mathsf{*.f64}\left(b, b\right)\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(a, \frac{1}{2}\right), \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)\right)} \]
      *-un-lft-identity [<=] 53.5	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right), \mathsf{*.f64}\left(b, b\right)\right)}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(a, \frac{1}{2}\right), \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)\right) \]
      add-sqr-sqrt [<=] 53.6	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)}, \mathsf{*.f64}\left(b, b\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(a, \frac{1}{2}\right), \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)\right) \]
      +-commutative [=>] 53.6	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right), \mathsf{*.f64}\left(b, b\right)\right)}, \mathsf{*.f64}\left(b, b\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(a, \frac{1}{2}\right), \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)\right) \]
      associate--l+ [=>] 61.9	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right)\right)}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(a, \frac{1}{2}\right), \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)\right) \]
      fma-def [=>] 61.9	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right)\right)}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(a, \frac{1}{2}\right), \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)\right) \]
      div-inv [=>] 61.9	\[ \mathsf{/.f64}\left(\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(a, \mathsf{/.f64}\left(1, \frac{1}{2}\right)\right)}, \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)\right) \]
      metadata-eval [=>] 61.9	\[ \mathsf{/.f64}\left(\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, \color{blue}{2}\right), \mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right)\right)\right) \]
      +-commutative [=>] 61.9	\[ \mathsf{/.f64}\left(\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, 2\right), \color{blue}{\mathsf{+.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)}\right)\right) \]

   5. Simplified 67.7%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), 0\right), \mathsf{*.f64}\left(a, 2\right)\right), \mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 57.0	\[ \mathsf{/.f64}\left(\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, 2\right), \mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)\right)\right) \]
      associate-/r* [=>] 67.7	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(b, b\right)\right)\right), \mathsf{*.f64}\left(a, 2\right)\right), \mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)\right)} \]
      +-inverses [=>] 67.7	\[ \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{fma.f64}\left(a, \mathsf{*.f64}\left(c, -4\right), \color{blue}{0}\right), \mathsf{*.f64}\left(a, 2\right)\right), \mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)\right) \]

   6. Taylor expanded in a around 0 80.2%

      \[\leadsto \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-2, c\right)}, \mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)\right) \]

   if 1.0000000000000001e-292 < (neg.f64 b) < 5.00000000000000001e-168

   1. Initial program 75.0%

      \[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

   2. Simplified 74.9%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right)} \]
      Proof

      [Start] 75.0	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
      /-rgt-identity [<=] 75.0	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(2, a\right), 1\right)}\right) \]
      metadata-eval [<=] 75.0	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(2, a\right), \color{blue}{\mathsf{neg.f64}\left(-1\right)}\right)\right) \]
      associate-/l* [<=] 75.0	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{neg.f64}\left(-1\right)\right), \mathsf{*.f64}\left(2, a\right)\right)} \]
      associate-*r/ [<=] 74.9	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right)} \]
      +-commutative [=>] 74.9	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), \mathsf{neg.f64}\left(b\right)\right)}, \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      unsub-neg [=>] 74.9	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), b\right)}, \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      fma-neg [=>] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(b, b, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)}\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      *-commutative [=>] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, c\right), 4\right)}\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      distribute-rgt-neg-in [=>] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, c\right), \mathsf{neg.f64}\left(4\right)\right)}\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      associate-*l* [=>] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \color{blue}{\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, \mathsf{neg.f64}\left(4\right)\right)\right)}\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      metadata-eval [=>] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, \color{blue}{-4}\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      associate-/r* [=>] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), 2\right), a\right)}\right) \]
      metadata-eval [=>] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(\color{blue}{1}, 2\right), a\right)\right) \]
      metadata-eval [=>] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\color{blue}{\frac{1}{2}}, a\right)\right) \]

   3. Applied egg-rr 81.8%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \frac{1}{2}\right)\right)\right)} \]
      Proof

      [Start] 74.9	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right) \]
      associate-*r/ [=>] 75.1	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \frac{1}{2}\right), a\right)} \]
      clear-num [=>] 75.0	\[ \color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \frac{1}{2}\right)\right)\right)} \]
      fma-udef [=>] 75.0	\[ \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)}\right), b\right), \frac{1}{2}\right)\right)\right) \]
      add-sqr-sqrt [=>] 75.0	\[ \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)}\right)\right), b\right), \frac{1}{2}\right)\right)\right) \]
      hypot-def [=>] 81.8	\[ \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)}, b\right), \frac{1}{2}\right)\right)\right) \]

   4. Applied egg-rr 49.6%

      \[\leadsto \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{hypot.f64}\left(b, \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, -4\right)\right), \mathsf{sqrt.f64}\left(a\right)\right)}\right), b\right), \frac{1}{2}\right)\right)\right) \]
      Proof

      [Start] 81.8	\[ \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \frac{1}{2}\right)\right)\right) \]
      *-commutative [=>] 81.8	\[ \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, -4\right), a\right)}\right)\right), b\right), \frac{1}{2}\right)\right)\right) \]
      sqrt-prod [=>] 49.6	\[ \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{hypot.f64}\left(b, \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, -4\right)\right), \mathsf{sqrt.f64}\left(a\right)\right)}\right), b\right), \frac{1}{2}\right)\right)\right) \]

   if 5.00000000000000001e-168 < (neg.f64 b) < 9.99999999999999983e76

   1. Initial program 89.4%

      \[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

   if 9.99999999999999983e76 < (neg.f64 b)

   1. Initial program 35.1%

      \[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]

   2. Simplified 35.0%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right)} \]
      Proof

      [Start] 35.1	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(2, a\right)\right) \]
      /-rgt-identity [<=] 35.1	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(2, a\right), 1\right)}\right) \]
      metadata-eval [<=] 35.1	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(2, a\right), \color{blue}{\mathsf{neg.f64}\left(-1\right)}\right)\right) \]
      associate-/l* [<=] 35.1	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{neg.f64}\left(-1\right)\right), \mathsf{*.f64}\left(2, a\right)\right)} \]
      associate-*r/ [<=] 35.0	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right)} \]
      +-commutative [=>] 35.0	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), \mathsf{neg.f64}\left(b\right)\right)}, \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      unsub-neg [=>] 35.0	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), b\right)}, \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      fma-neg [=>] 35.0	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(b, b, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(4, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)}\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      *-commutative [=>] 35.0	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, c\right), 4\right)}\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      distribute-rgt-neg-in [=>] 35.0	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, c\right), \mathsf{neg.f64}\left(4\right)\right)}\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      associate-*l* [=>] 35.0	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \color{blue}{\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, \mathsf{neg.f64}\left(4\right)\right)\right)}\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      metadata-eval [=>] 35.0	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, \color{blue}{-4}\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(2, a\right)\right)\right) \]
      associate-/r* [=>] 35.0	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), 2\right), a\right)}\right) \]
      metadata-eval [=>] 35.0	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(\color{blue}{1}, 2\right), a\right)\right) \]
      metadata-eval [=>] 35.0	\[ \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right), b\right), \mathsf{/.f64}\left(\color{blue}{\frac{1}{2}}, a\right)\right) \]

   3. Taylor expanded in b around -inf 93.3%

      \[\leadsto \color{blue}{\mathsf{+.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(b, a\right)\right)\right)} \]

   4. Simplified 93.3%

      \[\leadsto \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{/.f64}\left(b, a\right)\right)} \]
      Proof

      [Start] 93.3	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(b, a\right)\right)\right) \]
      mul-1-neg [=>] 93.3	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(c, b\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{/.f64}\left(b, a\right)\right)}\right) \]
      unsub-neg [=>] 93.3	\[ \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{/.f64}\left(b, a\right)\right)} \]

3. Recombined 5 regimes into one program.

4. Final simplification 85.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-8711228593176025}{43556142965880123323311949751266331066368}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{2247116418577895}{22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, -2\right), \mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{5311379928167671}{1062275985633534197379176413104937254659186235454063846398888276400807119721704485478325004530458571337778658972493002030693158675305414478819039957533174703887662541670786438063456256}\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{hypot.f64}\left(b, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, -4\right)\right), \mathsf{sqrt.f64}\left(a\right)\right)\right), b\right), \frac{1}{2}\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), 99999999999999998278261272554585856747747644714015897553975120217811154108416\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(c, a\right)\right)\right)\right), b\right), \mathsf{*.f64}\left(a, 2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{/.f64}\left(b, a\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	76.3%
Cost	7889

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-7136238463529799}{1427247692705959881058285969449495136382746624}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{4149515568880993}{2074757784440496479256203931845580575506223116121218449997828664845326405706454073199853524473551897144098943305650394591197575537705887653943437417056981843530590901700754761842688}\right) \lor \neg \mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{578960446186581}{28948022309329048855892746252171976963317496166410141009864396001978282409984}\right) \land \mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{7378697629483821}{147573952589676412928}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, a\right), \mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -4\right)\right)\right), b\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{/.f64}\left(b, a\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	83.7%
Cost	7752

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-7136238463529799}{1427247692705959881058285969449495136382746624}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), 99999999999999998278261272554585856747747644714015897553975120217811154108416\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -4\right)\right), \mathsf{*.f64}\left(b, b\right)\right)\right), b\right), \mathsf{/.f64}\left(\frac{1}{2}, a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{/.f64}\left(b, a\right)\right)\\ \end{array} \]

Alternative 3
Accuracy	83.8%
Cost	7752

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-7136238463529799}{1427247692705959881058285969449495136382746624}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), 99999999999999998278261272554585856747747644714015897553975120217811154108416\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(4, \mathsf{*.f64}\left(c, a\right)\right)\right)\right), b\right), \mathsf{*.f64}\left(a, 2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{/.f64}\left(b, a\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	65.4%
Cost	388

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, \frac{2447171965689999}{1747979975492856518824388667826833403974715525645181428798916607807071777670465341756914322865272727992514618482604963383447074020817466839626771608982213111603568988524121832413745194182066575698549805189925857389888339453536229468710863470854144}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(b\right), a\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(c\right), b\right)\\ \end{array} \]

Alternative 5
Accuracy	29.8%
Cost	256

\[\mathsf{/.f64}\left(\mathsf{neg.f64}\left(b\right), a\right) \]

Alternative 6
Accuracy	2.6%
Cost	192

\[\mathsf{/.f64}\left(b, a\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (a b c)
  :name "quadp (p42, positive)"
  :precision binary64

  :herbie-target
  (if (< b 0.0) (/ (+ (- b) (sqrt (- (* b b) (* 4.0 (* a c))))) (* 2.0 a)) (/ c (* a (/ (- (- b) (sqrt (- (* b b) (* 4.0 (* a c))))) (* 2.0 a)))))

  (/ (+ (- b) (sqrt (- (* b b) (* 4.0 (* a c))))) (* 2.0 a)))