Toniolo and Linder, Equation (3b), real

Percentage Accurate: 94.0% → 99.7%
Time: 25.5s
Alternatives: 20
Speedup: TODO×

Specification

?
\[\begin{array}{l} t_1 := \sin ky\\ \frac{t_1}{\sqrt{{\sin kx}^{2} + {t_1}^{2}}} \cdot \sin th \end{array} \]

Your Program's Arguments

Results

Enter valid numbers for all inputs

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 20 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Alternative 1?

\[\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}} \]
Derivation
  1. Initial program 93.9%

    \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
  2. Step-by-step derivation
    1. +-commutative93.9%

      \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
    2. unpow293.9%

      \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
    3. unpow293.9%

      \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
    4. hypot-def99.7%

      \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
  3. Simplified99.7%

    \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
  4. Step-by-step derivation
    1. *-commutative99.7%

      \[\leadsto \color{blue}{\sin th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    2. clear-num99.6%

      \[\leadsto \sin th \cdot \color{blue}{\frac{1}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    3. un-div-inv99.7%

      \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
  5. Applied egg-rr99.7%

    \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
  6. Final simplification99.7%

    \[\leadsto \frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}} \]

Alternative 2?

\[\begin{array}{l} t_1 := \sin th \cdot \left|\frac{\sin ky}{\sin kx}\right|\\ \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -1 \cdot 10^{-212}:\\ \;\;\;\;\frac{\sin th \cdot ky}{\sin kx}\\ \mathbf{elif}\;\sin ky \leq -2 \cdot 10^{-277}:\\ \;\;\;\;\sin th \cdot \frac{\left|\sin ky\right|}{\sin kx}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-89}:\\ \;\;\;\;\frac{\sin th}{1 + \frac{0.5 \cdot \left(kx \cdot kx\right)}{{\sin ky}^{2}}}\\ \mathbf{elif}\;\sin ky \leq 0.05:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 6 regimes
  2. if (sin.f64 ky) < -1.99999999999999985e-104

    1. Initial program 99.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.7%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/99.6%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.8%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.8%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod17.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg17.8%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod21.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt56.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr56.5%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative56.5%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*56.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses56.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified56.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -1.99999999999999985e-104 < (sin.f64 ky) < -9.99999999999999954e-213

    1. Initial program 81.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative81.6%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow281.6%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow281.6%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 60.4%

      \[\leadsto \color{blue}{\frac{\sin th \cdot ky}{\sin kx}} \]

    if -9.99999999999999954e-213 < (sin.f64 ky) < -1.99999999999999994e-277

    1. Initial program 64.5%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative64.5%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow264.5%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow264.5%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 22.2%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sin kx}} \cdot \sin th \]
    5. Step-by-step derivation
      1. add-sqr-sqrt0.0%

        \[\leadsto \frac{\color{blue}{\sqrt{\sin ky} \cdot \sqrt{\sin ky}}}{\sin kx} \cdot \sin th \]
      2. sqrt-prod5.4%

        \[\leadsto \frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky}}}{\sin kx} \cdot \sin th \]
      3. rem-sqrt-square73.2%

        \[\leadsto \frac{\color{blue}{\left|\sin ky\right|}}{\sin kx} \cdot \sin th \]
    6. Applied egg-rr73.2%

      \[\leadsto \frac{\color{blue}{\left|\sin ky\right|}}{\sin kx} \cdot \sin th \]

    if -1.99999999999999994e-277 < (sin.f64 ky) < 2.00000000000000011e-128 or 2.00000000000000008e-89 < (sin.f64 ky) < 0.050000000000000003

    1. Initial program 87.3%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative87.3%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow287.3%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow287.3%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 57.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sin kx}} \cdot \sin th \]
    5. Step-by-step derivation
      1. add-sqr-sqrt49.9%

        \[\leadsto \color{blue}{\left(\sqrt{\frac{\sin ky}{\sin kx}} \cdot \sqrt{\frac{\sin ky}{\sin kx}}\right)} \cdot \sin th \]
      2. sqrt-unprod68.3%

        \[\leadsto \color{blue}{\sqrt{\frac{\sin ky}{\sin kx} \cdot \frac{\sin ky}{\sin kx}}} \cdot \sin th \]
      3. pow268.3%

        \[\leadsto \sqrt{\color{blue}{{\left(\frac{\sin ky}{\sin kx}\right)}^{2}}} \cdot \sin th \]
    6. Applied egg-rr68.3%

      \[\leadsto \color{blue}{\sqrt{{\left(\frac{\sin ky}{\sin kx}\right)}^{2}}} \cdot \sin th \]
    7. Step-by-step derivation
      1. unpow268.3%

        \[\leadsto \sqrt{\color{blue}{\frac{\sin ky}{\sin kx} \cdot \frac{\sin ky}{\sin kx}}} \cdot \sin th \]
      2. rem-sqrt-square85.5%

        \[\leadsto \color{blue}{\left|\frac{\sin ky}{\sin kx}\right|} \cdot \sin th \]
    8. Simplified85.5%

      \[\leadsto \color{blue}{\left|\frac{\sin ky}{\sin kx}\right|} \cdot \sin th \]

    if 2.00000000000000011e-128 < (sin.f64 ky) < 2.00000000000000008e-89

    1. Initial program 100.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative100.0%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow2100.0%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow2100.0%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def100.0%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \color{blue}{\sin th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
      2. clear-num100.0%

        \[\leadsto \sin th \cdot \color{blue}{\frac{1}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      3. un-div-inv100.0%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    5. Applied egg-rr100.0%

      \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    6. Taylor expanded in kx around 0 87.2%

      \[\leadsto \frac{\sin th}{\color{blue}{1 + 0.5 \cdot \frac{{kx}^{2}}{{\sin ky}^{2}}}} \]
    7. Step-by-step derivation
      1. associate-*r/87.2%

        \[\leadsto \frac{\sin th}{1 + \color{blue}{\frac{0.5 \cdot {kx}^{2}}{{\sin ky}^{2}}}} \]
      2. unpow287.2%

        \[\leadsto \frac{\sin th}{1 + \frac{0.5 \cdot \color{blue}{\left(kx \cdot kx\right)}}{{\sin ky}^{2}}} \]
    8. Simplified87.2%

      \[\leadsto \frac{\sin th}{\color{blue}{1 + \frac{0.5 \cdot \left(kx \cdot kx\right)}{{\sin ky}^{2}}}} \]

    if 0.050000000000000003 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 66.8%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 6 regimes into one program.
  4. Final simplification67.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -1 \cdot 10^{-212}:\\ \;\;\;\;\frac{\sin th \cdot ky}{\sin kx}\\ \mathbf{elif}\;\sin ky \leq -2 \cdot 10^{-277}:\\ \;\;\;\;\sin th \cdot \frac{\left|\sin ky\right|}{\sin kx}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\sin th \cdot \left|\frac{\sin ky}{\sin kx}\right|\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-89}:\\ \;\;\;\;\frac{\sin th}{1 + \frac{0.5 \cdot \left(kx \cdot kx\right)}{{\sin ky}^{2}}}\\ \mathbf{elif}\;\sin ky \leq 0.05:\\ \;\;\;\;\sin th \cdot \left|\frac{\sin ky}{\sin kx}\right|\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 3?

\[\begin{array}{l} t_1 := \sin th \cdot \left|\frac{\sin ky}{\sin kx}\right|\\ \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -5 \cdot 10^{-295}:\\ \;\;\;\;\frac{\sin th \cdot ky}{\sin kx}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-89}:\\ \;\;\;\;\frac{\sin th}{1 + \frac{0.5 \cdot \left(kx \cdot kx\right)}{{\sin ky}^{2}}}\\ \mathbf{elif}\;\sin ky \leq 0.05:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 5 regimes
  2. if (sin.f64 ky) < -1.99999999999999985e-104

    1. Initial program 99.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.7%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/99.6%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.8%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.8%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod17.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg17.8%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod21.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt56.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr56.5%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative56.5%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*56.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses56.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified56.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -1.99999999999999985e-104 < (sin.f64 ky) < -5.00000000000000008e-295

    1. Initial program 77.8%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative77.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow277.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow277.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 51.9%

      \[\leadsto \color{blue}{\frac{\sin th \cdot ky}{\sin kx}} \]

    if -5.00000000000000008e-295 < (sin.f64 ky) < 2.00000000000000011e-128 or 2.00000000000000008e-89 < (sin.f64 ky) < 0.050000000000000003

    1. Initial program 86.8%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative86.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow286.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow286.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 55.8%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sin kx}} \cdot \sin th \]
    5. Step-by-step derivation
      1. add-sqr-sqrt52.1%

        \[\leadsto \color{blue}{\left(\sqrt{\frac{\sin ky}{\sin kx}} \cdot \sqrt{\frac{\sin ky}{\sin kx}}\right)} \cdot \sin th \]
      2. sqrt-unprod68.9%

        \[\leadsto \color{blue}{\sqrt{\frac{\sin ky}{\sin kx} \cdot \frac{\sin ky}{\sin kx}}} \cdot \sin th \]
      3. pow268.9%

        \[\leadsto \sqrt{\color{blue}{{\left(\frac{\sin ky}{\sin kx}\right)}^{2}}} \cdot \sin th \]
    6. Applied egg-rr68.9%

      \[\leadsto \color{blue}{\sqrt{{\left(\frac{\sin ky}{\sin kx}\right)}^{2}}} \cdot \sin th \]
    7. Step-by-step derivation
      1. unpow268.9%

        \[\leadsto \sqrt{\color{blue}{\frac{\sin ky}{\sin kx} \cdot \frac{\sin ky}{\sin kx}}} \cdot \sin th \]
      2. rem-sqrt-square86.8%

        \[\leadsto \color{blue}{\left|\frac{\sin ky}{\sin kx}\right|} \cdot \sin th \]
    8. Simplified86.8%

      \[\leadsto \color{blue}{\left|\frac{\sin ky}{\sin kx}\right|} \cdot \sin th \]

    if 2.00000000000000011e-128 < (sin.f64 ky) < 2.00000000000000008e-89

    1. Initial program 100.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative100.0%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow2100.0%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow2100.0%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def100.0%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Step-by-step derivation
      1. *-commutative100.0%

        \[\leadsto \color{blue}{\sin th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
      2. clear-num100.0%

        \[\leadsto \sin th \cdot \color{blue}{\frac{1}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      3. un-div-inv100.0%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    5. Applied egg-rr100.0%

      \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    6. Taylor expanded in kx around 0 87.2%

      \[\leadsto \frac{\sin th}{\color{blue}{1 + 0.5 \cdot \frac{{kx}^{2}}{{\sin ky}^{2}}}} \]
    7. Step-by-step derivation
      1. associate-*r/87.2%

        \[\leadsto \frac{\sin th}{1 + \color{blue}{\frac{0.5 \cdot {kx}^{2}}{{\sin ky}^{2}}}} \]
      2. unpow287.2%

        \[\leadsto \frac{\sin th}{1 + \frac{0.5 \cdot \color{blue}{\left(kx \cdot kx\right)}}{{\sin ky}^{2}}} \]
    8. Simplified87.2%

      \[\leadsto \frac{\sin th}{\color{blue}{1 + \frac{0.5 \cdot \left(kx \cdot kx\right)}{{\sin ky}^{2}}}} \]

    if 0.050000000000000003 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 66.8%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 5 regimes into one program.
  4. Final simplification65.5%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -5 \cdot 10^{-295}:\\ \;\;\;\;\frac{\sin th \cdot ky}{\sin kx}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\sin th \cdot \left|\frac{\sin ky}{\sin kx}\right|\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-89}:\\ \;\;\;\;\frac{\sin th}{1 + \frac{0.5 \cdot \left(kx \cdot kx\right)}{{\sin ky}^{2}}}\\ \mathbf{elif}\;\sin ky \leq 0.05:\\ \;\;\;\;\sin th \cdot \left|\frac{\sin ky}{\sin kx}\right|\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 4?

\[\begin{array}{l} t_1 := \frac{\sin th \cdot ky}{\sin kx}\\ \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -4 \cdot 10^{-227}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\sin ky \leq 5 \cdot 10^{-223}:\\ \;\;\;\;\left|\sin ky \cdot \frac{\sin th}{\sin kx}\right|\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\sin ky \leq 10^{-44}:\\ \;\;\;\;th \cdot \left(\sin ky \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 5 regimes
  2. if (sin.f64 ky) < -1.99999999999999985e-104

    1. Initial program 99.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.7%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/99.6%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.8%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.8%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod17.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg17.8%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod21.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt56.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr56.5%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative56.5%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*56.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses56.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified56.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -1.99999999999999985e-104 < (sin.f64 ky) < -3.99999999999999978e-227 or 5.00000000000000024e-223 < (sin.f64 ky) < 2.00000000000000011e-128

    1. Initial program 82.4%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative82.4%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow282.4%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow282.4%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 60.5%

      \[\leadsto \color{blue}{\frac{\sin th \cdot ky}{\sin kx}} \]

    if -3.99999999999999978e-227 < (sin.f64 ky) < 5.00000000000000024e-223

    1. Initial program 74.1%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative74.1%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow274.1%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow274.1%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 58.3%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sin kx}} \cdot \sin th \]
    5. Step-by-step derivation
      1. add-sqr-sqrt57.4%

        \[\leadsto \color{blue}{\sqrt{\frac{\sin ky}{\sin kx} \cdot \sin th} \cdot \sqrt{\frac{\sin ky}{\sin kx} \cdot \sin th}} \]
      2. sqrt-unprod47.3%

        \[\leadsto \color{blue}{\sqrt{\left(\frac{\sin ky}{\sin kx} \cdot \sin th\right) \cdot \left(\frac{\sin ky}{\sin kx} \cdot \sin th\right)}} \]
      3. pow247.3%

        \[\leadsto \sqrt{\color{blue}{{\left(\frac{\sin ky}{\sin kx} \cdot \sin th\right)}^{2}}} \]
      4. *-commutative47.3%

        \[\leadsto \sqrt{{\color{blue}{\left(\sin th \cdot \frac{\sin ky}{\sin kx}\right)}}^{2}} \]
    6. Applied egg-rr47.3%

      \[\leadsto \color{blue}{\sqrt{{\left(\sin th \cdot \frac{\sin ky}{\sin kx}\right)}^{2}}} \]
    7. Step-by-step derivation
      1. unpow247.3%

        \[\leadsto \sqrt{\color{blue}{\left(\sin th \cdot \frac{\sin ky}{\sin kx}\right) \cdot \left(\sin th \cdot \frac{\sin ky}{\sin kx}\right)}} \]
      2. rem-sqrt-square83.2%

        \[\leadsto \color{blue}{\left|\sin th \cdot \frac{\sin ky}{\sin kx}\right|} \]
      3. associate-*r/71.2%

        \[\leadsto \left|\color{blue}{\frac{\sin th \cdot \sin ky}{\sin kx}}\right| \]
      4. associate-/l*83.3%

        \[\leadsto \left|\color{blue}{\frac{\sin th}{\frac{\sin kx}{\sin ky}}}\right| \]
      5. associate-/r/83.4%

        \[\leadsto \left|\color{blue}{\frac{\sin th}{\sin kx} \cdot \sin ky}\right| \]
    8. Simplified83.4%

      \[\leadsto \color{blue}{\left|\frac{\sin th}{\sin kx} \cdot \sin ky\right|} \]

    if 2.00000000000000011e-128 < (sin.f64 ky) < 9.99999999999999953e-45

    1. Initial program 99.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.9%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. +-commutative99.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      3. unpow299.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      4. unpow299.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      5. hypot-def99.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.9%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in th around 0 79.4%

      \[\leadsto \frac{\color{blue}{\sin ky \cdot th}}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \]
    5. Taylor expanded in ky around 0 79.4%

      \[\leadsto \frac{\sin ky \cdot th}{\mathsf{hypot}\left(\color{blue}{ky}, \sin kx\right)} \]
    6. Step-by-step derivation
      1. div-inv79.2%

        \[\leadsto \color{blue}{\left(\sin ky \cdot th\right) \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}} \]
      2. *-commutative79.2%

        \[\leadsto \color{blue}{\left(th \cdot \sin ky\right)} \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)} \]
      3. associate-*l*79.5%

        \[\leadsto \color{blue}{th \cdot \left(\sin ky \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}\right)} \]
    7. Applied egg-rr79.5%

      \[\leadsto \color{blue}{th \cdot \left(\sin ky \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}\right)} \]

    if 9.99999999999999953e-45 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 63.4%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 5 regimes into one program.
  4. Final simplification63.5%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -4 \cdot 10^{-227}:\\ \;\;\;\;\frac{\sin th \cdot ky}{\sin kx}\\ \mathbf{elif}\;\sin ky \leq 5 \cdot 10^{-223}:\\ \;\;\;\;\left|\sin ky \cdot \frac{\sin th}{\sin kx}\right|\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\frac{\sin th \cdot ky}{\sin kx}\\ \mathbf{elif}\;\sin ky \leq 10^{-44}:\\ \;\;\;\;th \cdot \left(\sin ky \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 5?

\[\begin{array}{l} t_1 := th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}\\ \mathbf{if}\;\sin ky \leq -0.814:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\sin ky \leq -0.68:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -0.004:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(ky, \sin kx\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 4 regimes
  2. if (sin.f64 ky) < -0.813999999999999946 or -0.680000000000000049 < (sin.f64 ky) < -0.0040000000000000001

    1. Initial program 99.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/99.5%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative99.5%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow299.5%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow299.5%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 65.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/65.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow265.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow265.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def65.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity65.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def65.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow265.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow265.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative65.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow265.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow265.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def65.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified65.7%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Step-by-step derivation
      1. associate-/r/65.8%

        \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot th} \]
      2. hypot-udef65.9%

        \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}} \cdot th \]
      3. +-commutative65.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}} \cdot th \]
      4. hypot-udef65.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot th \]
    8. Applied egg-rr65.8%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot th} \]

    if -0.813999999999999946 < (sin.f64 ky) < -0.680000000000000049

    1. Initial program 100.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/100.0%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow2100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow2100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.3%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.3%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.3%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod24.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg24.3%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod33.0%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt89.2%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr89.2%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative89.2%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*89.4%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg89.4%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses89.4%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval89.4%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified89.4%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -0.0040000000000000001 < (sin.f64 ky) < 1.00000000000000006e-9

    1. Initial program 86.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/85.6%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/86.8%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative86.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow286.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow286.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.5%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in ky around 0 98.7%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\color{blue}{ky}, \sin kx\right)} \]

    if 1.00000000000000006e-9 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 65.3%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 4 regimes into one program.
  4. Final simplification81.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -0.814:\\ \;\;\;\;th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}\\ \mathbf{elif}\;\sin ky \leq -0.68:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -0.004:\\ \;\;\;\;th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(ky, \sin kx\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 6?

\[\begin{array}{l} \mathbf{if}\;\sin ky \leq -0.814:\\ \;\;\;\;\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}\\ \mathbf{elif}\;\sin ky \leq -0.68:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -0.004:\\ \;\;\;\;th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(ky, \sin kx\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 5 regimes
  2. if (sin.f64 ky) < -0.813999999999999946

    1. Initial program 99.5%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/99.3%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative99.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow299.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow299.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.4%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.4%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 70.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/70.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative70.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified70.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Step-by-step derivation
      1. associate-/r/70.8%

        \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot th} \]
      2. hypot-udef70.9%

        \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}} \cdot th \]
      3. +-commutative70.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}} \cdot th \]
      4. hypot-udef70.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot th \]
    8. Applied egg-rr70.8%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot th} \]
    9. Step-by-step derivation
      1. *-commutative70.8%

        \[\leadsto \color{blue}{th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
      2. clear-num70.7%

        \[\leadsto th \cdot \color{blue}{\frac{1}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      3. un-div-inv70.9%

        \[\leadsto \color{blue}{\frac{th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      4. hypot-udef70.8%

        \[\leadsto \frac{th}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{\sin ky}} \]
      5. +-commutative70.8%

        \[\leadsto \frac{th}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}{\sin ky}} \]
      6. hypot-udef70.9%

        \[\leadsto \frac{th}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{\sin ky}} \]
      7. add-sqr-sqrt70.5%

        \[\leadsto \frac{th}{\frac{\color{blue}{\sqrt{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot \sqrt{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}}{\sin ky}} \]
      8. add-sqr-sqrt70.9%

        \[\leadsto \frac{th}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{\sin ky}} \]
    10. Applied egg-rr70.9%

      \[\leadsto \color{blue}{\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}} \]

    if -0.813999999999999946 < (sin.f64 ky) < -0.680000000000000049

    1. Initial program 100.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/100.0%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow2100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow2100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.3%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.3%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.3%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod24.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg24.3%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod33.0%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt89.2%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr89.2%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative89.2%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*89.4%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg89.4%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses89.4%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval89.4%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified89.4%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -0.680000000000000049 < (sin.f64 ky) < -0.0040000000000000001

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/99.6%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative99.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow299.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow299.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 61.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/61.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def61.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity61.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def61.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative61.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def61.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified61.7%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Step-by-step derivation
      1. associate-/r/61.8%

        \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot th} \]
      2. hypot-udef61.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}} \cdot th \]
      3. +-commutative61.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}} \cdot th \]
      4. hypot-udef61.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot th \]
    8. Applied egg-rr61.8%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot th} \]

    if -0.0040000000000000001 < (sin.f64 ky) < 1.00000000000000006e-9

    1. Initial program 86.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/85.6%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/86.8%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative86.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow286.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow286.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.5%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in ky around 0 98.7%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\color{blue}{ky}, \sin kx\right)} \]

    if 1.00000000000000006e-9 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 65.3%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 5 regimes into one program.
  4. Final simplification81.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -0.814:\\ \;\;\;\;\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}\\ \mathbf{elif}\;\sin ky \leq -0.68:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -0.004:\\ \;\;\;\;th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(ky, \sin kx\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 7?

\[\begin{array}{l} \mathbf{if}\;\sin ky \leq -0.814:\\ \;\;\;\;\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}\\ \mathbf{elif}\;\sin ky \leq -0.68:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -0.004:\\ \;\;\;\;th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\frac{\sin th}{\frac{\mathsf{hypot}\left(ky, \sin kx\right)}{\sin ky}}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 5 regimes
  2. if (sin.f64 ky) < -0.813999999999999946

    1. Initial program 99.5%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/99.3%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative99.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow299.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow299.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.4%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.4%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 70.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/70.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative70.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified70.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Step-by-step derivation
      1. associate-/r/70.8%

        \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot th} \]
      2. hypot-udef70.9%

        \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}} \cdot th \]
      3. +-commutative70.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}} \cdot th \]
      4. hypot-udef70.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot th \]
    8. Applied egg-rr70.8%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot th} \]
    9. Step-by-step derivation
      1. *-commutative70.8%

        \[\leadsto \color{blue}{th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
      2. clear-num70.7%

        \[\leadsto th \cdot \color{blue}{\frac{1}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      3. un-div-inv70.9%

        \[\leadsto \color{blue}{\frac{th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      4. hypot-udef70.8%

        \[\leadsto \frac{th}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{\sin ky}} \]
      5. +-commutative70.8%

        \[\leadsto \frac{th}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}{\sin ky}} \]
      6. hypot-udef70.9%

        \[\leadsto \frac{th}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{\sin ky}} \]
      7. add-sqr-sqrt70.5%

        \[\leadsto \frac{th}{\frac{\color{blue}{\sqrt{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot \sqrt{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}}{\sin ky}} \]
      8. add-sqr-sqrt70.9%

        \[\leadsto \frac{th}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{\sin ky}} \]
    10. Applied egg-rr70.9%

      \[\leadsto \color{blue}{\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}} \]

    if -0.813999999999999946 < (sin.f64 ky) < -0.680000000000000049

    1. Initial program 100.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/100.0%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow2100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow2100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.3%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.3%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.3%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod24.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg24.3%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod33.0%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt89.2%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr89.2%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative89.2%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*89.4%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg89.4%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses89.4%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval89.4%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified89.4%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -0.680000000000000049 < (sin.f64 ky) < -0.0040000000000000001

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/99.6%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative99.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow299.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow299.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 61.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/61.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def61.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity61.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def61.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative61.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow261.7%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def61.7%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified61.7%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Step-by-step derivation
      1. associate-/r/61.8%

        \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot th} \]
      2. hypot-udef61.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}} \cdot th \]
      3. +-commutative61.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}} \cdot th \]
      4. hypot-udef61.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot th \]
    8. Applied egg-rr61.8%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot th} \]

    if -0.0040000000000000001 < (sin.f64 ky) < 1.00000000000000006e-9

    1. Initial program 86.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative86.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow286.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow286.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \color{blue}{\sin th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
      2. clear-num99.6%

        \[\leadsto \sin th \cdot \color{blue}{\frac{1}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      3. un-div-inv99.7%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    5. Applied egg-rr99.7%

      \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    6. Taylor expanded in ky around 0 98.9%

      \[\leadsto \frac{\sin th}{\frac{\mathsf{hypot}\left(\color{blue}{ky}, \sin kx\right)}{\sin ky}} \]

    if 1.00000000000000006e-9 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 65.3%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 5 regimes into one program.
  4. Final simplification81.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -0.814:\\ \;\;\;\;\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}\\ \mathbf{elif}\;\sin ky \leq -0.68:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -0.004:\\ \;\;\;\;th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\frac{\sin th}{\frac{\mathsf{hypot}\left(ky, \sin kx\right)}{\sin ky}}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 8?

\[\begin{array}{l} \mathbf{if}\;\sin ky \leq -0.814:\\ \;\;\;\;\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}\\ \mathbf{elif}\;\sin ky \leq -0.68:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -0.004:\\ \;\;\;\;\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \left(\frac{1}{th} + th \cdot 0.16666666666666666\right)}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\frac{\sin th}{\frac{\mathsf{hypot}\left(ky, \sin kx\right)}{\sin ky}}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 5 regimes
  2. if (sin.f64 ky) < -0.813999999999999946

    1. Initial program 99.5%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/99.3%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative99.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow299.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow299.3%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.4%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.4%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 70.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/70.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative70.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow270.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def70.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified70.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Step-by-step derivation
      1. associate-/r/70.8%

        \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot th} \]
      2. hypot-udef70.9%

        \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}} \cdot th \]
      3. +-commutative70.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}} \cdot th \]
      4. hypot-udef70.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot th \]
    8. Applied egg-rr70.8%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot th} \]
    9. Step-by-step derivation
      1. *-commutative70.8%

        \[\leadsto \color{blue}{th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
      2. clear-num70.7%

        \[\leadsto th \cdot \color{blue}{\frac{1}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      3. un-div-inv70.9%

        \[\leadsto \color{blue}{\frac{th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      4. hypot-udef70.8%

        \[\leadsto \frac{th}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{\sin ky}} \]
      5. +-commutative70.8%

        \[\leadsto \frac{th}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx + \sin ky \cdot \sin ky}}}{\sin ky}} \]
      6. hypot-udef70.9%

        \[\leadsto \frac{th}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{\sin ky}} \]
      7. add-sqr-sqrt70.5%

        \[\leadsto \frac{th}{\frac{\color{blue}{\sqrt{\mathsf{hypot}\left(\sin kx, \sin ky\right)} \cdot \sqrt{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}}{\sin ky}} \]
      8. add-sqr-sqrt70.9%

        \[\leadsto \frac{th}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{\sin ky}} \]
    10. Applied egg-rr70.9%

      \[\leadsto \color{blue}{\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}} \]

    if -0.813999999999999946 < (sin.f64 ky) < -0.680000000000000049

    1. Initial program 100.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/100.0%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow2100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow2100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def100.0%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified100.0%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.3%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.3%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.3%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod24.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg24.3%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod33.0%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt89.2%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr89.2%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative89.2%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*89.4%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg89.4%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses89.4%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval89.4%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified89.4%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -0.680000000000000049 < (sin.f64 ky) < -0.0040000000000000001

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/99.6%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative99.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow299.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow299.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Step-by-step derivation
      1. div-inv99.4%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \frac{1}{\sin th}}} \]
    5. Applied egg-rr99.4%

      \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \frac{1}{\sin th}}} \]
    6. Taylor expanded in th around 0 61.8%

      \[\leadsto \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \color{blue}{\left(\frac{1}{th} + 0.16666666666666666 \cdot th\right)}} \]
    7. Step-by-step derivation
      1. *-commutative61.8%

        \[\leadsto \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \left(\frac{1}{th} + \color{blue}{th \cdot 0.16666666666666666}\right)} \]
    8. Simplified61.8%

      \[\leadsto \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \color{blue}{\left(\frac{1}{th} + th \cdot 0.16666666666666666\right)}} \]

    if -0.0040000000000000001 < (sin.f64 ky) < 1.00000000000000006e-9

    1. Initial program 86.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative86.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow286.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow286.9%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Step-by-step derivation
      1. *-commutative99.6%

        \[\leadsto \color{blue}{\sin th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
      2. clear-num99.6%

        \[\leadsto \sin th \cdot \color{blue}{\frac{1}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
      3. un-div-inv99.7%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    5. Applied egg-rr99.7%

      \[\leadsto \color{blue}{\frac{\sin th}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin ky}}} \]
    6. Taylor expanded in ky around 0 98.9%

      \[\leadsto \frac{\sin th}{\frac{\mathsf{hypot}\left(\color{blue}{ky}, \sin kx\right)}{\sin ky}} \]

    if 1.00000000000000006e-9 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 65.3%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 5 regimes into one program.
  4. Final simplification81.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -0.814:\\ \;\;\;\;\frac{th}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{\sin ky}}\\ \mathbf{elif}\;\sin ky \leq -0.68:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq -0.004:\\ \;\;\;\;\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right) \cdot \left(\frac{1}{th} + th \cdot 0.16666666666666666\right)}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\frac{\sin th}{\frac{\mathsf{hypot}\left(ky, \sin kx\right)}{\sin ky}}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 9?

