Error

Derivation

1. Initial program 2.4

   \[\frac{\left(\frac{\left(\left(i \cdot i\right) \cdot \left(i \cdot i\right)\right)}{\left(\left(\left(real->posit(2)\right) \cdot i\right) \cdot \left(\left(real->posit(2)\right) \cdot i\right)\right)}\right)}{\left(\left(\left(\left(real->posit(2)\right) \cdot i\right) \cdot \left(\left(real->posit(2)\right) \cdot i\right)\right) - \left(real->posit(1.0)\right)\right)}\]

2. Simplified2.4

   \[\leadsto \color{blue}{\left(\frac{\left(i \cdot i\right)}{\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) \cdot \left(i \cdot \left(real->posit(2)\right)\right)\right) \cdot \left(\left(\left(i \cdot \left(real->posit(2)\right)\right) \cdot \left(i \cdot \left(real->posit(2)\right)\right)\right) - \left(real->posit(1.0)\right)\right)\right)}\right) \cdot \left(i \cdot i\right)}\]
3. Using strategy rm

4. Applied *-commutative2.4

   \[\leadsto \left(\frac{\left(i \cdot i\right)}{\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) \cdot \left(i \cdot \left(real->posit(2)\right)\right)\right) \cdot \left(\color{blue}{\left(\left(i \cdot \left(real->posit(2)\right)\right) \cdot \left(i \cdot \left(real->posit(2)\right)\right)\right)} - \left(real->posit(1.0)\right)\right)\right)}\right) \cdot \left(i \cdot i\right)\]

5. Applied difference-of-sqr-12.4

   \[\leadsto \left(\frac{\left(i \cdot i\right)}{\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) \cdot \left(i \cdot \left(real->posit(2)\right)\right)\right) \cdot \color{blue}{\left(\left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right) \cdot \left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)\right)}\right)}\right) \cdot \left(i \cdot i\right)\]

6. Applied associate-*r*2.4

   \[\leadsto \left(\frac{\left(i \cdot i\right)}{\color{blue}{\left(\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) \cdot \left(i \cdot \left(real->posit(2)\right)\right)\right) \cdot \left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)\right) \cdot \left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)\right)}}\right) \cdot \left(i \cdot i\right)\]

7. Applied associate-/r*1.7

   \[\leadsto \color{blue}{\left(\frac{\left(\frac{\left(i \cdot i\right)}{\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) \cdot \left(i \cdot \left(real->posit(2)\right)\right)\right) \cdot \left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)\right)}\right)}{\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)}\right)} \cdot \left(i \cdot i\right)\]

8. Applied associate-*l/1.8

   \[\leadsto \color{blue}{\frac{\left(\left(\frac{\left(i \cdot i\right)}{\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) \cdot \left(i \cdot \left(real->posit(2)\right)\right)\right) \cdot \left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)\right)}\right) \cdot \left(i \cdot i\right)\right)}{\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)}}\]

9. Simplified0.7

   \[\leadsto \frac{\color{blue}{\left(\frac{\left(\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(real->posit(1.0)\right)\right) \cdot \left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(real->posit(1.0)\right)\right)\right)}{\left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)}\right)}}{\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)}\]
10. Using strategy rm

11. Applied *-commutative0.7

    \[\leadsto \frac{\left(\frac{\left(\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(real->posit(1.0)\right)\right) \cdot \color{blue}{\left(\left(real->posit(1.0)\right) \cdot \left(\frac{i}{\left(real->posit(2)\right)}\right)\right)}\right)}{\left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)}\right)}{\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)}\]

12. Applied associate-*r*0.7

    \[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(real->posit(1.0)\right)\right) \cdot \left(real->posit(1.0)\right)\right) \cdot \left(\frac{i}{\left(real->posit(2)\right)}\right)\right)}}{\left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)}\right)}{\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)}\]

13. Applied associate-/l*0.5

    \[\leadsto \frac{\color{blue}{\left(\frac{\left(\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(real->posit(1.0)\right)\right) \cdot \left(real->posit(1.0)\right)\right)}{\left(\frac{\left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)}{\left(\frac{i}{\left(real->posit(2)\right)}\right)}\right)}\right)}}{\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)}\]

14. Applied associate-/l/0.5

    \[\leadsto \color{blue}{\frac{\left(\left(\left(\frac{i}{\left(real->posit(2)\right)}\right) \cdot \left(real->posit(1.0)\right)\right) \cdot \left(real->posit(1.0)\right)\right)}{\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right) \cdot \left(\frac{\left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)}{\left(\frac{i}{\left(real->posit(2)\right)}\right)}\right)\right)}}\]

15. Simplified0.5

    \[\leadsto \frac{\color{blue}{\left(\frac{i}{\left(real->posit(2)\right)}\right)}}{\left(\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right) \cdot \left(\frac{\left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)}{\left(\frac{i}{\left(real->posit(2)\right)}\right)}\right)\right)}\]
16. Using strategy rm

17. Applied associate-/r*0.4

    \[\leadsto \color{blue}{\frac{\left(\frac{\left(\frac{i}{\left(real->posit(2)\right)}\right)}{\left(\left(i \cdot \left(real->posit(2)\right)\right) - \left(real->posit(1.0)\right)\right)}\right)}{\left(\frac{\left(\frac{\left(i \cdot \left(real->posit(2)\right)\right)}{\left(real->posit(1.0)\right)}\right)}{\left(\frac{i}{\left(real->posit(2)\right)}\right)}\right)}}\]

18. Final simplification0.4

    \[\leadsto \frac{\frac{\frac{i}{2}}{i \cdot 2 - 1.0}}{\frac{i \cdot 2 + 1.0}{\frac{i}{2}}}\]

Reproduce

herbie shell --seed 2019088 +o rules:numerics
(FPCore (i)
  :name "Octave 3.8, jcobi/4, as called"
  :pre (and (>.p16 i (real->posit16 0)))
  (/.p16 (/.p16 (*.p16 (*.p16 i i) (*.p16 i i)) (*.p16 (*.p16 (real->posit16 2) i) (*.p16 (real->posit16 2) i))) (-.p16 (*.p16 (*.p16 (real->posit16 2) i) (*.p16 (real->posit16 2) i)) (real->posit16 1.0))))