1. Initial program 3.4%

   \[\left(1 + t \cdot 2 \cdot 10^{-16}\right) \cdot \left(1 + t \cdot 2 \cdot 10^{-16}\right) + \left(-1 - 2 \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) \]
2. Step-by-step derivation

   1. associate-+r-9.9%

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

   2. sub-neg9.9%

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

   3. +-commutative9.9%

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

   4. difference-of-sqr--19.9%

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

   5. +-commutative9.9%

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

   6. associate--l+3.4%

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

   7. metadata-eval3.4%

      \[\leadsto \left(-2 \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) + \left(\left(1 + t \cdot 2 \cdot 10^{-16}\right) + 1\right) \cdot \left(t \cdot 2 \cdot 10^{-16} + \color{blue}{0}\right) \]

   8. +-rgt-identity3.4%

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

   9. distribute-lft1-in20.9%

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

   10. *-commutative20.9%

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

   11. associate-+r+20.9%

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

   12. +-commutative20.9%

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

   13. +-commutative20.9%

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

   14. *-rgt-identity20.9%

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

3. Simplified99.3%

   \[\leadsto \color{blue}{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)} \]

4. Taylor expanded in t around 0 99.3%

   \[\leadsto \color{blue}{4 \cdot 10^{-32} \cdot {t}^{2}} \]
5. Step-by-step derivation

   1. *-commutative99.3%

      \[\leadsto \color{blue}{{t}^{2} \cdot 4 \cdot 10^{-32}} \]

   2. unpow299.3%

      \[\leadsto \color{blue}{\left(t \cdot t\right)} \cdot 4 \cdot 10^{-32} \]

   3. metadata-eval99.1%

      \[\leadsto \left(t \cdot t\right) \cdot \color{blue}{\left(2 \cdot 10^{-16} \cdot 2 \cdot 10^{-16}\right)} \]

   4. swap-sqr99.3%

      \[\leadsto \color{blue}{\left(t \cdot 2 \cdot 10^{-16}\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right)} \]

   5. unpow299.3%

      \[\leadsto \color{blue}{{\left(t \cdot 2 \cdot 10^{-16}\right)}^{2}} \]

6. Simplified99.3%

   \[\leadsto \color{blue}{{\left(t \cdot 2 \cdot 10^{-16}\right)}^{2}} \]