\[\begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\frac{\sin th}{\frac{\sin kx}{ky}}\\ \mathbf{elif}\;\sin ky \leq 10^{-44}:\\ \;\;\;\;th \cdot \left(\sin ky \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 4 regimes
  2. if (sin.f64 ky) < -1.99999999999999985e-104

    1. Initial program 99.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.7%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/99.6%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.8%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.8%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod17.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg17.8%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod21.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt56.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr56.5%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative56.5%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*56.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses56.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified56.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -1.99999999999999985e-104 < (sin.f64 ky) < 2.00000000000000011e-128

    1. Initial program 79.8%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative79.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow279.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow279.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 58.7%

      \[\leadsto \color{blue}{\frac{\sin th \cdot ky}{\sin kx}} \]
    5. Step-by-step derivation
      1. associate-/l*59.7%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{\sin kx}{ky}}} \]
    6. Simplified59.7%

      \[\leadsto \color{blue}{\frac{\sin th}{\frac{\sin kx}{ky}}} \]

    if 2.00000000000000011e-128 < (sin.f64 ky) < 9.99999999999999953e-45

    1. Initial program 99.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.9%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. +-commutative99.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      3. unpow299.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      4. unpow299.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      5. hypot-def99.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.9%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in th around 0 79.4%

      \[\leadsto \frac{\color{blue}{\sin ky \cdot th}}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \]
    5. Taylor expanded in ky around 0 79.4%

      \[\leadsto \frac{\sin ky \cdot th}{\mathsf{hypot}\left(\color{blue}{ky}, \sin kx\right)} \]
    6. Step-by-step derivation
      1. div-inv79.2%

        \[\leadsto \color{blue}{\left(\sin ky \cdot th\right) \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}} \]
      2. *-commutative79.2%

        \[\leadsto \color{blue}{\left(th \cdot \sin ky\right)} \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)} \]
      3. associate-*l*79.5%

        \[\leadsto \color{blue}{th \cdot \left(\sin ky \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}\right)} \]
    7. Applied egg-rr79.5%

      \[\leadsto \color{blue}{th \cdot \left(\sin ky \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}\right)} \]

    if 9.99999999999999953e-45 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 63.4%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 4 regimes into one program.
  4. Final simplification61.2%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\frac{\sin th}{\frac{\sin kx}{ky}}\\ \mathbf{elif}\;\sin ky \leq 10^{-44}:\\ \;\;\;\;th \cdot \left(\sin ky \cdot \frac{1}{\mathsf{hypot}\left(ky, \sin kx\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 10?

\[\begin{array}{l} \mathbf{if}\;\sin ky \leq -0.001:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(ky, \sin kx\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if (sin.f64 ky) < -1e-3

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.7%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/99.6%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.9%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.9%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.9%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.9%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod18.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg18.5%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod20.7%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt58.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr58.5%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative58.5%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*58.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg58.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses58.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval58.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified58.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -1e-3 < (sin.f64 ky) < 1.00000000000000006e-9

    1. Initial program 86.8%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/85.5%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/86.7%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative86.7%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow286.7%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow286.7%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.5%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in ky around 0 99.5%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\color{blue}{ky}, \sin kx\right)} \]

    if 1.00000000000000006e-9 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 65.3%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification78.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -0.001:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 10^{-9}:\\ \;\;\;\;\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(ky, \sin kx\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 11?

\[\begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\frac{\sin th}{\frac{\sin kx}{ky}}\\ \mathbf{elif}\;\sin ky \leq 10^{-44}:\\ \;\;\;\;\frac{th \cdot ky}{\mathsf{hypot}\left(ky, \sin kx\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 4 regimes
  2. if (sin.f64 ky) < -1.99999999999999985e-104

    1. Initial program 99.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.7%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/99.6%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.8%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.8%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod17.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg17.8%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod21.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt56.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr56.5%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative56.5%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*56.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses56.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified56.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -1.99999999999999985e-104 < (sin.f64 ky) < 2.00000000000000011e-128

    1. Initial program 79.8%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative79.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow279.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow279.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 58.7%

      \[\leadsto \color{blue}{\frac{\sin th \cdot ky}{\sin kx}} \]
    5. Step-by-step derivation
      1. associate-/l*59.7%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{\sin kx}{ky}}} \]
    6. Simplified59.7%

      \[\leadsto \color{blue}{\frac{\sin th}{\frac{\sin kx}{ky}}} \]

    if 2.00000000000000011e-128 < (sin.f64 ky) < 9.99999999999999953e-45

    1. Initial program 99.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.9%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. +-commutative99.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      3. unpow299.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      4. unpow299.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      5. hypot-def99.9%

        \[\leadsto \frac{\sin ky \cdot \sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.9%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in th around 0 79.4%

      \[\leadsto \frac{\color{blue}{\sin ky \cdot th}}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \]
    5. Taylor expanded in ky around 0 79.4%

      \[\leadsto \frac{\sin ky \cdot th}{\mathsf{hypot}\left(\color{blue}{ky}, \sin kx\right)} \]
    6. Taylor expanded in ky around 0 79.4%

      \[\leadsto \frac{\color{blue}{th \cdot ky}}{\mathsf{hypot}\left(ky, \sin kx\right)} \]

    if 9.99999999999999953e-45 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 63.4%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 4 regimes into one program.
  4. Final simplification61.2%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\frac{\sin th}{\frac{\sin kx}{ky}}\\ \mathbf{elif}\;\sin ky \leq 10^{-44}:\\ \;\;\;\;\frac{th \cdot ky}{\mathsf{hypot}\left(ky, \sin kx\right)}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 12?

\[\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \]
Derivation
  1. Initial program 93.9%

    \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
  2. Step-by-step derivation
    1. associate-*l/93.4%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
    2. associate-*r/93.9%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
    3. +-commutative93.9%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
    4. unpow293.9%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
    5. unpow293.9%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
    6. hypot-def99.6%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
  3. Simplified99.6%

    \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
  4. Final simplification99.6%

    \[\leadsto \sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \]

Alternative 13?

\[\sin th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \]
Derivation
  1. Initial program 93.9%

    \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
  2. Step-by-step derivation
    1. +-commutative93.9%

      \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
    2. unpow293.9%

      \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
    3. unpow293.9%

      \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
    4. hypot-def99.7%

      \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
  3. Simplified99.7%

    \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
  4. Final simplification99.7%

    \[\leadsto \sin th \cdot \frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \]

Alternative 14?

\[\begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\sin th \cdot \frac{ky}{\sin kx}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if (sin.f64 ky) < -1.99999999999999985e-104

    1. Initial program 99.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.7%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/99.6%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.8%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.8%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod17.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg17.8%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod21.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt56.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr56.5%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative56.5%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*56.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses56.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified56.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -1.99999999999999985e-104 < (sin.f64 ky) < 2.00000000000000011e-128

    1. Initial program 79.8%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative79.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow279.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow279.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 59.6%

      \[\leadsto \color{blue}{\frac{ky}{\sin kx}} \cdot \sin th \]

    if 2.00000000000000011e-128 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.8%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 61.0%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification59.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\sin th \cdot \frac{ky}{\sin kx}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 15?

\[\begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\frac{\sin th}{\frac{\sin kx}{ky}}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if (sin.f64 ky) < -1.99999999999999985e-104

    1. Initial program 99.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/99.7%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/99.6%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow299.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.6%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 2.8%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg2.8%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/2.8%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt1.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod17.8%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg17.8%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod21.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt56.5%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr56.5%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative56.5%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*56.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses56.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval56.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified56.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -1.99999999999999985e-104 < (sin.f64 ky) < 2.00000000000000011e-128

    1. Initial program 79.8%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative79.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow279.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow279.8%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in ky around 0 58.7%

      \[\leadsto \color{blue}{\frac{\sin th \cdot ky}{\sin kx}} \]
    5. Step-by-step derivation
      1. associate-/l*59.7%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{\sin kx}{ky}}} \]
    6. Simplified59.7%

      \[\leadsto \color{blue}{\frac{\sin th}{\frac{\sin kx}{ky}}} \]

    if 2.00000000000000011e-128 < (sin.f64 ky)

    1. Initial program 99.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative99.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow299.7%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.8%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.8%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 61.0%

      \[\leadsto \color{blue}{\sin th} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification59.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\sin ky \leq -2 \cdot 10^{-104}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;\sin ky \leq 2 \cdot 10^{-128}:\\ \;\;\;\;\frac{\sin th}{\frac{\sin kx}{ky}}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 16?

\[\begin{array}{l} t_1 := \frac{\sin th}{-1}\\ \mathbf{if}\;ky \leq -2.95 \cdot 10^{+23}:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq -2.2 \cdot 10^{-258}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;ky \leq 8.8 \cdot 10^{-225}:\\ \;\;\;\;th \cdot \frac{ky}{kx}\\ \mathbf{elif}\;ky \leq 9.2 \cdot 10^{+168}:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq 1.6 \cdot 10^{+260}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if ky < -2.94999999999999994e23 or 8.8e-225 < ky < 9.1999999999999997e168 or 1.6e260 < ky

    1. Initial program 97.2%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative97.2%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow297.2%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow297.2%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 36.6%

      \[\leadsto \color{blue}{\sin th} \]

    if -2.94999999999999994e23 < ky < -2.20000000000000015e-258 or 9.1999999999999997e168 < ky < 1.6e260

    1. Initial program 89.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/88.1%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/88.8%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative88.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow288.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow288.8%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.5%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 9.6%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg9.6%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/14.1%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt7.6%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod22.3%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg22.3%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod17.2%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt40.6%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr40.6%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative40.6%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*37.3%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg37.3%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses37.3%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval37.3%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified37.3%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -2.20000000000000015e-258 < ky < 8.8e-225

    1. Initial program 86.5%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/86.5%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative86.5%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow286.5%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow286.5%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.5%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 51.4%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/51.4%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow251.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow251.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def64.4%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity64.4%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def51.4%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow251.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow251.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative51.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow251.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow251.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def64.4%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified64.4%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Taylor expanded in ky around 0 49.1%

      \[\leadsto \color{blue}{\frac{ky \cdot th}{\sin kx}} \]
    8. Step-by-step derivation
      1. associate-/l*55.2%

        \[\leadsto \color{blue}{\frac{ky}{\frac{\sin kx}{th}}} \]
    9. Simplified55.2%

      \[\leadsto \color{blue}{\frac{ky}{\frac{\sin kx}{th}}} \]
    10. Taylor expanded in kx around 0 50.1%

      \[\leadsto \color{blue}{\frac{th \cdot ky}{kx}} \]
    11. Step-by-step derivation
      1. *-commutative50.1%

        \[\leadsto \frac{\color{blue}{ky \cdot th}}{kx} \]
      2. associate-/l*56.2%

        \[\leadsto \color{blue}{\frac{ky}{\frac{kx}{th}}} \]
    12. Simplified56.2%

      \[\leadsto \color{blue}{\frac{ky}{\frac{kx}{th}}} \]
    13. Step-by-step derivation
      1. associate-/r/56.6%

        \[\leadsto \color{blue}{\frac{ky}{kx} \cdot th} \]
    14. Applied egg-rr56.6%

      \[\leadsto \color{blue}{\frac{ky}{kx} \cdot th} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification38.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;ky \leq -2.95 \cdot 10^{+23}:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq -2.2 \cdot 10^{-258}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;ky \leq 8.8 \cdot 10^{-225}:\\ \;\;\;\;th \cdot \frac{ky}{kx}\\ \mathbf{elif}\;ky \leq 9.2 \cdot 10^{+168}:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq 1.6 \cdot 10^{+260}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 17?

\[\begin{array}{l} t_1 := \frac{\sin th}{-1}\\ \mathbf{if}\;ky \leq -2.95 \cdot 10^{+23}:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq -2.1 \cdot 10^{-236}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;ky \leq 8.8 \cdot 10^{-225}:\\ \;\;\;\;\left|ky \cdot \frac{th}{kx}\right|\\ \mathbf{elif}\;ky \leq 9.2 \cdot 10^{+168}:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq 1.6 \cdot 10^{+260}:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 3 regimes
  2. if ky < -2.94999999999999994e23 or 8.8e-225 < ky < 9.1999999999999997e168 or 1.6e260 < ky

    1. Initial program 97.2%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative97.2%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow297.2%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow297.2%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 36.6%

      \[\leadsto \color{blue}{\sin th} \]

    if -2.94999999999999994e23 < ky < -2.09999999999999979e-236 or 9.1999999999999997e168 < ky < 1.6e260

    1. Initial program 91.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-*l/90.1%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      2. associate-*r/90.9%

        \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}} \]
      3. +-commutative90.9%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \]
      4. unpow290.9%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \]
      5. unpow290.9%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \]
      6. hypot-def99.5%

        \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    3. Simplified99.5%

      \[\leadsto \color{blue}{\sin ky \cdot \frac{\sin th}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \]
    4. Taylor expanded in kx around 0 9.8%

      \[\leadsto \sin ky \cdot \frac{\sin th}{\color{blue}{\sin ky}} \]
    5. Step-by-step derivation
      1. frac-2neg9.8%

        \[\leadsto \sin ky \cdot \color{blue}{\frac{-\sin th}{-\sin ky}} \]
      2. associate-*r/14.5%

        \[\leadsto \color{blue}{\frac{\sin ky \cdot \left(-\sin th\right)}{-\sin ky}} \]
      3. add-sqr-sqrt7.7%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{-\sin th} \cdot \sqrt{-\sin th}\right)}}{-\sin ky} \]
      4. sqrt-unprod23.0%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sqrt{\left(-\sin th\right) \cdot \left(-\sin th\right)}}}{-\sin ky} \]
      5. sqr-neg23.0%

        \[\leadsto \frac{\sin ky \cdot \sqrt{\color{blue}{\sin th \cdot \sin th}}}{-\sin ky} \]
      6. sqrt-unprod17.9%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\left(\sqrt{\sin th} \cdot \sqrt{\sin th}\right)}}{-\sin ky} \]
      7. add-sqr-sqrt41.9%

        \[\leadsto \frac{\sin ky \cdot \color{blue}{\sin th}}{-\sin ky} \]
    6. Applied egg-rr41.9%

      \[\leadsto \color{blue}{\frac{\sin ky \cdot \sin th}{-\sin ky}} \]
    7. Step-by-step derivation
      1. *-commutative41.9%

        \[\leadsto \frac{\color{blue}{\sin th \cdot \sin ky}}{-\sin ky} \]
      2. associate-/l*38.5%

        \[\leadsto \color{blue}{\frac{\sin th}{\frac{-\sin ky}{\sin ky}}} \]
      3. distribute-frac-neg38.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-\frac{\sin ky}{\sin ky}}} \]
      4. *-inverses38.5%

        \[\leadsto \frac{\sin th}{-\color{blue}{1}} \]
      5. metadata-eval38.5%

        \[\leadsto \frac{\sin th}{\color{blue}{-1}} \]
    8. Simplified38.5%

      \[\leadsto \color{blue}{\frac{\sin th}{-1}} \]

    if -2.09999999999999979e-236 < ky < 8.8e-225

    1. Initial program 77.9%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/77.9%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative77.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow277.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow277.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.4%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.4%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 43.6%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/43.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow243.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow243.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def59.8%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity59.8%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def43.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow243.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow243.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative43.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow243.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow243.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def59.8%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified59.8%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Taylor expanded in ky around 0 42.2%

      \[\leadsto \color{blue}{\frac{ky \cdot th}{\sin kx}} \]
    8. Step-by-step derivation
      1. associate-/l*47.2%

        \[\leadsto \color{blue}{\frac{ky}{\frac{\sin kx}{th}}} \]
    9. Simplified47.2%

      \[\leadsto \color{blue}{\frac{ky}{\frac{\sin kx}{th}}} \]
    10. Taylor expanded in kx around 0 42.8%

      \[\leadsto \color{blue}{\frac{th \cdot ky}{kx}} \]
    11. Step-by-step derivation
      1. *-commutative42.8%

        \[\leadsto \frac{\color{blue}{ky \cdot th}}{kx} \]
      2. associate-/l*47.8%

        \[\leadsto \color{blue}{\frac{ky}{\frac{kx}{th}}} \]
    12. Simplified47.8%

      \[\leadsto \color{blue}{\frac{ky}{\frac{kx}{th}}} \]
    13. Step-by-step derivation
      1. add-sqr-sqrt46.2%

        \[\leadsto \color{blue}{\sqrt{\frac{ky}{\frac{kx}{th}}} \cdot \sqrt{\frac{ky}{\frac{kx}{th}}}} \]
      2. sqrt-unprod43.2%

        \[\leadsto \color{blue}{\sqrt{\frac{ky}{\frac{kx}{th}} \cdot \frac{ky}{\frac{kx}{th}}}} \]
      3. pow243.2%

        \[\leadsto \sqrt{\color{blue}{{\left(\frac{ky}{\frac{kx}{th}}\right)}^{2}}} \]
      4. div-inv43.2%

        \[\leadsto \sqrt{{\color{blue}{\left(ky \cdot \frac{1}{\frac{kx}{th}}\right)}}^{2}} \]
      5. clear-num43.2%

        \[\leadsto \sqrt{{\left(ky \cdot \color{blue}{\frac{th}{kx}}\right)}^{2}} \]
    14. Applied egg-rr43.2%

      \[\leadsto \color{blue}{\sqrt{{\left(ky \cdot \frac{th}{kx}\right)}^{2}}} \]
    15. Step-by-step derivation
      1. unpow243.2%

        \[\leadsto \sqrt{\color{blue}{\left(ky \cdot \frac{th}{kx}\right) \cdot \left(ky \cdot \frac{th}{kx}\right)}} \]
      2. rem-sqrt-square59.1%

        \[\leadsto \color{blue}{\left|ky \cdot \frac{th}{kx}\right|} \]
    16. Simplified59.1%

      \[\leadsto \color{blue}{\left|ky \cdot \frac{th}{kx}\right|} \]
  3. Recombined 3 regimes into one program.
  4. Final simplification38.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;ky \leq -2.95 \cdot 10^{+23}:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq -2.1 \cdot 10^{-236}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{elif}\;ky \leq 8.8 \cdot 10^{-225}:\\ \;\;\;\;\left|ky \cdot \frac{th}{kx}\right|\\ \mathbf{elif}\;ky \leq 9.2 \cdot 10^{+168}:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq 1.6 \cdot 10^{+260}:\\ \;\;\;\;\frac{\sin th}{-1}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 18?

