(- (/ x0 (- 1 x1)) x0)

Average Error: 7.8 → 7.2

Time: 52.8s

Precision: 64

• could not determine a ground truth for program pre

  1. x0 = 2.985
  2. x1 = 0.000209

\[x0 = 1.854999999999999982236431605997495353222 \land x1 = 2.090000000000000115064208161541614572343 \cdot 10^{-4} \lor x0 = 2.984999999999999875655021241982467472553 \land x1 = 0.01859999999999999847899445626353553961962\]

Math

\[\frac{x0}{1 - x1} - x0\]

↓

\[\frac{\frac{\frac{\frac{\left(\left(\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right)\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\left(\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right)\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) - \left(\left(\left(x0 \cdot x0\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right)}{\left(\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right)\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(\left(x0 \cdot x0\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)}}{\left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right) + \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) + \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right)\right)}}{\left(\left(x0 \cdot x0\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) + \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}} \cdot x0}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(\frac{x0}{1 - x1} \cdot x0 + x0 \cdot x0\right)}\]

C

double f(double x0, double x1) {
        double r6709693 = x0;
        double r6709694 = 1.0;
        double r6709695 = x1;
        double r6709696 = r6709694 - r6709695;
        double r6709697 = r6709693 / r6709696;
        double r6709698 = r6709697 - r6709693;
        return r6709698;
}

↓

double f(double x0, double x1) {
        double r6709699 = x0;
        double r6709700 = 1.0;
        double r6709701 = x1;
        double r6709702 = r6709700 - r6709701;
        double r6709703 = r6709699 / r6709702;
        double r6709704 = r6709703 * r6709703;
        double r6709705 = r6709704 / r6709702;
        double r6709706 = r6709705 * r6709705;
        double r6709707 = r6709706 * r6709706;
        double r6709708 = r6709707 * r6709707;
        double r6709709 = r6709708 * r6709705;
        double r6709710 = r6709709 * r6709709;
        double r6709711 = r6709699 * r6709699;
        double r6709712 = r6709711 * r6709711;
        double r6709713 = r6709712 * r6709712;
        double r6709714 = r6709711 * r6709713;
        double r6709715 = r6709714 * r6709713;
        double r6709716 = r6709715 * r6709715;
        double r6709717 = r6709710 - r6709716;
        double r6709718 = r6709709 + r6709715;
        double r6709719 = r6709717 / r6709718;
        double r6709720 = r6709712 * r6709711;
        double r6709721 = r6709706 * r6709705;
        double r6709722 = r6709720 + r6709721;
        double r6709723 = r6709722 * r6709721;
        double r6709724 = r6709720 * r6709720;
        double r6709725 = r6709723 + r6709724;
        double r6709726 = r6709719 / r6709725;
        double r6709727 = r6709711 * r6709705;
        double r6709728 = r6709727 + r6709712;
        double r6709729 = r6709728 + r6709706;
        double r6709730 = r6709726 / r6709729;
        double r6709731 = r6709730 * r6709699;
        double r6709732 = r6709703 * r6709699;
        double r6709733 = r6709732 + r6709711;
        double r6709734 = r6709704 + r6709733;
        double r6709735 = r6709731 / r6709734;
        return r6709735;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	7.8
Target	0.2
Herbie	7.2

\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

1. Initial program 7.8

   \[\frac{x0}{1 - x1} - x0\]
2. Using strategy rm

3. Applied flip3-- 7.6

   \[\leadsto \color{blue}{\frac{{\left(\frac{x0}{1 - x1}\right)}^{3} - {x0}^{3}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}}\]

4. Simplified 7.3

   \[\leadsto \frac{\color{blue}{x0 \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} - x0 \cdot x0\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]
5. Using strategy rm

6. Applied flip3-- 7.4

   \[\leadsto \frac{x0 \cdot \color{blue}{\frac{{\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)}^{3} - {\left(x0 \cdot x0\right)}^{3}}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right) + \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \left(x0 \cdot x0\right)\right)}}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]

7. Simplified 7.4

   \[\leadsto \frac{x0 \cdot \frac{\color{blue}{\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} - \left(x0 \cdot x0\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)}}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right) + \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \left(x0 \cdot x0\right)\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]
8. Using strategy rm

9. Applied flip3-- 7.3

   \[\leadsto \frac{x0 \cdot \frac{\color{blue}{\frac{{\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)}^{3} - {\left(\left(x0 \cdot x0\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)}^{3}}{\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) + \left(\left(\left(x0 \cdot x0\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right) + \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right)}}}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right) + \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \left(x0 \cdot x0\right)\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]

10. Simplified 7.1

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

11. Simplified 7.1

    \[\leadsto \frac{x0 \cdot \frac{\frac{\left(\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right)\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} - \left(\left(x0 \cdot x0\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)}{\color{blue}{\left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right)\right) + \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right)\right)}}}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right) + \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \left(x0 \cdot x0\right)\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]
12. Using strategy rm

13. Applied flip-- 7.2

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

14. Final simplification 7.2

    \[\leadsto \frac{\frac{\frac{\frac{\left(\left(\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right)\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\left(\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right)\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) - \left(\left(\left(x0 \cdot x0\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right)}{\left(\left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right)\right)\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(\left(x0 \cdot x0\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right)\right)}}{\left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right) + \left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \left(\left(\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}\right) + \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(\left(\left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot x0\right)\right)}}{\left(\left(x0 \cdot x0\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} + \left(x0 \cdot x0\right) \cdot \left(x0 \cdot x0\right)\right) + \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{1 - x1}} \cdot x0}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(\frac{x0}{1 - x1} \cdot x0 + x0 \cdot x0\right)}\]

Reproduce

herbie shell --seed 2019192 
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :pre (or (and (== x0 1.855) (== x1 0.000209)) (and (== x0 2.985) (== x1 0.0186)))

  :herbie-target
  (/ (* x0 x1) (- 1.0 x1))

  (- (/ x0 (- 1.0 x1)) x0))