Average Error: 8.1 → 8.1
Time: 59.7s
Precision: 64
$\tan^{-1} \left(\frac{\sqrt{1 - \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right)}}{\sqrt{{\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}}}\right)$
$\tan^{-1} \left(\frac{\sqrt{\frac{1}{\frac{1 + \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right)}{1 \cdot 1 - \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right) \cdot \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right)}}}}{\sqrt{\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}}}\right)$
\tan^{-1} \left(\frac{\sqrt{1 - \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right)}}{\sqrt{{\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}}}\right)
\tan^{-1} \left(\frac{\sqrt{\frac{1}{\frac{1 + \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right)}{1 \cdot 1 - \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right) \cdot \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right)}}}}{\sqrt{\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}}}\right)
double f(double deltaLat, double lat1, double lat2, double deltaLon) {
double r9435468 = 1.0;
double r9435469 = deltaLat;
double r9435470 = 2.0;
double r9435471 = r9435469 / r9435470;
double r9435472 = sin(r9435471);
double r9435473 = pow(r9435472, r9435470);
double r9435474 = lat1;
double r9435475 = cos(r9435474);
double r9435476 = lat2;
double r9435477 = cos(r9435476);
double r9435478 = r9435475 * r9435477;
double r9435479 = deltaLon;
double r9435480 = r9435479 / r9435470;
double r9435481 = sin(r9435480);
double r9435482 = pow(r9435481, r9435470);
double r9435483 = r9435478 * r9435482;
double r9435484 = r9435473 + r9435483;
double r9435485 = r9435468 - r9435484;
double r9435486 = sqrt(r9435485);
double r9435487 = sqrt(r9435484);
double r9435488 = r9435486 / r9435487;
double r9435489 = atan(r9435488);
return r9435489;
}


double f(double deltaLat, double lat1, double lat2, double deltaLon) {
double r9435490 = 1.0;
double r9435491 = 1.0;
double r9435492 = lat1;
double r9435493 = cos(r9435492);
double r9435494 = lat2;
double r9435495 = cos(r9435494);
double r9435496 = r9435493 * r9435495;
double r9435497 = deltaLon;
double r9435498 = 2.0;
double r9435499 = r9435497 / r9435498;
double r9435500 = sin(r9435499);
double r9435501 = pow(r9435500, r9435498);
double r9435502 = r9435496 * r9435501;
double r9435503 = deltaLat;
double r9435504 = r9435503 / r9435498;
double r9435505 = sin(r9435504);
double r9435506 = pow(r9435505, r9435498);
double r9435507 = r9435502 + r9435506;
double r9435508 = r9435491 + r9435507;
double r9435509 = r9435491 * r9435491;
double r9435510 = r9435507 * r9435507;
double r9435511 = r9435509 - r9435510;
double r9435512 = r9435508 / r9435511;
double r9435513 = r9435490 / r9435512;
double r9435514 = sqrt(r9435513);
double r9435515 = sqrt(r9435507);
double r9435516 = r9435514 / r9435515;
double r9435517 = atan(r9435516);
return r9435517;
}



# Try it out

Results

 In Out
Enter valid numbers for all inputs

# Derivation

1. Initial program 8.1

$\tan^{-1} \left(\frac{\sqrt{1 - \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right)}}{\sqrt{{\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}}}\right)$
2. Using strategy rm
3. Applied flip--8.1

$\leadsto \tan^{-1} \left(\frac{\sqrt{\color{blue}{\frac{1 \cdot 1 - \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right) \cdot \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right)}{1 + \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right)}}}}{\sqrt{{\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}}}\right)$
4. Using strategy rm
5. Applied clear-num8.1

$\leadsto \tan^{-1} \left(\frac{\sqrt{\color{blue}{\frac{1}{\frac{1 + \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right)}{1 \cdot 1 - \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right) \cdot \left({\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}\right)}}}}}{\sqrt{{\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2} + \left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2}}}\right)$
6. Final simplification8.1

$\leadsto \tan^{-1} \left(\frac{\sqrt{\frac{1}{\frac{1 + \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right)}{1 \cdot 1 - \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right) \cdot \left(\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}\right)}}}}{\sqrt{\left(\cos lat1 \cdot \cos lat2\right) \cdot {\left(\sin \left(\frac{deltaLon}{2}\right)\right)}^{2} + {\left(\sin \left(\frac{deltaLat}{2}\right)\right)}^{2}}}\right)$

# Reproduce

herbie shell --seed 1
(FPCore (deltaLat lat1 lat2 deltaLon)
:name "atan(sqrt(1.0 - (pow(sin(deltaLat / 2.0), 2) + cos(lat1) * cos(lat2) * pow(sin(deltaLon / 2.0), 2))) / sqrt(pow(sin(deltaLat / 2.0), 2) + cos(lat1) * cos(lat2) * pow(sin(deltaLon / 2.0), 2)))"
(atan (/ (sqrt (- 1.0 (+ (pow (sin (/ deltaLat 2.0)) 2.0) (* (* (cos lat1) (cos lat2)) (pow (sin (/ deltaLon 2.0)) 2.0))))) (sqrt (+ (pow (sin (/ deltaLat 2.0)) 2.0) (* (* (cos lat1) (cos lat2)) (pow (sin (/ deltaLon 2.0)) 2.0)))))))