\[\begin{array}{l} \mathbf{if}\;ky \leq -200:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq 8.8 \cdot 10^{-225}:\\ \;\;\;\;th \cdot \frac{ky}{kx}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if ky < -200 or 8.8e-225 < ky

    1. Initial program 97.6%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. +-commutative97.6%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}} \cdot \sin th \]
      2. unpow297.6%

        \[\leadsto \frac{\sin ky}{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}} \cdot \sin th \]
      3. unpow297.6%

        \[\leadsto \frac{\sin ky}{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}} \cdot \sin th \]
      4. hypot-def99.7%

        \[\leadsto \frac{\sin ky}{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}} \cdot \sin th \]
    3. Simplified99.7%

      \[\leadsto \color{blue}{\frac{\sin ky}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot \sin th} \]
    4. Taylor expanded in kx around 0 34.5%

      \[\leadsto \color{blue}{\sin th} \]

    if -200 < ky < 8.8e-225

    1. Initial program 84.0%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/84.2%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative84.2%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow284.2%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow284.2%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 44.0%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/44.1%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow244.1%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow244.1%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def53.0%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity53.0%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def44.1%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow244.1%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow244.1%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative44.1%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow244.1%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow244.1%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def53.0%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified53.0%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Taylor expanded in ky around 0 27.3%

      \[\leadsto \color{blue}{\frac{ky \cdot th}{\sin kx}} \]
    8. Step-by-step derivation
      1. associate-/l*28.6%

        \[\leadsto \color{blue}{\frac{ky}{\frac{\sin kx}{th}}} \]
    9. Simplified28.6%

      \[\leadsto \color{blue}{\frac{ky}{\frac{\sin kx}{th}}} \]
    10. Taylor expanded in kx around 0 23.8%

      \[\leadsto \color{blue}{\frac{th \cdot ky}{kx}} \]
    11. Step-by-step derivation
      1. *-commutative23.8%

        \[\leadsto \frac{\color{blue}{ky \cdot th}}{kx} \]
      2. associate-/l*25.1%

        \[\leadsto \color{blue}{\frac{ky}{\frac{kx}{th}}} \]
    12. Simplified25.1%

      \[\leadsto \color{blue}{\frac{ky}{\frac{kx}{th}}} \]
    13. Step-by-step derivation
      1. associate-/r/25.1%

        \[\leadsto \color{blue}{\frac{ky}{kx} \cdot th} \]
    14. Applied egg-rr25.1%

      \[\leadsto \color{blue}{\frac{ky}{kx} \cdot th} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification32.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;ky \leq -200:\\ \;\;\;\;\sin th\\ \mathbf{elif}\;ky \leq 8.8 \cdot 10^{-225}:\\ \;\;\;\;th \cdot \frac{ky}{kx}\\ \mathbf{else}:\\ \;\;\;\;\sin th\\ \end{array} \]

