Average Error: 0.0 → 0.0
Time: 7.2s
Precision: binary64
\[1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
↓
\[\begin{array}{l} t_1 := 1 + \frac{1}{t}\\ t_2 := 2 - \frac{\frac{2}{t}}{t_1}\\ 1 - \frac{1}{2 + \left(2 \cdot t_2 - t_2 \cdot \left(\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{t_1}\right)\right)} \end{array} \]
1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}
↓
\begin{array}{l}
t_1 := 1 + \frac{1}{t}\\
t_2 := 2 - \frac{\frac{2}{t}}{t_1}\\
1 - \frac{1}{2 + \left(2 \cdot t_2 - t_2 \cdot \left(\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{t_1}\right)\right)}
\end{array}

(FPCore (t)
 :precision binary64
 (-
  1.0
  (/
   1.0
   (+
    2.0
    (*
     (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))))
     (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))))))))
↓
(FPCore (t)
 :precision binary64
 (let* ((t_1 (+ 1.0 (/ 1.0 t))) (t_2 (- 2.0 (/ (/ 2.0 t) t_1))))
   (-
    1.0
    (/
     1.0
     (+
      2.0
      (-
       (* 2.0 t_2)
       (*
        t_2
        (*
         (/ (* (cbrt 2.0) (cbrt 2.0)) (* (cbrt t) (cbrt t)))
         (/ (/ (cbrt 2.0) (cbrt t)) t_1)))))))))
double code(double t) {
	return 1.0 - (1.0 / (2.0 + ((2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))) * (2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))))));
}
↓
double code(double t) {
	double t_1 = 1.0 + (1.0 / t);
	double t_2 = 2.0 - ((2.0 / t) / t_1);
	return 1.0 - (1.0 / (2.0 + ((2.0 * t_2) - (t_2 * (((cbrt(2.0) * cbrt(2.0)) / (cbrt(t) * cbrt(t))) * ((cbrt(2.0) / cbrt(t)) / t_1))))));
}

Error

Bits error versus t

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 0.0

    \[1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
  2. Using strategy rm

  3. Applied *-un-lft-identity_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{\color{blue}{1 \cdot \left(1 + \frac{1}{t}\right)}}\right)} \]

  4. Applied add-cube-cbrt_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{\color{blue}{\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \sqrt[3]{t}}}}{1 \cdot \left(1 + \frac{1}{t}\right)}\right)} \]

  5. Applied add-cube-cbrt_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{\color{blue}{\left(\sqrt[3]{2} \cdot \sqrt[3]{2}\right) \cdot \sqrt[3]{2}}}{\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \sqrt[3]{t}}}{1 \cdot \left(1 + \frac{1}{t}\right)}\right)} \]

  6. Applied times-frac_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\color{blue}{\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\sqrt[3]{2}}{\sqrt[3]{t}}}}{1 \cdot \left(1 + \frac{1}{t}\right)}\right)} \]

  7. Applied times-frac_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \color{blue}{\frac{\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}{1} \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{1 + \frac{1}{t}}}\right)} \]

  8. Applied cancel-sign-sub-inv_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \color{blue}{\left(2 + \left(-\frac{\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}{1}\right) \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{1 + \frac{1}{t}}\right)}} \]

  9. Applied distribute-rgt-in_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(2 \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + \left(\left(-\frac{\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}}}{1}\right) \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right)}} \]

  10. Simplified0.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + \color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(\left(-\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}}\right) \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{1 + \frac{1}{t}}\right)}\right)} \]
  11. Using strategy rm

  12. Applied distribute-lft-neg-out_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \color{blue}{\left(-\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{1 + \frac{1}{t}}\right)}\right)} \]

  13. Applied distribute-rgt-neg-out_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + \color{blue}{\left(-\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{1 + \frac{1}{t}}\right)\right)}\right)} \]

  14. Applied unsub-neg_binary640.0

    \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(2 \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{1 + \frac{1}{t}}\right)\right)}} \]

  15. Final simplification0.0

    \[\leadsto 1 - \frac{1}{2 + \left(2 \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(\frac{\sqrt[3]{2} \cdot \sqrt[3]{2}}{\sqrt[3]{t} \cdot \sqrt[3]{t}} \cdot \frac{\frac{\sqrt[3]{2}}{\sqrt[3]{t}}}{1 + \frac{1}{t}}\right)\right)} \]

Reproduce

herbie shell --seed 2021205 
(FPCore (t)
  :name "Kahan p13 Example 3"
  :precision binary64
  (- 1.0 (/ 1.0 (+ 2.0 (* (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))) (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))))))))