Given's Rotation SVD example, simplified

Percentage Accurate: 75.9% → 99.4%

Time: 11.2s

Alternatives: 6

Speedup: 1.9×

Specification

Math

\[\begin{array}{l} \\ 1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \end{array} \]

FPCore

(FPCore (x)
 :precision binary64
 (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))

C

double code(double x) {
	return 1.0 - sqrt((0.5 * (1.0 + (1.0 / hypot(1.0, x)))));
}

Java

public static double code(double x) {
	return 1.0 - Math.sqrt((0.5 * (1.0 + (1.0 / Math.hypot(1.0, x)))));
}

Python

def code(x):
	return 1.0 - math.sqrt((0.5 * (1.0 + (1.0 / math.hypot(1.0, x)))))

Julia

function code(x)
	return Float64(1.0 - sqrt(Float64(0.5 * Float64(1.0 + Float64(1.0 / hypot(1.0, x))))))
end

MATLAB

function tmp = code(x)
	tmp = 1.0 - sqrt((0.5 * (1.0 + (1.0 / hypot(1.0, x)))));
end

Wolfram

code[x_] := N[(1.0 - N[Sqrt[N[(0.5 * N[(1.0 + N[(1.0 / N[Sqrt[1.0 ^ 2 + x ^ 2], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

Initial Program: 75.9% accurate, 1.0× speedup

Math

\[\begin{array}{l} \\ 1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \end{array} \]

FPCore

(FPCore (x)
 :precision binary64
 (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))

C

double code(double x) {
	return 1.0 - sqrt((0.5 * (1.0 + (1.0 / hypot(1.0, x)))));
}

Java

public static double code(double x) {
	return 1.0 - Math.sqrt((0.5 * (1.0 + (1.0 / Math.hypot(1.0, x)))));
}

Python

def code(x):
	return 1.0 - math.sqrt((0.5 * (1.0 + (1.0 / math.hypot(1.0, x)))))

Julia

function code(x)
	return Float64(1.0 - sqrt(Float64(0.5 * Float64(1.0 + Float64(1.0 / hypot(1.0, x))))))
end

MATLAB

function tmp = code(x)
	tmp = 1.0 - sqrt((0.5 * (1.0 + (1.0 / hypot(1.0, x)))));
end

Wolfram

code[x_] := N[(1.0 - N[Sqrt[N[(0.5 * N[(1.0 + N[(1.0 / N[Sqrt[1.0 ^ 2 + x ^ 2], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]

Alternative 1: 99.4% accurate, 0.5× speedup

Math

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\_m\right) \leq 2:\\ \;\;\;\;{x\_m}^{2} \cdot \left(0.125 + {x\_m}^{2} \cdot \left({x\_m}^{2} \cdot 0.0673828125 - 0.0859375\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5 - \frac{0.5}{x\_m}}{1 + \sqrt{0.5 + \frac{0.5}{x\_m}}}\\ \end{array} \end{array} \]

FPCore

x_m = (fabs.f64 x)
(FPCore (x_m)
 :precision binary64
 (if (<= (hypot 1.0 x_m) 2.0)
   (*
    (pow x_m 2.0)
    (+ 0.125 (* (pow x_m 2.0) (- (* (pow x_m 2.0) 0.0673828125) 0.0859375))))
   (/ (- 0.5 (/ 0.5 x_m)) (+ 1.0 (sqrt (+ 0.5 (/ 0.5 x_m)))))))

C

x_m = fabs(x);
double code(double x_m) {
	double tmp;
	if (hypot(1.0, x_m) <= 2.0) {
		tmp = pow(x_m, 2.0) * (0.125 + (pow(x_m, 2.0) * ((pow(x_m, 2.0) * 0.0673828125) - 0.0859375)));
	} else {
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + sqrt((0.5 + (0.5 / x_m))));
	}
	return tmp;
}

Java

x_m = Math.abs(x);
public static double code(double x_m) {
	double tmp;
	if (Math.hypot(1.0, x_m) <= 2.0) {
		tmp = Math.pow(x_m, 2.0) * (0.125 + (Math.pow(x_m, 2.0) * ((Math.pow(x_m, 2.0) * 0.0673828125) - 0.0859375)));
	} else {
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + Math.sqrt((0.5 + (0.5 / x_m))));
	}
	return tmp;
}

Python

x_m = math.fabs(x)
def code(x_m):
	tmp = 0
	if math.hypot(1.0, x_m) <= 2.0:
		tmp = math.pow(x_m, 2.0) * (0.125 + (math.pow(x_m, 2.0) * ((math.pow(x_m, 2.0) * 0.0673828125) - 0.0859375)))
	else:
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + math.sqrt((0.5 + (0.5 / x_m))))
	return tmp

Julia

x_m = abs(x)
function code(x_m)
	tmp = 0.0
	if (hypot(1.0, x_m) <= 2.0)
		tmp = Float64((x_m ^ 2.0) * Float64(0.125 + Float64((x_m ^ 2.0) * Float64(Float64((x_m ^ 2.0) * 0.0673828125) - 0.0859375))));
	else
		tmp = Float64(Float64(0.5 - Float64(0.5 / x_m)) / Float64(1.0 + sqrt(Float64(0.5 + Float64(0.5 / x_m)))));
	end
	return tmp
end

MATLAB

x_m = abs(x);
function tmp_2 = code(x_m)
	tmp = 0.0;
	if (hypot(1.0, x_m) <= 2.0)
		tmp = (x_m ^ 2.0) * (0.125 + ((x_m ^ 2.0) * (((x_m ^ 2.0) * 0.0673828125) - 0.0859375)));
	else
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + sqrt((0.5 + (0.5 / x_m))));
	end
	tmp_2 = tmp;
end

Wolfram

x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := If[LessEqual[N[Sqrt[1.0 ^ 2 + x$95$m ^ 2], $MachinePrecision], 2.0], N[(N[Power[x$95$m, 2.0], $MachinePrecision] * N[(0.125 + N[(N[Power[x$95$m, 2.0], $MachinePrecision] * N[(N[(N[Power[x$95$m, 2.0], $MachinePrecision] * 0.0673828125), $MachinePrecision] - 0.0859375), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(0.5 - N[(0.5 / x$95$m), $MachinePrecision]), $MachinePrecision] / N[(1.0 + N[Sqrt[N[(0.5 + N[(0.5 / x$95$m), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if (hypot.f64 #s(literal 1 binary64) x) < 2

   1. Initial program 49.6%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 49.6%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 49.6%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 49.6%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 49.6%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 49.6%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around 0 100.0%

      \[\leadsto \color{blue}{{x}^{2} \cdot \left(0.125 + {x}^{2} \cdot \left(0.0673828125 \cdot {x}^{2} - 0.0859375\right)\right)} \]

   if 2 < (hypot.f64 #s(literal 1 binary64) x)

   1. Initial program 98.5%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 98.5%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf 98.4%

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 + 0.5 \cdot \frac{1}{x}}} \]
   6. Step-by-step derivation

      1. associate-*r/ 98.4%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{x}}} \]

      2. metadata-eval 98.4%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{x}} \]

   7. Simplified 98.4%

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 + \frac{0.5}{x}}} \]
   8. Step-by-step derivation

      1. flip-- 98.4%

         \[\leadsto \color{blue}{\frac{1 \cdot 1 - \sqrt{0.5 + \frac{0.5}{x}} \cdot \sqrt{0.5 + \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}} \]

      2. metadata-eval 98.4%

         \[\leadsto \frac{\color{blue}{1} - \sqrt{0.5 + \frac{0.5}{x}} \cdot \sqrt{0.5 + \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      3. add-sqr-sqrt 99.9%

         \[\leadsto \frac{1 - \color{blue}{\left(0.5 + \frac{0.5}{x}\right)}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      4. associate--r+ 99.9%

         \[\leadsto \frac{\color{blue}{\left(1 - 0.5\right) - \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      5. metadata-eval 99.9%

         \[\leadsto \frac{\color{blue}{0.5} - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

   9. Applied egg-rr 99.9%

      \[\leadsto \color{blue}{\frac{0.5 - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 100.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \leq 2:\\ \;\;\;\;{x}^{2} \cdot \left(0.125 + {x}^{2} \cdot \left({x}^{2} \cdot 0.0673828125 - 0.0859375\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5 - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}\\ \end{array} \]
5. Add Preprocessing

Alternative 2: 99.3% accurate, 0.7× speedup

Math

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\_m\right) \leq 2:\\ \;\;\;\;{x\_m}^{2} \cdot \left(0.125 + {x\_m}^{2} \cdot -0.0859375\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5 - \frac{0.5}{x\_m}}{1 + \sqrt{0.5 + \frac{0.5}{x\_m}}}\\ \end{array} \end{array} \]

FPCore

x_m = (fabs.f64 x)
(FPCore (x_m)
 :precision binary64
 (if (<= (hypot 1.0 x_m) 2.0)
   (* (pow x_m 2.0) (+ 0.125 (* (pow x_m 2.0) -0.0859375)))
   (/ (- 0.5 (/ 0.5 x_m)) (+ 1.0 (sqrt (+ 0.5 (/ 0.5 x_m)))))))

C

x_m = fabs(x);
double code(double x_m) {
	double tmp;
	if (hypot(1.0, x_m) <= 2.0) {
		tmp = pow(x_m, 2.0) * (0.125 + (pow(x_m, 2.0) * -0.0859375));
	} else {
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + sqrt((0.5 + (0.5 / x_m))));
	}
	return tmp;
}

Java

x_m = Math.abs(x);
public static double code(double x_m) {
	double tmp;
	if (Math.hypot(1.0, x_m) <= 2.0) {
		tmp = Math.pow(x_m, 2.0) * (0.125 + (Math.pow(x_m, 2.0) * -0.0859375));
	} else {
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + Math.sqrt((0.5 + (0.5 / x_m))));
	}
	return tmp;
}

Python

x_m = math.fabs(x)
def code(x_m):
	tmp = 0
	if math.hypot(1.0, x_m) <= 2.0:
		tmp = math.pow(x_m, 2.0) * (0.125 + (math.pow(x_m, 2.0) * -0.0859375))
	else:
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + math.sqrt((0.5 + (0.5 / x_m))))
	return tmp

Julia

x_m = abs(x)
function code(x_m)
	tmp = 0.0
	if (hypot(1.0, x_m) <= 2.0)
		tmp = Float64((x_m ^ 2.0) * Float64(0.125 + Float64((x_m ^ 2.0) * -0.0859375)));
	else
		tmp = Float64(Float64(0.5 - Float64(0.5 / x_m)) / Float64(1.0 + sqrt(Float64(0.5 + Float64(0.5 / x_m)))));
	end
	return tmp
end

MATLAB

x_m = abs(x);
function tmp_2 = code(x_m)
	tmp = 0.0;
	if (hypot(1.0, x_m) <= 2.0)
		tmp = (x_m ^ 2.0) * (0.125 + ((x_m ^ 2.0) * -0.0859375));
	else
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + sqrt((0.5 + (0.5 / x_m))));
	end
	tmp_2 = tmp;
end

Wolfram

x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := If[LessEqual[N[Sqrt[1.0 ^ 2 + x$95$m ^ 2], $MachinePrecision], 2.0], N[(N[Power[x$95$m, 2.0], $MachinePrecision] * N[(0.125 + N[(N[Power[x$95$m, 2.0], $MachinePrecision] * -0.0859375), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(N[(0.5 - N[(0.5 / x$95$m), $MachinePrecision]), $MachinePrecision] / N[(1.0 + N[Sqrt[N[(0.5 + N[(0.5 / x$95$m), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if (hypot.f64 #s(literal 1 binary64) x) < 2

   1. Initial program 49.6%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 49.6%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 49.6%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 49.6%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 49.6%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 49.6%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around 0 99.9%

      \[\leadsto \color{blue}{{x}^{2} \cdot \left(0.125 + -0.0859375 \cdot {x}^{2}\right)} \]
   6. Step-by-step derivation

      1. *-commutative 99.9%

         \[\leadsto {x}^{2} \cdot \left(0.125 + \color{blue}{{x}^{2} \cdot -0.0859375}\right) \]

   7. Simplified 99.9%

      \[\leadsto \color{blue}{{x}^{2} \cdot \left(0.125 + {x}^{2} \cdot -0.0859375\right)} \]

   if 2 < (hypot.f64 #s(literal 1 binary64) x)

   1. Initial program 98.5%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 98.5%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf 98.4%

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 + 0.5 \cdot \frac{1}{x}}} \]
   6. Step-by-step derivation

      1. associate-*r/ 98.4%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{x}}} \]

      2. metadata-eval 98.4%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{x}} \]

   7. Simplified 98.4%

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 + \frac{0.5}{x}}} \]
   8. Step-by-step derivation

      1. flip-- 98.4%

         \[\leadsto \color{blue}{\frac{1 \cdot 1 - \sqrt{0.5 + \frac{0.5}{x}} \cdot \sqrt{0.5 + \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}} \]

      2. metadata-eval 98.4%

         \[\leadsto \frac{\color{blue}{1} - \sqrt{0.5 + \frac{0.5}{x}} \cdot \sqrt{0.5 + \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      3. add-sqr-sqrt 99.9%

         \[\leadsto \frac{1 - \color{blue}{\left(0.5 + \frac{0.5}{x}\right)}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      4. associate--r+ 99.9%

         \[\leadsto \frac{\color{blue}{\left(1 - 0.5\right) - \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      5. metadata-eval 99.9%

         \[\leadsto \frac{\color{blue}{0.5} - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

   9. Applied egg-rr 99.9%

      \[\leadsto \color{blue}{\frac{0.5 - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 99.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \leq 2:\\ \;\;\;\;{x}^{2} \cdot \left(0.125 + {x}^{2} \cdot -0.0859375\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5 - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}\\ \end{array} \]
5. Add Preprocessing

Alternative 3: 99.1% accurate, 1.0× speedup

Math

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\_m\right) \leq 2:\\ \;\;\;\;\left(x\_m \cdot x\_m\right) \cdot \left(--0.125\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5 - \frac{0.5}{x\_m}}{1 + \sqrt{0.5 + \frac{0.5}{x\_m}}}\\ \end{array} \end{array} \]

FPCore

x_m = (fabs.f64 x)
(FPCore (x_m)
 :precision binary64
 (if (<= (hypot 1.0 x_m) 2.0)
   (* (* x_m x_m) (- -0.125))
   (/ (- 0.5 (/ 0.5 x_m)) (+ 1.0 (sqrt (+ 0.5 (/ 0.5 x_m)))))))

C

x_m = fabs(x);
double code(double x_m) {
	double tmp;
	if (hypot(1.0, x_m) <= 2.0) {
		tmp = (x_m * x_m) * -(-0.125);
	} else {
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + sqrt((0.5 + (0.5 / x_m))));
	}
	return tmp;
}

Java

x_m = Math.abs(x);
public static double code(double x_m) {
	double tmp;
	if (Math.hypot(1.0, x_m) <= 2.0) {
		tmp = (x_m * x_m) * -(-0.125);
	} else {
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + Math.sqrt((0.5 + (0.5 / x_m))));
	}
	return tmp;
}

Python

x_m = math.fabs(x)
def code(x_m):
	tmp = 0
	if math.hypot(1.0, x_m) <= 2.0:
		tmp = (x_m * x_m) * -(-0.125)
	else:
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + math.sqrt((0.5 + (0.5 / x_m))))
	return tmp

Julia

x_m = abs(x)
function code(x_m)
	tmp = 0.0
	if (hypot(1.0, x_m) <= 2.0)
		tmp = Float64(Float64(x_m * x_m) * Float64(-(-0.125)));
	else
		tmp = Float64(Float64(0.5 - Float64(0.5 / x_m)) / Float64(1.0 + sqrt(Float64(0.5 + Float64(0.5 / x_m)))));
	end
	return tmp
end

MATLAB

x_m = abs(x);
function tmp_2 = code(x_m)
	tmp = 0.0;
	if (hypot(1.0, x_m) <= 2.0)
		tmp = (x_m * x_m) * -(-0.125);
	else
		tmp = (0.5 - (0.5 / x_m)) / (1.0 + sqrt((0.5 + (0.5 / x_m))));
	end
	tmp_2 = tmp;
end

Wolfram

x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := If[LessEqual[N[Sqrt[1.0 ^ 2 + x$95$m ^ 2], $MachinePrecision], 2.0], N[(N[(x$95$m * x$95$m), $MachinePrecision] * (--0.125)), $MachinePrecision], N[(N[(0.5 - N[(0.5 / x$95$m), $MachinePrecision]), $MachinePrecision] / N[(1.0 + N[Sqrt[N[(0.5 + N[(0.5 / x$95$m), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if (hypot.f64 #s(literal 1 binary64) x) < 2

   1. Initial program 49.6%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 49.6%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 49.6%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 49.6%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 49.6%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 49.6%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around 0 49.5%

      \[\leadsto 1 - \color{blue}{\left(1 + -0.125 \cdot {x}^{2}\right)} \]
   6. Step-by-step derivation

      1. *-commutative 49.5%

         \[\leadsto 1 - \left(1 + \color{blue}{{x}^{2} \cdot -0.125}\right) \]

   7. Simplified 49.5%

      \[\leadsto 1 - \color{blue}{\left(1 + {x}^{2} \cdot -0.125\right)} \]
   8. Step-by-step derivation

      1. associate--r+ 99.3%

         \[\leadsto \color{blue}{\left(1 - 1\right) - {x}^{2} \cdot -0.125} \]

      2. metadata-eval 99.3%

         \[\leadsto \color{blue}{0} - {x}^{2} \cdot -0.125 \]

      3. flip-- 28.8%

         \[\leadsto \color{blue}{\frac{0 \cdot 0 - \left({x}^{2} \cdot -0.125\right) \cdot \left({x}^{2} \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125}} \]

      4. metadata-eval 28.8%

         \[\leadsto \frac{\color{blue}{0} - \left({x}^{2} \cdot -0.125\right) \cdot \left({x}^{2} \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      5. swap-sqr 28.8%

         \[\leadsto \frac{0 - \color{blue}{\left({x}^{2} \cdot {x}^{2}\right) \cdot \left(-0.125 \cdot -0.125\right)}}{0 + {x}^{2} \cdot -0.125} \]

      6. pow-prod-up 28.7%

         \[\leadsto \frac{0 - \color{blue}{{x}^{\left(2 + 2\right)}} \cdot \left(-0.125 \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      7. metadata-eval 28.7%

         \[\leadsto \frac{0 - {x}^{\color{blue}{4}} \cdot \left(-0.125 \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      8. metadata-eval 28.7%

         \[\leadsto \frac{0 - {x}^{4} \cdot \color{blue}{0.015625}}{0 + {x}^{2} \cdot -0.125} \]

   9. Applied egg-rr 28.7%

      \[\leadsto \color{blue}{\frac{0 - {x}^{4} \cdot 0.015625}{0 + {x}^{2} \cdot -0.125}} \]
   10. Step-by-step derivation

       1. sub0-neg 28.7%

          \[\leadsto \frac{\color{blue}{-{x}^{4} \cdot 0.015625}}{0 + {x}^{2} \cdot -0.125} \]

       2. +-lft-identity 28.7%

          \[\leadsto \frac{-\color{blue}{\left(0 + {x}^{4} \cdot 0.015625\right)}}{0 + {x}^{2} \cdot -0.125} \]

       3. +-commutative 28.7%

          \[\leadsto \frac{-\color{blue}{\left({x}^{4} \cdot 0.015625 + 0\right)}}{0 + {x}^{2} \cdot -0.125} \]

       4. mul0-lft 28.7%

          \[\leadsto \frac{-\left({x}^{4} \cdot 0.015625 + \color{blue}{0 \cdot \left({x}^{2} \cdot -0.125\right)}\right)}{0 + {x}^{2} \cdot -0.125} \]

       5. +-lft-identity 28.7%

          \[\leadsto \frac{-\color{blue}{\left(0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)\right)}}{0 + {x}^{2} \cdot -0.125} \]

       6. +-lft-identity 28.7%

          \[\leadsto \frac{-\left(0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)\right)}{\color{blue}{{x}^{2} \cdot -0.125}} \]

       7. distribute-frac-neg 28.7%

          \[\leadsto \color{blue}{-\frac{0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)}{{x}^{2} \cdot -0.125}} \]

       8. +-lft-identity 28.7%

          \[\leadsto -\frac{\color{blue}{{x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)}}{{x}^{2} \cdot -0.125} \]

       9. mul0-lft 28.7%

          \[\leadsto -\frac{{x}^{4} \cdot 0.015625 + \color{blue}{0}}{{x}^{2} \cdot -0.125} \]

       10. +-commutative 28.7%

           \[\leadsto -\frac{\color{blue}{0 + {x}^{4} \cdot 0.015625}}{{x}^{2} \cdot -0.125} \]

       11. +-lft-identity 28.7%

           \[\leadsto -\frac{\color{blue}{{x}^{4} \cdot 0.015625}}{{x}^{2} \cdot -0.125} \]

       12. +-lft-identity 28.7%

           \[\leadsto -\frac{{x}^{4} \cdot 0.015625}{\color{blue}{0 + {x}^{2} \cdot -0.125}} \]

       13. *-commutative 28.7%

           \[\leadsto -\frac{\color{blue}{0.015625 \cdot {x}^{4}}}{0 + {x}^{2} \cdot -0.125} \]

       14. +-lft-identity 28.7%

           \[\leadsto -\frac{0.015625 \cdot {x}^{4}}{\color{blue}{{x}^{2} \cdot -0.125}} \]

       15. *-commutative 28.7%

           \[\leadsto -\frac{0.015625 \cdot {x}^{4}}{\color{blue}{-0.125 \cdot {x}^{2}}} \]

       16. times-frac 28.8%

           \[\leadsto -\color{blue}{\frac{0.015625}{-0.125} \cdot \frac{{x}^{4}}{{x}^{2}}} \]

       17. metadata-eval 28.8%

           \[\leadsto -\color{blue}{-0.125} \cdot \frac{{x}^{4}}{{x}^{2}} \]

   11. Simplified 28.8%

       \[\leadsto \color{blue}{--0.125 \cdot \frac{{x}^{4}}{{x}^{2}}} \]
   12. Step-by-step derivation

       1. pow-div 99.3%

          \[\leadsto --0.125 \cdot \color{blue}{{x}^{\left(4 - 2\right)}} \]

       2. metadata-eval 99.3%

          \[\leadsto --0.125 \cdot {x}^{\color{blue}{2}} \]

       3. unpow2 99.3%

          \[\leadsto --0.125 \cdot \color{blue}{\left(x \cdot x\right)} \]

   13. Applied egg-rr 99.3%

       \[\leadsto --0.125 \cdot \color{blue}{\left(x \cdot x\right)} \]

   if 2 < (hypot.f64 #s(literal 1 binary64) x)

   1. Initial program 98.5%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 98.5%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf 98.4%

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 + 0.5 \cdot \frac{1}{x}}} \]
   6. Step-by-step derivation

      1. associate-*r/ 98.4%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{x}}} \]

      2. metadata-eval 98.4%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{x}} \]

   7. Simplified 98.4%

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 + \frac{0.5}{x}}} \]
   8. Step-by-step derivation

      1. flip-- 98.4%

         \[\leadsto \color{blue}{\frac{1 \cdot 1 - \sqrt{0.5 + \frac{0.5}{x}} \cdot \sqrt{0.5 + \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}} \]

      2. metadata-eval 98.4%

         \[\leadsto \frac{\color{blue}{1} - \sqrt{0.5 + \frac{0.5}{x}} \cdot \sqrt{0.5 + \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      3. add-sqr-sqrt 99.9%

         \[\leadsto \frac{1 - \color{blue}{\left(0.5 + \frac{0.5}{x}\right)}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      4. associate--r+ 99.9%

         \[\leadsto \frac{\color{blue}{\left(1 - 0.5\right) - \frac{0.5}{x}}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

      5. metadata-eval 99.9%

         \[\leadsto \frac{\color{blue}{0.5} - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}} \]

   9. Applied egg-rr 99.9%

      \[\leadsto \color{blue}{\frac{0.5 - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 99.6%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{hypot}\left(1, x\right) \leq 2:\\ \;\;\;\;\left(x \cdot x\right) \cdot \left(--0.125\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5 - \frac{0.5}{x}}{1 + \sqrt{0.5 + \frac{0.5}{x}}}\\ \end{array} \]
5. Add Preprocessing

Alternative 4: 98.4% accurate, 1.9× speedup

Math

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;x\_m \leq 1.52:\\ \;\;\;\;\left(x\_m \cdot x\_m\right) \cdot \left(--0.125\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5}{1 + \sqrt{0.5}}\\ \end{array} \end{array} \]

FPCore

x_m = (fabs.f64 x)
(FPCore (x_m)
 :precision binary64
 (if (<= x_m 1.52) (* (* x_m x_m) (- -0.125)) (/ 0.5 (+ 1.0 (sqrt 0.5)))))

C

x_m = fabs(x);
double code(double x_m) {
	double tmp;
	if (x_m <= 1.52) {
		tmp = (x_m * x_m) * -(-0.125);
	} else {
		tmp = 0.5 / (1.0 + sqrt(0.5));
	}
	return tmp;
}

Fortran

x_m = abs(x)
real(8) function code(x_m)
    real(8), intent (in) :: x_m
    real(8) :: tmp
    if (x_m <= 1.52d0) then
        tmp = (x_m * x_m) * -(-0.125d0)
    else
        tmp = 0.5d0 / (1.0d0 + sqrt(0.5d0))
    end if
    code = tmp
end function

Java

x_m = Math.abs(x);
public static double code(double x_m) {
	double tmp;
	if (x_m <= 1.52) {
		tmp = (x_m * x_m) * -(-0.125);
	} else {
		tmp = 0.5 / (1.0 + Math.sqrt(0.5));
	}
	return tmp;
}

Python

x_m = math.fabs(x)
def code(x_m):
	tmp = 0
	if x_m <= 1.52:
		tmp = (x_m * x_m) * -(-0.125)
	else:
		tmp = 0.5 / (1.0 + math.sqrt(0.5))
	return tmp

Julia

x_m = abs(x)
function code(x_m)
	tmp = 0.0
	if (x_m <= 1.52)
		tmp = Float64(Float64(x_m * x_m) * Float64(-(-0.125)));
	else
		tmp = Float64(0.5 / Float64(1.0 + sqrt(0.5)));
	end
	return tmp
end

MATLAB

x_m = abs(x);
function tmp_2 = code(x_m)
	tmp = 0.0;
	if (x_m <= 1.52)
		tmp = (x_m * x_m) * -(-0.125);
	else
		tmp = 0.5 / (1.0 + sqrt(0.5));
	end
	tmp_2 = tmp;
end

Wolfram

x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := If[LessEqual[x$95$m, 1.52], N[(N[(x$95$m * x$95$m), $MachinePrecision] * (--0.125)), $MachinePrecision], N[(0.5 / N[(1.0 + N[Sqrt[0.5], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if x < 1.52

   1. Initial program 67.2%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 67.2%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 67.2%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 67.2%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 67.2%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 67.2%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around 0 33.1%

      \[\leadsto 1 - \color{blue}{\left(1 + -0.125 \cdot {x}^{2}\right)} \]
   6. Step-by-step derivation

      1. *-commutative 33.1%

         \[\leadsto 1 - \left(1 + \color{blue}{{x}^{2} \cdot -0.125}\right) \]

   7. Simplified 33.1%

      \[\leadsto 1 - \color{blue}{\left(1 + {x}^{2} \cdot -0.125\right)} \]
   8. Step-by-step derivation

      1. associate--r+ 65.0%

         \[\leadsto \color{blue}{\left(1 - 1\right) - {x}^{2} \cdot -0.125} \]

      2. metadata-eval 65.0%

         \[\leadsto \color{blue}{0} - {x}^{2} \cdot -0.125 \]

      3. flip-- 19.2%

         \[\leadsto \color{blue}{\frac{0 \cdot 0 - \left({x}^{2} \cdot -0.125\right) \cdot \left({x}^{2} \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125}} \]

      4. metadata-eval 19.2%

         \[\leadsto \frac{\color{blue}{0} - \left({x}^{2} \cdot -0.125\right) \cdot \left({x}^{2} \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      5. swap-sqr 19.2%

         \[\leadsto \frac{0 - \color{blue}{\left({x}^{2} \cdot {x}^{2}\right) \cdot \left(-0.125 \cdot -0.125\right)}}{0 + {x}^{2} \cdot -0.125} \]

      6. pow-prod-up 19.1%

         \[\leadsto \frac{0 - \color{blue}{{x}^{\left(2 + 2\right)}} \cdot \left(-0.125 \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      7. metadata-eval 19.1%

         \[\leadsto \frac{0 - {x}^{\color{blue}{4}} \cdot \left(-0.125 \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      8. metadata-eval 19.1%

         \[\leadsto \frac{0 - {x}^{4} \cdot \color{blue}{0.015625}}{0 + {x}^{2} \cdot -0.125} \]

   9. Applied egg-rr 19.1%

      \[\leadsto \color{blue}{\frac{0 - {x}^{4} \cdot 0.015625}{0 + {x}^{2} \cdot -0.125}} \]
   10. Step-by-step derivation

       1. sub0-neg 19.1%

          \[\leadsto \frac{\color{blue}{-{x}^{4} \cdot 0.015625}}{0 + {x}^{2} \cdot -0.125} \]

       2. +-lft-identity 19.1%

          \[\leadsto \frac{-\color{blue}{\left(0 + {x}^{4} \cdot 0.015625\right)}}{0 + {x}^{2} \cdot -0.125} \]

       3. +-commutative 19.1%

          \[\leadsto \frac{-\color{blue}{\left({x}^{4} \cdot 0.015625 + 0\right)}}{0 + {x}^{2} \cdot -0.125} \]

       4. mul0-lft 19.1%

          \[\leadsto \frac{-\left({x}^{4} \cdot 0.015625 + \color{blue}{0 \cdot \left({x}^{2} \cdot -0.125\right)}\right)}{0 + {x}^{2} \cdot -0.125} \]

       5. +-lft-identity 19.1%

          \[\leadsto \frac{-\color{blue}{\left(0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)\right)}}{0 + {x}^{2} \cdot -0.125} \]

       6. +-lft-identity 19.1%

          \[\leadsto \frac{-\left(0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)\right)}{\color{blue}{{x}^{2} \cdot -0.125}} \]

       7. distribute-frac-neg 19.1%

          \[\leadsto \color{blue}{-\frac{0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)}{{x}^{2} \cdot -0.125}} \]

       8. +-lft-identity 19.1%

          \[\leadsto -\frac{\color{blue}{{x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)}}{{x}^{2} \cdot -0.125} \]

       9. mul0-lft 19.1%

          \[\leadsto -\frac{{x}^{4} \cdot 0.015625 + \color{blue}{0}}{{x}^{2} \cdot -0.125} \]

       10. +-commutative 19.1%

           \[\leadsto -\frac{\color{blue}{0 + {x}^{4} \cdot 0.015625}}{{x}^{2} \cdot -0.125} \]

       11. +-lft-identity 19.1%

           \[\leadsto -\frac{\color{blue}{{x}^{4} \cdot 0.015625}}{{x}^{2} \cdot -0.125} \]

       12. +-lft-identity 19.1%

           \[\leadsto -\frac{{x}^{4} \cdot 0.015625}{\color{blue}{0 + {x}^{2} \cdot -0.125}} \]

       13. *-commutative 19.1%

           \[\leadsto -\frac{\color{blue}{0.015625 \cdot {x}^{4}}}{0 + {x}^{2} \cdot -0.125} \]

       14. +-lft-identity 19.1%

           \[\leadsto -\frac{0.015625 \cdot {x}^{4}}{\color{blue}{{x}^{2} \cdot -0.125}} \]

       15. *-commutative 19.1%

           \[\leadsto -\frac{0.015625 \cdot {x}^{4}}{\color{blue}{-0.125 \cdot {x}^{2}}} \]

       16. times-frac 19.2%

           \[\leadsto -\color{blue}{\frac{0.015625}{-0.125} \cdot \frac{{x}^{4}}{{x}^{2}}} \]

       17. metadata-eval 19.2%

           \[\leadsto -\color{blue}{-0.125} \cdot \frac{{x}^{4}}{{x}^{2}} \]

   11. Simplified 19.2%

       \[\leadsto \color{blue}{--0.125 \cdot \frac{{x}^{4}}{{x}^{2}}} \]
   12. Step-by-step derivation

       1. pow-div 65.0%

          \[\leadsto --0.125 \cdot \color{blue}{{x}^{\left(4 - 2\right)}} \]

       2. metadata-eval 65.0%

          \[\leadsto --0.125 \cdot {x}^{\color{blue}{2}} \]

       3. unpow2 65.0%

          \[\leadsto --0.125 \cdot \color{blue}{\left(x \cdot x\right)} \]

   13. Applied egg-rr 65.0%

       \[\leadsto --0.125 \cdot \color{blue}{\left(x \cdot x\right)} \]

   if 1.52 < x

   1. Initial program 98.5%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 98.5%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing
   5. Step-by-step derivation

      1. flip-- 98.5%

         \[\leadsto \color{blue}{\frac{1 \cdot 1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} \cdot \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}} \]

      2. metadata-eval 98.5%

         \[\leadsto \frac{\color{blue}{1} - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} \cdot \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]

      3. add-sqr-sqrt 100.0%

         \[\leadsto \frac{1 - \color{blue}{\left(0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right)}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. associate--r+ 100.0%

         \[\leadsto \frac{\color{blue}{\left(1 - 0.5\right) - \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]

      5. metadata-eval 100.0%

         \[\leadsto \frac{\color{blue}{0.5} - \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]

   6. Applied egg-rr 100.0%

      \[\leadsto \color{blue}{\frac{0.5 - \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}{1 + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}}} \]

   7. Taylor expanded in x around inf 99.1%

      \[\leadsto \color{blue}{\frac{0.5}{1 + \sqrt{0.5}}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 71.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 1.52:\\ \;\;\;\;\left(x \cdot x\right) \cdot \left(--0.125\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0.5}{1 + \sqrt{0.5}}\\ \end{array} \]
5. Add Preprocessing

Alternative 5: 97.7% accurate, 1.9× speedup

Math

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;x\_m \leq 1.52:\\ \;\;\;\;\left(x\_m \cdot x\_m\right) \cdot \left(--0.125\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \sqrt{0.5}\\ \end{array} \end{array} \]

FPCore

x_m = (fabs.f64 x)
(FPCore (x_m)
 :precision binary64
 (if (<= x_m 1.52) (* (* x_m x_m) (- -0.125)) (- 1.0 (sqrt 0.5))))

C

x_m = fabs(x);
double code(double x_m) {
	double tmp;
	if (x_m <= 1.52) {
		tmp = (x_m * x_m) * -(-0.125);
	} else {
		tmp = 1.0 - sqrt(0.5);
	}
	return tmp;
}

Fortran

x_m = abs(x)
real(8) function code(x_m)
    real(8), intent (in) :: x_m
    real(8) :: tmp
    if (x_m <= 1.52d0) then
        tmp = (x_m * x_m) * -(-0.125d0)
    else
        tmp = 1.0d0 - sqrt(0.5d0)
    end if
    code = tmp
end function

Java

x_m = Math.abs(x);
public static double code(double x_m) {
	double tmp;
	if (x_m <= 1.52) {
		tmp = (x_m * x_m) * -(-0.125);
	} else {
		tmp = 1.0 - Math.sqrt(0.5);
	}
	return tmp;
}

Python

x_m = math.fabs(x)
def code(x_m):
	tmp = 0
	if x_m <= 1.52:
		tmp = (x_m * x_m) * -(-0.125)
	else:
		tmp = 1.0 - math.sqrt(0.5)
	return tmp

Julia

x_m = abs(x)
function code(x_m)
	tmp = 0.0
	if (x_m <= 1.52)
		tmp = Float64(Float64(x_m * x_m) * Float64(-(-0.125)));
	else
		tmp = Float64(1.0 - sqrt(0.5));
	end
	return tmp
end

MATLAB

x_m = abs(x);
function tmp_2 = code(x_m)
	tmp = 0.0;
	if (x_m <= 1.52)
		tmp = (x_m * x_m) * -(-0.125);
	else
		tmp = 1.0 - sqrt(0.5);
	end
	tmp_2 = tmp;
end

Wolfram

x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := If[LessEqual[x$95$m, 1.52], N[(N[(x$95$m * x$95$m), $MachinePrecision] * (--0.125)), $MachinePrecision], N[(1.0 - N[Sqrt[0.5], $MachinePrecision]), $MachinePrecision]]

Derivation

1. Split input into 2 regimes

2. if x < 1.52

   1. Initial program 67.2%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 67.2%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 67.2%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 67.2%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 67.2%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 67.2%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around 0 33.1%

      \[\leadsto 1 - \color{blue}{\left(1 + -0.125 \cdot {x}^{2}\right)} \]
   6. Step-by-step derivation

      1. *-commutative 33.1%

         \[\leadsto 1 - \left(1 + \color{blue}{{x}^{2} \cdot -0.125}\right) \]

   7. Simplified 33.1%

      \[\leadsto 1 - \color{blue}{\left(1 + {x}^{2} \cdot -0.125\right)} \]
   8. Step-by-step derivation

      1. associate--r+ 65.0%

         \[\leadsto \color{blue}{\left(1 - 1\right) - {x}^{2} \cdot -0.125} \]

      2. metadata-eval 65.0%

         \[\leadsto \color{blue}{0} - {x}^{2} \cdot -0.125 \]

      3. flip-- 19.2%

         \[\leadsto \color{blue}{\frac{0 \cdot 0 - \left({x}^{2} \cdot -0.125\right) \cdot \left({x}^{2} \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125}} \]

      4. metadata-eval 19.2%

         \[\leadsto \frac{\color{blue}{0} - \left({x}^{2} \cdot -0.125\right) \cdot \left({x}^{2} \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      5. swap-sqr 19.2%

         \[\leadsto \frac{0 - \color{blue}{\left({x}^{2} \cdot {x}^{2}\right) \cdot \left(-0.125 \cdot -0.125\right)}}{0 + {x}^{2} \cdot -0.125} \]

      6. pow-prod-up 19.1%

         \[\leadsto \frac{0 - \color{blue}{{x}^{\left(2 + 2\right)}} \cdot \left(-0.125 \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      7. metadata-eval 19.1%

         \[\leadsto \frac{0 - {x}^{\color{blue}{4}} \cdot \left(-0.125 \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

      8. metadata-eval 19.1%

         \[\leadsto \frac{0 - {x}^{4} \cdot \color{blue}{0.015625}}{0 + {x}^{2} \cdot -0.125} \]

   9. Applied egg-rr 19.1%

      \[\leadsto \color{blue}{\frac{0 - {x}^{4} \cdot 0.015625}{0 + {x}^{2} \cdot -0.125}} \]
   10. Step-by-step derivation

       1. sub0-neg 19.1%

          \[\leadsto \frac{\color{blue}{-{x}^{4} \cdot 0.015625}}{0 + {x}^{2} \cdot -0.125} \]

       2. +-lft-identity 19.1%

          \[\leadsto \frac{-\color{blue}{\left(0 + {x}^{4} \cdot 0.015625\right)}}{0 + {x}^{2} \cdot -0.125} \]

       3. +-commutative 19.1%

          \[\leadsto \frac{-\color{blue}{\left({x}^{4} \cdot 0.015625 + 0\right)}}{0 + {x}^{2} \cdot -0.125} \]

       4. mul0-lft 19.1%

          \[\leadsto \frac{-\left({x}^{4} \cdot 0.015625 + \color{blue}{0 \cdot \left({x}^{2} \cdot -0.125\right)}\right)}{0 + {x}^{2} \cdot -0.125} \]

       5. +-lft-identity 19.1%

          \[\leadsto \frac{-\color{blue}{\left(0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)\right)}}{0 + {x}^{2} \cdot -0.125} \]

       6. +-lft-identity 19.1%

          \[\leadsto \frac{-\left(0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)\right)}{\color{blue}{{x}^{2} \cdot -0.125}} \]

       7. distribute-frac-neg 19.1%

          \[\leadsto \color{blue}{-\frac{0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)}{{x}^{2} \cdot -0.125}} \]

       8. +-lft-identity 19.1%

          \[\leadsto -\frac{\color{blue}{{x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)}}{{x}^{2} \cdot -0.125} \]

       9. mul0-lft 19.1%

          \[\leadsto -\frac{{x}^{4} \cdot 0.015625 + \color{blue}{0}}{{x}^{2} \cdot -0.125} \]

       10. +-commutative 19.1%

           \[\leadsto -\frac{\color{blue}{0 + {x}^{4} \cdot 0.015625}}{{x}^{2} \cdot -0.125} \]

       11. +-lft-identity 19.1%

           \[\leadsto -\frac{\color{blue}{{x}^{4} \cdot 0.015625}}{{x}^{2} \cdot -0.125} \]

       12. +-lft-identity 19.1%

           \[\leadsto -\frac{{x}^{4} \cdot 0.015625}{\color{blue}{0 + {x}^{2} \cdot -0.125}} \]

       13. *-commutative 19.1%

           \[\leadsto -\frac{\color{blue}{0.015625 \cdot {x}^{4}}}{0 + {x}^{2} \cdot -0.125} \]

       14. +-lft-identity 19.1%

           \[\leadsto -\frac{0.015625 \cdot {x}^{4}}{\color{blue}{{x}^{2} \cdot -0.125}} \]

       15. *-commutative 19.1%

           \[\leadsto -\frac{0.015625 \cdot {x}^{4}}{\color{blue}{-0.125 \cdot {x}^{2}}} \]

       16. times-frac 19.2%

           \[\leadsto -\color{blue}{\frac{0.015625}{-0.125} \cdot \frac{{x}^{4}}{{x}^{2}}} \]

       17. metadata-eval 19.2%

           \[\leadsto -\color{blue}{-0.125} \cdot \frac{{x}^{4}}{{x}^{2}} \]

   11. Simplified 19.2%

       \[\leadsto \color{blue}{--0.125 \cdot \frac{{x}^{4}}{{x}^{2}}} \]
   12. Step-by-step derivation

       1. pow-div 65.0%

          \[\leadsto --0.125 \cdot \color{blue}{{x}^{\left(4 - 2\right)}} \]

       2. metadata-eval 65.0%

          \[\leadsto --0.125 \cdot {x}^{\color{blue}{2}} \]

       3. unpow2 65.0%

          \[\leadsto --0.125 \cdot \color{blue}{\left(x \cdot x\right)} \]

   13. Applied egg-rr 65.0%

       \[\leadsto --0.125 \cdot \color{blue}{\left(x \cdot x\right)} \]

   if 1.52 < x

   1. Initial program 98.5%

      \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
   2. Step-by-step derivation

      1. distribute-lft-in 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

      2. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

      3. associate-*r/ 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

      4. metadata-eval 98.5%

         \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

   3. Simplified 98.5%

      \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
   4. Add Preprocessing

   5. Taylor expanded in x around inf 97.6%

      \[\leadsto \color{blue}{1 - \sqrt{0.5}} \]
3. Recombined 2 regimes into one program.

4. Final simplification 70.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 1.52:\\ \;\;\;\;\left(x \cdot x\right) \cdot \left(--0.125\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \sqrt{0.5}\\ \end{array} \]
5. Add Preprocessing

Alternative 6: 51.9% accurate, 35.0× speedup

Math

\[\begin{array}{l} x_m = \left|x\right| \\ \left(x\_m \cdot x\_m\right) \cdot \left(--0.125\right) \end{array} \]

FPCore

x_m = (fabs.f64 x)
(FPCore (x_m) :precision binary64 (* (* x_m x_m) (- -0.125)))

C

x_m = fabs(x);
double code(double x_m) {
	return (x_m * x_m) * -(-0.125);
}

Fortran

x_m = abs(x)
real(8) function code(x_m)
    real(8), intent (in) :: x_m
    code = (x_m * x_m) * -(-0.125d0)
end function

Java

x_m = Math.abs(x);
public static double code(double x_m) {
	return (x_m * x_m) * -(-0.125);
}

Python

x_m = math.fabs(x)
def code(x_m):
	return (x_m * x_m) * -(-0.125)

Julia

x_m = abs(x)
function code(x_m)
	return Float64(Float64(x_m * x_m) * Float64(-(-0.125)))
end

MATLAB

x_m = abs(x);
function tmp = code(x_m)
	tmp = (x_m * x_m) * -(-0.125);
end

Wolfram

x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := N[(N[(x$95$m * x$95$m), $MachinePrecision] * (--0.125)), $MachinePrecision]

Derivation

1. Initial program 72.7%

   \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \]
2. Step-by-step derivation

   1. distribute-lft-in 72.7%

      \[\leadsto 1 - \sqrt{\color{blue}{0.5 \cdot 1 + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}}} \]

   2. metadata-eval 72.7%

      \[\leadsto 1 - \sqrt{\color{blue}{0.5} + 0.5 \cdot \frac{1}{\mathsf{hypot}\left(1, x\right)}} \]

   3. associate-*r/ 72.7%

      \[\leadsto 1 - \sqrt{0.5 + \color{blue}{\frac{0.5 \cdot 1}{\mathsf{hypot}\left(1, x\right)}}} \]

   4. metadata-eval 72.7%

      \[\leadsto 1 - \sqrt{0.5 + \frac{\color{blue}{0.5}}{\mathsf{hypot}\left(1, x\right)}} \]

3. Simplified 72.7%

   \[\leadsto \color{blue}{1 - \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}} \]
4. Add Preprocessing

5. Taylor expanded in x around 0 28.0%

   \[\leadsto 1 - \color{blue}{\left(1 + -0.125 \cdot {x}^{2}\right)} \]
6. Step-by-step derivation

   1. *-commutative 28.0%

      \[\leadsto 1 - \left(1 + \color{blue}{{x}^{2} \cdot -0.125}\right) \]

7. Simplified 28.0%

   \[\leadsto 1 - \color{blue}{\left(1 + {x}^{2} \cdot -0.125\right)} \]
8. Step-by-step derivation

   1. associate--r+ 54.2%

      \[\leadsto \color{blue}{\left(1 - 1\right) - {x}^{2} \cdot -0.125} \]

   2. metadata-eval 54.2%

      \[\leadsto \color{blue}{0} - {x}^{2} \cdot -0.125 \]

   3. flip-- 16.3%

      \[\leadsto \color{blue}{\frac{0 \cdot 0 - \left({x}^{2} \cdot -0.125\right) \cdot \left({x}^{2} \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125}} \]

   4. metadata-eval 16.3%

      \[\leadsto \frac{\color{blue}{0} - \left({x}^{2} \cdot -0.125\right) \cdot \left({x}^{2} \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

   5. swap-sqr 16.3%

      \[\leadsto \frac{0 - \color{blue}{\left({x}^{2} \cdot {x}^{2}\right) \cdot \left(-0.125 \cdot -0.125\right)}}{0 + {x}^{2} \cdot -0.125} \]

   6. pow-prod-up 16.2%

      \[\leadsto \frac{0 - \color{blue}{{x}^{\left(2 + 2\right)}} \cdot \left(-0.125 \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

   7. metadata-eval 16.2%

      \[\leadsto \frac{0 - {x}^{\color{blue}{4}} \cdot \left(-0.125 \cdot -0.125\right)}{0 + {x}^{2} \cdot -0.125} \]

   8. metadata-eval 16.2%

      \[\leadsto \frac{0 - {x}^{4} \cdot \color{blue}{0.015625}}{0 + {x}^{2} \cdot -0.125} \]

9. Applied egg-rr 16.2%

   \[\leadsto \color{blue}{\frac{0 - {x}^{4} \cdot 0.015625}{0 + {x}^{2} \cdot -0.125}} \]
10. Step-by-step derivation

    1. sub0-neg 16.2%

       \[\leadsto \frac{\color{blue}{-{x}^{4} \cdot 0.015625}}{0 + {x}^{2} \cdot -0.125} \]

    2. +-lft-identity 16.2%

       \[\leadsto \frac{-\color{blue}{\left(0 + {x}^{4} \cdot 0.015625\right)}}{0 + {x}^{2} \cdot -0.125} \]

    3. +-commutative 16.2%

       \[\leadsto \frac{-\color{blue}{\left({x}^{4} \cdot 0.015625 + 0\right)}}{0 + {x}^{2} \cdot -0.125} \]

    4. mul0-lft 16.2%

       \[\leadsto \frac{-\left({x}^{4} \cdot 0.015625 + \color{blue}{0 \cdot \left({x}^{2} \cdot -0.125\right)}\right)}{0 + {x}^{2} \cdot -0.125} \]

    5. +-lft-identity 16.2%

       \[\leadsto \frac{-\color{blue}{\left(0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)\right)}}{0 + {x}^{2} \cdot -0.125} \]

    6. +-lft-identity 16.2%

       \[\leadsto \frac{-\left(0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)\right)}{\color{blue}{{x}^{2} \cdot -0.125}} \]

    7. distribute-frac-neg 16.2%

       \[\leadsto \color{blue}{-\frac{0 + \left({x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)\right)}{{x}^{2} \cdot -0.125}} \]

    8. +-lft-identity 16.2%

       \[\leadsto -\frac{\color{blue}{{x}^{4} \cdot 0.015625 + 0 \cdot \left({x}^{2} \cdot -0.125\right)}}{{x}^{2} \cdot -0.125} \]

    9. mul0-lft 16.2%

       \[\leadsto -\frac{{x}^{4} \cdot 0.015625 + \color{blue}{0}}{{x}^{2} \cdot -0.125} \]

    10. +-commutative 16.2%

        \[\leadsto -\frac{\color{blue}{0 + {x}^{4} \cdot 0.015625}}{{x}^{2} \cdot -0.125} \]

    11. +-lft-identity 16.2%

        \[\leadsto -\frac{\color{blue}{{x}^{4} \cdot 0.015625}}{{x}^{2} \cdot -0.125} \]

    12. +-lft-identity 16.2%

        \[\leadsto -\frac{{x}^{4} \cdot 0.015625}{\color{blue}{0 + {x}^{2} \cdot -0.125}} \]

    13. *-commutative 16.2%

        \[\leadsto -\frac{\color{blue}{0.015625 \cdot {x}^{4}}}{0 + {x}^{2} \cdot -0.125} \]

    14. +-lft-identity 16.2%

        \[\leadsto -\frac{0.015625 \cdot {x}^{4}}{\color{blue}{{x}^{2} \cdot -0.125}} \]

    15. *-commutative 16.2%

        \[\leadsto -\frac{0.015625 \cdot {x}^{4}}{\color{blue}{-0.125 \cdot {x}^{2}}} \]

    16. times-frac 16.2%

        \[\leadsto -\color{blue}{\frac{0.015625}{-0.125} \cdot \frac{{x}^{4}}{{x}^{2}}} \]

    17. metadata-eval 16.2%

        \[\leadsto -\color{blue}{-0.125} \cdot \frac{{x}^{4}}{{x}^{2}} \]

11. Simplified 16.2%

    \[\leadsto \color{blue}{--0.125 \cdot \frac{{x}^{4}}{{x}^{2}}} \]
12. Step-by-step derivation

    1. pow-div 54.2%

       \[\leadsto --0.125 \cdot \color{blue}{{x}^{\left(4 - 2\right)}} \]

    2. metadata-eval 54.2%

       \[\leadsto --0.125 \cdot {x}^{\color{blue}{2}} \]

    3. unpow2 54.2%

       \[\leadsto --0.125 \cdot \color{blue}{\left(x \cdot x\right)} \]

13. Applied egg-rr 54.2%

    \[\leadsto --0.125 \cdot \color{blue}{\left(x \cdot x\right)} \]

14. Final simplification 54.2%

    \[\leadsto \left(x \cdot x\right) \cdot \left(--0.125\right) \]
15. Add Preprocessing

Reproduce

herbie shell --seed 2024071 
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  :precision binary64
  (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))