Alternative 19?

\[\begin{array}{l} \mathbf{if}\;ky \leq -2.6 \cdot 10^{-46}:\\ \;\;\;\;th\\ \mathbf{elif}\;ky \leq 3.8 \cdot 10^{-228}:\\ \;\;\;\;th \cdot \frac{ky}{kx}\\ \mathbf{else}:\\ \;\;\;\;th\\ \end{array} \]
Derivation
  1. Split input into 2 regimes
  2. if ky < -2.6000000000000002e-46 or 3.7999999999999999e-228 < ky

    1. Initial program 97.7%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/97.6%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative97.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow297.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow297.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 58.5%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/58.6%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow258.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow258.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def60.1%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity60.1%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def58.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow258.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow258.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative58.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow258.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow258.6%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def60.1%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified60.1%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Taylor expanded in kx around 0 22.8%

      \[\leadsto \color{blue}{th} \]

    if -2.6000000000000002e-46 < ky < 3.7999999999999999e-228

    1. Initial program 82.3%

      \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
    2. Step-by-step derivation
      1. associate-/r/82.4%

        \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
      2. +-commutative82.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
      3. unpow282.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
      4. unpow282.4%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
      5. hypot-def99.6%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
    3. Simplified99.6%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
    4. Taylor expanded in th around 0 40.9%

      \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
    5. Step-by-step derivation
      1. associate-*r/40.9%

        \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
      2. unpow240.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
      3. unpow240.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
      4. hypot-def50.9%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
      5. *-rgt-identity50.9%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
      6. hypot-def40.9%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
      7. unpow240.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
      8. unpow240.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
      9. +-commutative40.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
      10. unpow240.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
      11. unpow240.9%

        \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
      12. hypot-def50.9%

        \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
    6. Simplified50.9%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
    7. Taylor expanded in ky around 0 28.6%

      \[\leadsto \color{blue}{\frac{ky \cdot th}{\sin kx}} \]
    8. Step-by-step derivation
      1. associate-/l*30.0%

        \[\leadsto \color{blue}{\frac{ky}{\frac{\sin kx}{th}}} \]
    9. Simplified30.0%

      \[\leadsto \color{blue}{\frac{ky}{\frac{\sin kx}{th}}} \]
    10. Taylor expanded in kx around 0 26.1%

      \[\leadsto \color{blue}{\frac{th \cdot ky}{kx}} \]
    11. Step-by-step derivation
      1. *-commutative26.1%

        \[\leadsto \frac{\color{blue}{ky \cdot th}}{kx} \]
      2. associate-/l*27.5%

        \[\leadsto \color{blue}{\frac{ky}{\frac{kx}{th}}} \]
    12. Simplified27.5%

      \[\leadsto \color{blue}{\frac{ky}{\frac{kx}{th}}} \]
    13. Step-by-step derivation
      1. associate-/r/27.6%

        \[\leadsto \color{blue}{\frac{ky}{kx} \cdot th} \]
    14. Applied egg-rr27.6%

      \[\leadsto \color{blue}{\frac{ky}{kx} \cdot th} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification24.0%

    \[\leadsto \begin{array}{l} \mathbf{if}\;ky \leq -2.6 \cdot 10^{-46}:\\ \;\;\;\;th\\ \mathbf{elif}\;ky \leq 3.8 \cdot 10^{-228}:\\ \;\;\;\;th \cdot \frac{ky}{kx}\\ \mathbf{else}:\\ \;\;\;\;th\\ \end{array} \]

Alternative 20?

\[th \]
Derivation
  1. Initial program 93.9%

    \[\frac{\sin ky}{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}} \cdot \sin th \]
  2. Step-by-step derivation
    1. associate-/r/93.9%

      \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\sqrt{{\sin kx}^{2} + {\sin ky}^{2}}}{\sin th}}} \]
    2. +-commutative93.9%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2} + {\sin kx}^{2}}}}{\sin th}} \]
    3. unpow293.9%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}}}{\sin th}} \]
    4. unpow293.9%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}}}{\sin th}} \]
    5. hypot-def99.6%

      \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{\sin th}} \]
  3. Simplified99.6%

    \[\leadsto \color{blue}{\frac{\sin ky}{\frac{\mathsf{hypot}\left(\sin ky, \sin kx\right)}{\sin th}}} \]
  4. Taylor expanded in th around 0 54.3%

    \[\leadsto \frac{\sin ky}{\color{blue}{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot \frac{1}{th}}} \]
  5. Step-by-step derivation
    1. associate-*r/54.4%

      \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\sqrt{{\sin ky}^{2} + {\sin kx}^{2}} \cdot 1}{th}}} \]
    2. unpow254.4%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin ky \cdot \sin ky} + {\sin kx}^{2}} \cdot 1}{th}} \]
    3. unpow254.4%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin ky \cdot \sin ky + \color{blue}{\sin kx \cdot \sin kx}} \cdot 1}{th}} \]
    4. hypot-def57.9%

      \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)} \cdot 1}{th}} \]
    5. *-rgt-identity57.9%

      \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin ky, \sin kx\right)}}{th}} \]
    6. hypot-def54.4%

      \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\sqrt{\sin ky \cdot \sin ky + \sin kx \cdot \sin kx}}}{th}} \]
    7. unpow254.4%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin ky}^{2}} + \sin kx \cdot \sin kx}}{th}} \]
    8. unpow254.4%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{{\sin ky}^{2} + \color{blue}{{\sin kx}^{2}}}}{th}} \]
    9. +-commutative54.4%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{{\sin kx}^{2} + {\sin ky}^{2}}}}{th}} \]
    10. unpow254.4%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\color{blue}{\sin kx \cdot \sin kx} + {\sin ky}^{2}}}{th}} \]
    11. unpow254.4%

      \[\leadsto \frac{\sin ky}{\frac{\sqrt{\sin kx \cdot \sin kx + \color{blue}{\sin ky \cdot \sin ky}}}{th}} \]
    12. hypot-def57.9%

      \[\leadsto \frac{\sin ky}{\frac{\color{blue}{\mathsf{hypot}\left(\sin kx, \sin ky\right)}}{th}} \]
  6. Simplified57.9%

    \[\leadsto \frac{\sin ky}{\color{blue}{\frac{\mathsf{hypot}\left(\sin kx, \sin ky\right)}{th}}} \]
  7. Taylor expanded in kx around 0 18.2%

    \[\leadsto \color{blue}{th} \]
  8. Final simplification18.2%

    \[\leadsto th \]

Reproduce

?
herbie shell --seed 2023166 
(FPCore (kx ky th)
  :name "Toniolo and Linder, Equation (3b), real"
  :precision binary64
  (* (/ (sin ky) (sqrt (+ (pow (sin kx) 2.0) (pow (sin ky) 2.0)))) (sin th)))