Average Error: 15.3 → 1.6
Time: 38.3s
Precision: 64
Internal Precision: 1344
$2 \cdot \sin^{-1} \left(\sqrt{{\left(\sin \left(\frac{x - y}{2}\right)\right)}^{2} + \left(\cos x \cdot \cos y\right) \cdot {\left(\sin z\right)}^{2}}\right)$
$2 \cdot \sin^{-1} \left(\sqrt{\left(\left(\left(\cos y \cdot \cos x\right) \cdot {\left(\sin z\right)}^{2} + {\left(\cos \left(\frac{1}{2} \cdot x\right)\right)}^{2} \cdot {\left(\sin \left(y \cdot \frac{1}{2}\right)\right)}^{2}\right) + {\left(\sin \left(\frac{1}{2} \cdot x\right)\right)}^{2} \cdot {\left(\cos \left(y \cdot \frac{1}{2}\right)\right)}^{2}\right) - \left(\left(\left(\sin \left(\frac{1}{2} \cdot x\right) \cdot \cos \left(y \cdot \frac{1}{2}\right)\right) \cdot \sin \left(y \cdot \frac{1}{2}\right)\right) \cdot \cos \left(\frac{1}{2} \cdot x\right)\right) \cdot 2}\right)$

# Try it out

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Initial program 15.3

$2 \cdot \sin^{-1} \left(\sqrt{{\left(\sin \left(\frac{x - y}{2}\right)\right)}^{2} + \left(\cos x \cdot \cos y\right) \cdot {\left(\sin z\right)}^{2}}\right)$
2. Using strategy rm
3. Applied div-sub15.3

$\leadsto 2 \cdot \sin^{-1} \left(\sqrt{{\left(\sin \color{blue}{\left(\frac{x}{2} - \frac{y}{2}\right)}\right)}^{2} + \left(\cos x \cdot \cos y\right) \cdot {\left(\sin z\right)}^{2}}\right)$
4. Applied sin-diff1.6

$\leadsto 2 \cdot \sin^{-1} \left(\sqrt{{\color{blue}{\left(\sin \left(\frac{x}{2}\right) \cdot \cos \left(\frac{y}{2}\right) - \cos \left(\frac{x}{2}\right) \cdot \sin \left(\frac{y}{2}\right)\right)}}^{2} + \left(\cos x \cdot \cos y\right) \cdot {\left(\sin z\right)}^{2}}\right)$
5. Taylor expanded around inf 1.6

$\leadsto 2 \cdot \sin^{-1} \color{blue}{\left(\sqrt{\left({\left(\sin \left(\frac{1}{2} \cdot x\right)\right)}^{2} \cdot {\left(\cos \left(\frac{1}{2} \cdot y\right)\right)}^{2} + \left({\left(\cos \left(\frac{1}{2} \cdot x\right)\right)}^{2} \cdot {\left(\sin \left(\frac{1}{2} \cdot y\right)\right)}^{2} + {\left(\sin z\right)}^{2} \cdot \left(\cos x \cdot \cos y\right)\right)\right) - 2 \cdot \left(\cos \left(\frac{1}{2} \cdot x\right) \cdot \left(\sin \left(\frac{1}{2} \cdot y\right) \cdot \left(\sin \left(\frac{1}{2} \cdot x\right) \cdot \cos \left(\frac{1}{2} \cdot y\right)\right)\right)\right)}\right)}$
6. Final simplification1.6

$\leadsto 2 \cdot \sin^{-1} \left(\sqrt{\left(\left(\left(\cos y \cdot \cos x\right) \cdot {\left(\sin z\right)}^{2} + {\left(\cos \left(\frac{1}{2} \cdot x\right)\right)}^{2} \cdot {\left(\sin \left(y \cdot \frac{1}{2}\right)\right)}^{2}\right) + {\left(\sin \left(\frac{1}{2} \cdot x\right)\right)}^{2} \cdot {\left(\cos \left(y \cdot \frac{1}{2}\right)\right)}^{2}\right) - \left(\left(\left(\sin \left(\frac{1}{2} \cdot x\right) \cdot \cos \left(y \cdot \frac{1}{2}\right)\right) \cdot \sin \left(y \cdot \frac{1}{2}\right)\right) \cdot \cos \left(\frac{1}{2} \cdot x\right)\right) \cdot 2}\right)$

# Runtime

Time bar (total: 38.3s)Debug log

herbie shell --seed '#(2775764126 3555076145 3898259844 1891440260 2599947619 1948460636)'
(FPCore (x y z)
:name "2 * asin(sqrt(sin((x - y)/2)^2 + cos(x)*cos(y)*sin(z)^2))"
(* 2 (asin (sqrt (+ (pow (sin (/ (- x y) 2)) 2) (* (* (cos x) (cos y)) (pow (sin z) 2)))))))