Simplified0.4
\[\leadsto \color{blue}{\left(n0_i \cdot \left(u \cdot \left(0.5 + u \cdot -0.5\right)\right) + \left(n1_i - n0_i\right) \cdot \left(-0.16666666666666666 \cdot \left({u}^{3} - u\right)\right)\right)} \cdot {normAngle}^{2} + \left(n1_i \cdot u + \left(1 - u\right) \cdot n0_i\right)
\]
Proof
(+.f32 (*.f32 n0_i (*.f32 u (+.f32 1/2 (*.f32 u -1/2)))) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 n0_i (*.f32 u (+.f32 1/2 (Rewrite<= *-commutative_binary32 (*.f32 -1/2 u))))) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 n0_i (Rewrite<= distribute-rgt-out_binary32 (+.f32 (*.f32 1/2 u) (*.f32 (*.f32 -1/2 u) u)))) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 8 points increase in error, 16 points decrease in error
(+.f32 (*.f32 n0_i (+.f32 (*.f32 1/2 u) (Rewrite<= associate-*r*_binary32 (*.f32 -1/2 (*.f32 u u))))) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 n0_i (+.f32 (*.f32 1/2 u) (*.f32 -1/2 (Rewrite<= unpow2_binary32 (pow.f32 u 2))))) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 n0_i (Rewrite=> +-commutative_binary32 (+.f32 (*.f32 -1/2 (pow.f32 u 2)) (*.f32 1/2 u)))) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (Rewrite<= distribute-rgt-out_binary32 (+.f32 (*.f32 (*.f32 -1/2 (pow.f32 u 2)) n0_i) (*.f32 (*.f32 1/2 u) n0_i))) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 15 points increase in error, 16 points decrease in error
(+.f32 (+.f32 (Rewrite<= associate-*r*_binary32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i))) (*.f32 (*.f32 1/2 u) n0_i)) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (Rewrite<= associate-*r*_binary32 (*.f32 1/2 (*.f32 u n0_i)))) (*.f32 (-.f32 n1_i n0_i) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 1 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (Rewrite<= unsub-neg_binary32 (+.f32 n1_i (neg.f32 n0_i))) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 n1_i (Rewrite<= mul-1-neg_binary32 (*.f32 -1 n0_i))) (*.f32 -1/6 (-.f32 (pow.f32 u 3) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (Rewrite<= distribute-lft-out--_binary32 (-.f32 (*.f32 -1/6 (pow.f32 u 3)) (*.f32 -1/6 u))))): 11 points increase in error, 11 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (Rewrite=> cancel-sign-sub-inv_binary32 (+.f32 (*.f32 -1/6 (pow.f32 u 3)) (*.f32 (neg.f32 -1/6) u))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (+.f32 (*.f32 -1/6 (pow.f32 u 3)) (*.f32 (Rewrite=> metadata-eval 1/6) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (Rewrite=> +-commutative_binary32 (+.f32 (*.f32 1/6 u) (*.f32 -1/6 (pow.f32 u 3)))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (Rewrite<= distribute-lft-out_binary32 (+.f32 (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 1/6 u)) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3)))))): 17 points increase in error, 14 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) 1/6) u)) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 33 points increase in error, 30 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (Rewrite<= metadata-eval (neg.f32 -1/6))) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (Rewrite<= distribute-rgt-neg-in_binary32 (neg.f32 (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) -1/6))) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (Rewrite=> distribute-lft-neg-in_binary32 (*.f32 (neg.f32 (+.f32 n1_i (*.f32 -1 n0_i))) -1/6)) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (Rewrite=> associate-*l*_binary32 (*.f32 (neg.f32 (+.f32 n1_i (*.f32 -1 n0_i))) (*.f32 -1/6 u))) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 30 points increase in error, 33 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (Rewrite=> distribute-neg-in_binary32 (+.f32 (neg.f32 n1_i) (neg.f32 (*.f32 -1 n0_i)))) (*.f32 -1/6 u)) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (Rewrite<= mul-1-neg_binary32 (*.f32 -1 n1_i)) (neg.f32 (*.f32 -1 n0_i))) (*.f32 -1/6 u)) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1 n1_i) (neg.f32 (Rewrite=> mul-1-neg_binary32 (neg.f32 n0_i)))) (*.f32 -1/6 u)) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1 n1_i) (Rewrite=> remove-double-neg_binary32 n0_i)) (*.f32 -1/6 u)) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 (+.f32 (*.f32 -1 n1_i) n0_i) -1/6) u)) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 33 points increase in error, 30 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (Rewrite<= *-commutative_binary32 (*.f32 -1/6 (+.f32 (*.f32 -1 n1_i) n0_i))) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (*.f32 -1/6 (Rewrite=> +-commutative_binary32 (+.f32 n0_i (*.f32 -1 n1_i)))) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (Rewrite=> distribute-rgt-in_binary32 (+.f32 (*.f32 n0_i -1/6) (*.f32 (*.f32 -1 n1_i) -1/6))) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 18 points increase in error, 14 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (Rewrite<= *-commutative_binary32 (*.f32 -1/6 n0_i)) (*.f32 (*.f32 -1 n1_i) -1/6)) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (Rewrite<= *-commutative_binary32 (*.f32 -1/6 (*.f32 -1 n1_i)))) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (Rewrite=> associate-*r*_binary32 (*.f32 (*.f32 -1/6 -1) n1_i))) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 (Rewrite=> metadata-eval 1/6) n1_i)) u) (*.f32 (+.f32 n1_i (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (*.f32 (+.f32 (Rewrite<= remove-double-neg_binary32 (neg.f32 (neg.f32 n1_i))) (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (*.f32 (+.f32 (neg.f32 (Rewrite<= mul-1-neg_binary32 (*.f32 -1 n1_i))) (*.f32 -1 n0_i)) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (*.f32 (+.f32 (neg.f32 (*.f32 -1 n1_i)) (Rewrite=> mul-1-neg_binary32 (neg.f32 n0_i))) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (*.f32 (Rewrite<= distribute-neg-in_binary32 (neg.f32 (+.f32 (*.f32 -1 n1_i) n0_i))) (*.f32 -1/6 (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (Rewrite=> distribute-lft-neg-out_binary32 (neg.f32 (*.f32 (+.f32 (*.f32 -1 n1_i) n0_i) (*.f32 -1/6 (pow.f32 u 3))))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (neg.f32 (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 (+.f32 (*.f32 -1 n1_i) n0_i) -1/6) (pow.f32 u 3)))))): 1 points increase in error, 1 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (neg.f32 (*.f32 (Rewrite<= *-commutative_binary32 (*.f32 -1/6 (+.f32 (*.f32 -1 n1_i) n0_i))) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (neg.f32 (*.f32 (*.f32 -1/6 (Rewrite=> +-commutative_binary32 (+.f32 n0_i (*.f32 -1 n1_i)))) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (neg.f32 (*.f32 (Rewrite=> distribute-rgt-in_binary32 (+.f32 (*.f32 n0_i -1/6) (*.f32 (*.f32 -1 n1_i) -1/6))) (pow.f32 u 3))))): 1 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (neg.f32 (*.f32 (+.f32 (Rewrite<= *-commutative_binary32 (*.f32 -1/6 n0_i)) (*.f32 (*.f32 -1 n1_i) -1/6)) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (neg.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (Rewrite<= *-commutative_binary32 (*.f32 -1/6 (*.f32 -1 n1_i)))) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (neg.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (Rewrite=> associate-*r*_binary32 (*.f32 (*.f32 -1/6 -1) n1_i))) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (+.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (neg.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 (Rewrite=> metadata-eval 1/6) n1_i)) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (Rewrite=> unsub-neg_binary32 (-.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary32 (-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) u)) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3)))): 6 points increase in error, 10 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 (Rewrite=> *-commutative_binary32 (*.f32 n0_i -1/6)) (*.f32 1/6 n1_i)) u)) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 (*.f32 n0_i -1/6) (*.f32 (Rewrite<= metadata-eval (*.f32 -1/6 -1)) n1_i)) u)) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 (*.f32 n0_i -1/6) (Rewrite<= associate-*r*_binary32 (*.f32 -1/6 (*.f32 -1 n1_i)))) u)) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (+.f32 (*.f32 n0_i -1/6) (Rewrite=> *-commutative_binary32 (*.f32 (*.f32 -1 n1_i) -1/6))) u)) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (Rewrite<= distribute-rgt-in_binary32 (*.f32 -1/6 (+.f32 n0_i (*.f32 -1 n1_i)))) u)) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 14 points increase in error, 17 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (*.f32 -1/6 (Rewrite<= +-commutative_binary32 (+.f32 (*.f32 -1 n1_i) n0_i))) u)) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (Rewrite=> associate-*l*_binary32 (*.f32 -1/6 (*.f32 (+.f32 (*.f32 -1 n1_i) n0_i) u)))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 39 points increase in error, 34 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 -1/6 (*.f32 (+.f32 (*.f32 -1 n1_i) (Rewrite<= remove-double-neg_binary32 (neg.f32 (neg.f32 n0_i)))) u))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 -1/6 (*.f32 (+.f32 (*.f32 -1 n1_i) (neg.f32 (Rewrite<= mul-1-neg_binary32 (*.f32 -1 n0_i)))) u))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 -1/6 (*.f32 (+.f32 (Rewrite=> mul-1-neg_binary32 (neg.f32 n1_i)) (neg.f32 (*.f32 -1 n0_i))) u))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 -1/6 (*.f32 (Rewrite<= distribute-neg-in_binary32 (neg.f32 (+.f32 n1_i (*.f32 -1 n0_i)))) u))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (Rewrite<= associate-*l*_binary32 (*.f32 (*.f32 -1/6 (neg.f32 (+.f32 n1_i (*.f32 -1 n0_i)))) u))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 34 points increase in error, 39 points decrease in error
(-.f32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 1/2 (*.f32 u n0_i))) (*.f32 (Rewrite<= distribute-rgt-neg-in_binary32 (neg.f32 (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i))))) u)) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (Rewrite<= associate-+r+_binary32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (+.f32 (*.f32 1/2 (*.f32 u n0_i)) (*.f32 (neg.f32 (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u)))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 26 points increase in error, 27 points decrease in error
(-.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (+.f32 (*.f32 1/2 (Rewrite=> *-commutative_binary32 (*.f32 n0_i u))) (*.f32 (neg.f32 (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (+.f32 (Rewrite=> associate-*r*_binary32 (*.f32 (*.f32 1/2 n0_i) u)) (*.f32 (neg.f32 (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 1 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (Rewrite<= distribute-rgt-in_binary32 (*.f32 u (+.f32 (*.f32 1/2 n0_i) (neg.f32 (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))))))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 48 points increase in error, 31 points decrease in error
(-.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 u (Rewrite<= sub-neg_binary32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i))))))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(-.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (Rewrite<= *-commutative_binary32 (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))) (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary32 (+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u)) (neg.f32 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(+.f32 (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u)) (Rewrite<= mul-1-neg_binary32 (*.f32 -1 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary32 (+.f32 (*.f32 -1 (*.f32 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i)) (pow.f32 u 3))) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u)))): 0 points increase in error, 0 points decrease in error
(+.f32 (Rewrite=> associate-*r*_binary32 (*.f32 (*.f32 -1 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i))) (pow.f32 u 3))) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 0 points increase in error, 0 points decrease in error
(+.f32 (*.f32 (*.f32 -1 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i))) (Rewrite=> sqr-pow_binary32 (*.f32 (pow.f32 u (/.f32 3 2)) (pow.f32 u (/.f32 3 2))))) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 1 points increase in error, 2 points decrease in error
(+.f32 (Rewrite=> associate-*r*_binary32 (*.f32 (*.f32 (*.f32 -1 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i))) (pow.f32 u (/.f32 3 2))) (pow.f32 u (/.f32 3 2)))) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 2 points increase in error, 3 points decrease in error
(Rewrite<= fma-udef_binary32 (fma.f32 (*.f32 (*.f32 -1 (+.f32 (*.f32 -1/6 n0_i) (*.f32 1/6 n1_i))) (pow.f32 u (/.f32 3 2))) (pow.f32 u (/.f32 3 2)) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u)))): 3 points increase in error, 3 points decrease in error
(fma.f32 (*.f32 (Rewrite=> distribute-lft-in_binary32 (+.f32 (*.f32 -1 (*.f32 -1/6 n0_i)) (*.f32 -1 (*.f32 1/6 n1_i)))) (pow.f32 u (/.f32 3 2))) (pow.f32 u (/.f32 3 2)) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 0 points increase in error, 0 points decrease in error
(fma.f32 (*.f32 (+.f32 (Rewrite=> associate-*r*_binary32 (*.f32 (*.f32 -1 -1/6) n0_i)) (*.f32 -1 (*.f32 1/6 n1_i))) (pow.f32 u (/.f32 3 2))) (pow.f32 u (/.f32 3 2)) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 0 points increase in error, 0 points decrease in error
(fma.f32 (*.f32 (+.f32 (*.f32 (Rewrite=> metadata-eval 1/6) n0_i) (*.f32 -1 (*.f32 1/6 n1_i))) (pow.f32 u (/.f32 3 2))) (pow.f32 u (/.f32 3 2)) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 0 points increase in error, 0 points decrease in error
(fma.f32 (*.f32 (+.f32 (*.f32 1/6 n0_i) (Rewrite=> associate-*r*_binary32 (*.f32 (*.f32 -1 1/6) n1_i))) (pow.f32 u (/.f32 3 2))) (pow.f32 u (/.f32 3 2)) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 0 points increase in error, 0 points decrease in error
(fma.f32 (*.f32 (+.f32 (*.f32 1/6 n0_i) (*.f32 (Rewrite=> metadata-eval -1/6) n1_i)) (pow.f32 u (/.f32 3 2))) (pow.f32 u (/.f32 3 2)) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary32 (+.f32 (*.f32 (*.f32 (+.f32 (*.f32 1/6 n0_i) (*.f32 -1/6 n1_i)) (pow.f32 u (/.f32 3 2))) (pow.f32 u (/.f32 3 2))) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u)))): 3 points increase in error, 3 points decrease in error
(+.f32 (Rewrite<= associate-*r*_binary32 (*.f32 (+.f32 (*.f32 1/6 n0_i) (*.f32 -1/6 n1_i)) (*.f32 (pow.f32 u (/.f32 3 2)) (pow.f32 u (/.f32 3 2))))) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 3 points increase in error, 2 points decrease in error
(+.f32 (*.f32 (+.f32 (*.f32 1/6 n0_i) (*.f32 -1/6 n1_i)) (Rewrite<= sqr-pow_binary32 (pow.f32 u 3))) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 2 points increase in error, 1 points decrease in error
(+.f32 (Rewrite<= *-commutative_binary32 (*.f32 (pow.f32 u 3) (+.f32 (*.f32 1/6 n0_i) (*.f32 -1/6 n1_i)))) (+.f32 (*.f32 -1/2 (*.f32 (pow.f32 u 2) n0_i)) (*.f32 (-.f32 (*.f32 1/2 n0_i) (*.f32 -1/6 (+.f32 n1_i (*.f32 -1 n0_i)))) u))): 0 points increase in error, 0 points decrease in error