7. Step-by-step derivation

   1. unpow299.3%

      \[\leadsto \color{blue}{\left(t \cdot 2 \cdot 10^{-16}\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right)} \]

   2. add-sqr-sqrt98.9%

      \[\leadsto \left(\color{blue}{\left(\sqrt{t} \cdot \sqrt{t}\right)} \cdot 2 \cdot 10^{-16}\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   3. associate-*l*99.1%

      \[\leadsto \color{blue}{\left(\sqrt{t} \cdot \left(\sqrt{t} \cdot 2 \cdot 10^{-16}\right)\right)} \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   4. metadata-eval99.1%

      \[\leadsto \left(\sqrt{t} \cdot \left(\sqrt{t} \cdot \color{blue}{\sqrt{4 \cdot 10^{-32}}}\right)\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   5. sqrt-prod99.4%

      \[\leadsto \left(\sqrt{t} \cdot \color{blue}{\sqrt{t \cdot 4 \cdot 10^{-32}}}\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   6. sqrt-prod99.4%

      \[\leadsto \color{blue}{\sqrt{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)}} \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   7. *-commutative99.4%

      \[\leadsto \sqrt{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)} \cdot \color{blue}{\left(2 \cdot 10^{-16} \cdot t\right)} \]

   8. associate-*r*99.2%

      \[\leadsto \color{blue}{\left(\sqrt{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)} \cdot 2 \cdot 10^{-16}\right) \cdot t} \]

   9. associate-*r*99.4%

      \[\leadsto \left(\sqrt{\color{blue}{\left(t \cdot t\right) \cdot 4 \cdot 10^{-32}}} \cdot 2 \cdot 10^{-16}\right) \cdot t \]

   10. sqrt-prod99.5%

       \[\leadsto \left(\color{blue}{\left(\sqrt{t \cdot t} \cdot \sqrt{4 \cdot 10^{-32}}\right)} \cdot 2 \cdot 10^{-16}\right) \cdot t \]

   11. sqrt-prod99.0%

       \[\leadsto \left(\left(\color{blue}{\left(\sqrt{t} \cdot \sqrt{t}\right)} \cdot \sqrt{4 \cdot 10^{-32}}\right) \cdot 2 \cdot 10^{-16}\right) \cdot t \]

   12. add-sqr-sqrt99.5%

       \[\leadsto \left(\left(\color{blue}{t} \cdot \sqrt{4 \cdot 10^{-32}}\right) \cdot 2 \cdot 10^{-16}\right) \cdot t \]

   13. metadata-eval99.5%

       \[\leadsto \left(\left(t \cdot \color{blue}{2 \cdot 10^{-16}}\right) \cdot 2 \cdot 10^{-16}\right) \cdot t \]

8. Applied egg-rr99.5%

   \[\leadsto \color{blue}{\left(\left(t \cdot 2 \cdot 10^{-16}\right) \cdot 2 \cdot 10^{-16}\right) \cdot t} \]

9. Final simplification99.5%

   \[\leadsto t \cdot \left(2 \cdot 10^{-16} \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) \]

1. Initial program 3.4%

   \[\left(1 + t \cdot 2 \cdot 10^{-16}\right) \cdot \left(1 + t \cdot 2 \cdot 10^{-16}\right) + \left(-1 - 2 \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) \]
2. Step-by-step derivation

   1. associate-+r-9.9%

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

   2. sub-neg9.9%

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

   3. +-commutative9.9%

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

   4. difference-of-sqr--19.9%

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

   5. +-commutative9.9%

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

   6. associate--l+3.4%

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

   7. metadata-eval3.4%

      \[\leadsto \left(-2 \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) + \left(\left(1 + t \cdot 2 \cdot 10^{-16}\right) + 1\right) \cdot \left(t \cdot 2 \cdot 10^{-16} + \color{blue}{0}\right) \]

   8. +-rgt-identity3.4%

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

   9. distribute-lft1-in20.9%

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

   10. *-commutative20.9%

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

   11. associate-+r+20.9%

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

   12. +-commutative20.9%

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

   13. +-commutative20.9%

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

   14. *-rgt-identity20.9%

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

3. Simplified99.3%

   \[\leadsto \color{blue}{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)} \]

4. Taylor expanded in t around 0 99.3%

   \[\leadsto \color{blue}{4 \cdot 10^{-32} \cdot {t}^{2}} \]
5. Step-by-step derivation

   1. *-commutative99.3%

      \[\leadsto \color{blue}{{t}^{2} \cdot 4 \cdot 10^{-32}} \]

   2. unpow299.3%

      \[\leadsto \color{blue}{\left(t \cdot t\right)} \cdot 4 \cdot 10^{-32} \]

   3. metadata-eval99.1%

      \[\leadsto \left(t \cdot t\right) \cdot \color{blue}{\left(2 \cdot 10^{-16} \cdot 2 \cdot 10^{-16}\right)} \]

   4. swap-sqr99.3%

      \[\leadsto \color{blue}{\left(t \cdot 2 \cdot 10^{-16}\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right)} \]

   5. unpow299.3%

      \[\leadsto \color{blue}{{\left(t \cdot 2 \cdot 10^{-16}\right)}^{2}} \]

6. Simplified99.3%

   \[\leadsto \color{blue}{{\left(t \cdot 2 \cdot 10^{-16}\right)}^{2}} \]
7. Step-by-step derivation

   1. unpow299.3%

      \[\leadsto \color{blue}{\left(t \cdot 2 \cdot 10^{-16}\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right)} \]

   2. add-sqr-sqrt98.9%

      \[\leadsto \left(\color{blue}{\left(\sqrt{t} \cdot \sqrt{t}\right)} \cdot 2 \cdot 10^{-16}\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   3. associate-*l*99.1%

      \[\leadsto \color{blue}{\left(\sqrt{t} \cdot \left(\sqrt{t} \cdot 2 \cdot 10^{-16}\right)\right)} \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   4. metadata-eval99.1%

      \[\leadsto \left(\sqrt{t} \cdot \left(\sqrt{t} \cdot \color{blue}{\sqrt{4 \cdot 10^{-32}}}\right)\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   5. sqrt-prod99.4%

      \[\leadsto \left(\sqrt{t} \cdot \color{blue}{\sqrt{t \cdot 4 \cdot 10^{-32}}}\right) \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   6. sqrt-prod99.4%

      \[\leadsto \color{blue}{\sqrt{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)}} \cdot \left(t \cdot 2 \cdot 10^{-16}\right) \]

   7. associate-*r*99.4%

      \[\leadsto \color{blue}{\left(\sqrt{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)} \cdot t\right) \cdot 2 \cdot 10^{-16}} \]

   8. associate-*r*99.3%

      \[\leadsto \left(\sqrt{\color{blue}{\left(t \cdot t\right) \cdot 4 \cdot 10^{-32}}} \cdot t\right) \cdot 2 \cdot 10^{-16} \]

   9. sqrt-prod99.4%

      \[\leadsto \left(\color{blue}{\left(\sqrt{t \cdot t} \cdot \sqrt{4 \cdot 10^{-32}}\right)} \cdot t\right) \cdot 2 \cdot 10^{-16} \]

   10. sqrt-prod98.9%

       \[\leadsto \left(\left(\color{blue}{\left(\sqrt{t} \cdot \sqrt{t}\right)} \cdot \sqrt{4 \cdot 10^{-32}}\right) \cdot t\right) \cdot 2 \cdot 10^{-16} \]

   11. add-sqr-sqrt99.4%

       \[\leadsto \left(\left(\color{blue}{t} \cdot \sqrt{4 \cdot 10^{-32}}\right) \cdot t\right) \cdot 2 \cdot 10^{-16} \]

   12. metadata-eval99.4%

       \[\leadsto \left(\left(t \cdot \color{blue}{2 \cdot 10^{-16}}\right) \cdot t\right) \cdot 2 \cdot 10^{-16} \]

8. Applied egg-rr99.4%

   \[\leadsto \color{blue}{\left(\left(t \cdot 2 \cdot 10^{-16}\right) \cdot t\right) \cdot 2 \cdot 10^{-16}} \]

9. Taylor expanded in t around 0 99.3%

   \[\leadsto \color{blue}{\left(2 \cdot 10^{-16} \cdot {t}^{2}\right)} \cdot 2 \cdot 10^{-16} \]
10. Step-by-step derivation

    1. unpow299.3%

       \[\leadsto \left(2 \cdot 10^{-16} \cdot \color{blue}{\left(t \cdot t\right)}\right) \cdot 2 \cdot 10^{-16} \]

11. Simplified99.3%

    \[\leadsto \color{blue}{\left(2 \cdot 10^{-16} \cdot \left(t \cdot t\right)\right)} \cdot 2 \cdot 10^{-16} \]

12. Final simplification99.3%

    \[\leadsto 2 \cdot 10^{-16} \cdot \left(2 \cdot 10^{-16} \cdot \left(t \cdot t\right)\right) \]

1. Initial program 3.4%

   \[\left(1 + t \cdot 2 \cdot 10^{-16}\right) \cdot \left(1 + t \cdot 2 \cdot 10^{-16}\right) + \left(-1 - 2 \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) \]
2. Step-by-step derivation

   1. associate-+r-9.9%

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

   2. sub-neg9.9%

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

   3. +-commutative9.9%

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

   4. difference-of-sqr--19.9%

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

   5. +-commutative9.9%

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

   6. associate--l+3.4%

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

   7. metadata-eval3.4%

      \[\leadsto \left(-2 \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) + \left(\left(1 + t \cdot 2 \cdot 10^{-16}\right) + 1\right) \cdot \left(t \cdot 2 \cdot 10^{-16} + \color{blue}{0}\right) \]

   8. +-rgt-identity3.4%

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

   9. distribute-lft1-in20.9%

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

   10. *-commutative20.9%

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

   11. associate-+r+20.9%

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

   12. +-commutative20.9%

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

   13. +-commutative20.9%

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

   14. *-rgt-identity20.9%

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

3. Simplified99.3%

   \[\leadsto \color{blue}{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)} \]

4. Taylor expanded in t around 0 99.3%

   \[\leadsto \color{blue}{4 \cdot 10^{-32} \cdot {t}^{2}} \]
5. Step-by-step derivation

   1. unpow299.3%

      \[\leadsto 4 \cdot 10^{-32} \cdot \color{blue}{\left(t \cdot t\right)} \]

6. Simplified99.3%

   \[\leadsto \color{blue}{4 \cdot 10^{-32} \cdot \left(t \cdot t\right)} \]

7. Final simplification99.3%

   \[\leadsto \left(t \cdot t\right) \cdot 4 \cdot 10^{-32} \]

1. Initial program 3.4%

   \[\left(1 + t \cdot 2 \cdot 10^{-16}\right) \cdot \left(1 + t \cdot 2 \cdot 10^{-16}\right) + \left(-1 - 2 \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) \]
2. Step-by-step derivation

   1. associate-+r-9.9%

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

   2. sub-neg9.9%

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

   3. +-commutative9.9%

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

   4. difference-of-sqr--19.9%

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

   5. +-commutative9.9%

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

   6. associate--l+3.4%

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

   7. metadata-eval3.4%

      \[\leadsto \left(-2 \cdot \left(t \cdot 2 \cdot 10^{-16}\right)\right) + \left(\left(1 + t \cdot 2 \cdot 10^{-16}\right) + 1\right) \cdot \left(t \cdot 2 \cdot 10^{-16} + \color{blue}{0}\right) \]

   8. +-rgt-identity3.4%

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

   9. distribute-lft1-in20.9%

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

   10. *-commutative20.9%

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

   11. associate-+r+20.9%

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

   12. +-commutative20.9%

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

   13. +-commutative20.9%

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

   14. *-rgt-identity20.9%

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

3. Simplified99.3%

   \[\leadsto \color{blue}{t \cdot \left(t \cdot 4 \cdot 10^{-32}\right)} \]

4. Final simplification99.3%

   \[\leadsto t \cdot \left(t \cdot 4 \cdot 10^{-32}\right) \]

herbie shell --seed 2023166 
(FPCore (t)
  :name "fma_test1"
  :precision binary64
  :pre (and (<= 0.9 t) (<= t 1.1))

  :herbie-target
  (fma (+ 1.0 (* t 2e-16)) (+ 1.0 (* t 2e-16)) (- -1.0 (* 2.0 (* t 2e-16))))

  (+ (* (+ 1.0 (* t 2e-16)) (+ 1.0 (* t 2e-16))) (- -1.0 (* 2.0 (* t 2e-16)))))