Initial program 0.0
\[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}
\]
Simplified0.0
\[\leadsto \color{blue}{\frac{1 + \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}{2 + \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}}
\]
Proof
(/.f64 (+.f64 1 (*.f64 (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t))) (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t))))) (+.f64 2 (*.f64 (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t))) (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 1 (*.f64 (-.f64 2 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t))))) (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t))))) (+.f64 2 (*.f64 (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t))) (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t)))))): 1 points increase in error, 0 points decrease in error
(/.f64 (+.f64 1 (*.f64 (-.f64 2 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t)))) (-.f64 2 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t))))))) (+.f64 2 (*.f64 (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t))) (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 1 (*.f64 (-.f64 2 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t)))) (-.f64 2 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t)))))) (+.f64 2 (*.f64 (-.f64 2 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t))))) (-.f64 2 (/.f64 2 (*.f64 (+.f64 1 (/.f64 1 t)) t)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 1 (*.f64 (-.f64 2 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t)))) (-.f64 2 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t)))))) (+.f64 2 (*.f64 (-.f64 2 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t)))) (-.f64 2 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 2 t) (+.f64 1 (/.f64 1 t)))))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in t around 0 0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{\color{blue}{1 + t}}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}{2 + \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}
\]
Simplified0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{\color{blue}{t + 1}}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}{2 + \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}
\]
Proof
(+.f64 t 1): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 1 t)): 0 points increase in error, 0 points decrease in error
Taylor expanded in t around 0 0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{t + 1}\right) \cdot \left(2 - \frac{2}{\color{blue}{1 + t}}\right)}{2 + \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}
\]
Simplified0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{t + 1}\right) \cdot \left(2 - \frac{2}{\color{blue}{t + 1}}\right)}{2 + \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}
\]
Proof
(+.f64 t 1): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 1 t)): 0 points increase in error, 0 points decrease in error
Taylor expanded in t around 0 0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{t + 1}\right) \cdot \left(2 - \frac{2}{t + 1}\right)}{2 + \left(2 - \frac{2}{\color{blue}{1 + t}}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}
\]
Simplified0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{t + 1}\right) \cdot \left(2 - \frac{2}{t + 1}\right)}{2 + \left(2 - \frac{2}{\color{blue}{t + 1}}\right) \cdot \left(2 - \frac{2}{\left(1 + \frac{1}{t}\right) \cdot t}\right)}
\]
Proof
(+.f64 t 1): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 1 t)): 0 points increase in error, 0 points decrease in error
Taylor expanded in t around 0 0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{t + 1}\right) \cdot \left(2 - \frac{2}{t + 1}\right)}{2 + \left(2 - \frac{2}{t + 1}\right) \cdot \left(2 - \frac{2}{\color{blue}{1 + t}}\right)}
\]
Simplified0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{t + 1}\right) \cdot \left(2 - \frac{2}{t + 1}\right)}{2 + \left(2 - \frac{2}{t + 1}\right) \cdot \left(2 - \frac{2}{\color{blue}{t + 1}}\right)}
\]
Proof
(+.f64 t 1): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 1 t)): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \frac{1 + \left(2 - \frac{2}{1 + t}\right) \cdot \left(2 - \frac{2}{1 + t}\right)}{2 + \left(2 - \frac{2}{1 + t}\right) \cdot \left(2 - \frac{2}{1 + t}\right)}
\]