| step |
inference rule |
input |
feed |
output |
step validity (as per SymPy) |
|
1
|
- 0000111981:
declare initial expression
- number of inputs: 0;
feeds: 0;
outputs: 1
- Eq.~\ref{eq:#1} is an initial equation.
|
|
|
- 4938429483
\(\exp(i x) = \cos(x)+i \sin(x)\)
|
no validation is available for declarations |
|
2
|
- 0000111886:
change variable X to Y
- number of inputs: 1;
feeds: 2;
outputs: 1
- Change variable $#1$ to $#2$ in Eq.~\ref{eq:#3}; yields Eq.~\ref{eq:#4}.
|
- 4938429483
\(\exp(i x) = \cos(x)+i \sin(x)\)
|
- 0003949052
\(-x\)
- 0002393922
\(x\)
|
- 2394853829
\(\exp(-i x) = \cos(-x)+i \sin(-x)\)
|
LHS diff is 2*sinh(pdg0001464*pdg0004621)
RHS diff is 2*pdg0004621*sin(pdg0001464) |
|
3
|
- 0000111329:
function is even
- number of inputs: 1;
feeds: 3;
outputs: 1
- $#1$ is even with respect to $#2$, so replace $#1$ with $#3$ in Eq.~\ref{eq:#4}; yields Eq.~\ref{eq:#5}.
|
- 2394853829
\(\exp(-i x) = \cos(-x)+i \sin(-x)\)
|
- 0003413423
\(\cos(-x)\)
- 0001030901
\(\cos(x)\)
- 0004849392
\(x\)
|
- 4938429482
\(\exp(-i x) = \cos(x)+i \sin(-x)\)
|
|
|
4
|
- 0000111522:
function is odd
- number of inputs: 1;
feeds: 3;
outputs: 1
- $#1$ is odd with respect to $#2$, so replace $#1$ with $#3$ in Eq.~\ref{eq:#4}; yields Eq.~\ref{eq:#5}.
|
- 4938429482
\(\exp(-i x) = \cos(x)+i \sin(-x)\)
|
- 0002919191
\(\sin(-x)\)
- 0003981813
\(-\sin(x)\)
- 0003919391
\(x\)
|
- 4938429484
\(\exp(-i x) = \cos(x)-i \sin(x)\)
|
|
|
5
|
- 0000111980:
add expr 1 to expr 2
- number of inputs: 2;
feeds: 0;
outputs: 1
- Add Eq.~\ref{eq:#1} to Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#2}.
|
- 4938429484
\(\exp(-i x) = \cos(x)-i \sin(x)\)
- 4938429483
\(\exp(i x) = \cos(x)+i \sin(x)\)
|
|
- 4742644828
\(\exp(i x)+\exp(-i x) = 2 \cos(x)\)
|
valid |
|
6
|
- 0000111975:
divide both sides by
- number of inputs: 1;
feeds: 1;
outputs: 1
- Divide both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.
|
- 4742644828
\(\exp(i x)+\exp(-i x) = 2 \cos(x)\)
|
- 0004829194
\(2\)
|
- 3829492824
\(\frac{1}{2}\left(\exp(i x)+\exp(-i x) \right) = \cos(x)\)
|
valid |
|
7
|
- 0000111268:
swap LHS with RHS
- number of inputs: 1;
feeds: 0;
outputs: 1
- Swap LHS of Eq.~\ref{eq:#1} with RHS; yields Eq.~\ref{eq:#2}.
|
- 3829492824
\(\frac{1}{2}\left(\exp(i x)+\exp(-i x) \right) = \cos(x)\)
|
|
- 4585932229
\(\cos(x) = \frac{1}{2}\left(\exp(i x)+\exp(-i x) \right)\)
|
valid |
|
8
|
- 0000111341:
declare final expression
- number of inputs: 1;
feeds: 0;
outputs: 0
- Eq.~\ref{eq:#1} is one of the final equations.
|
- 2103023049
\(\sin(x) = \frac{1}{2i}\left(\exp(i x)-\exp(-i x) \right)\)
- 4585932229
\(\cos(x) = \frac{1}{2}\left(\exp(i x)+\exp(-i x) \right)\)
|
|
|
no validation is available for declarations |
|
9
|
- 0000111182:
multiply both sides by
- number of inputs: 1;
feeds: 1;
outputs: 1
- Multiply both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.
|
- 4938429484
\(\exp(-i x) = \cos(x)-i \sin(x)\)
|
- 0003747849
\(-1\)
|
- 2123139121
\(-\exp(-i x) = -\cos(x)+i \sin(x)\)
|
valid |
|
10
|
- 0000111980:
add expr 1 to expr 2
- number of inputs: 2;
feeds: 0;
outputs: 1
- Add Eq.~\ref{eq:#1} to Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#2}.
|
- 2123139121
\(-\exp(-i x) = -\cos(x)+i \sin(x)\)
- 4938429483
\(\exp(i x) = \cos(x)+i \sin(x)\)
|
|
- 3942849294
\(\exp(i x)-\exp(-i x) = 2 i \sin(x)\)
|
valid |
|
11
|
- 0000111975:
divide both sides by
- number of inputs: 1;
feeds: 1;
outputs: 1
- Divide both sides of Eq.~\ref{eq:#2} by $#1$; yields Eq.~\ref{eq:#3}.
|
- 3942849294
\(\exp(i x)-\exp(-i x) = 2 i \sin(x)\)
|
- 0001921933
\(2 i\)
|
- 4843995999
\(\frac{1}{2 i}\left(\exp(i x)-\exp(-i x) \right) = \sin(x)\)
|
valid |
|
12
|
- 0000111268:
swap LHS with RHS
- number of inputs: 1;
feeds: 0;
outputs: 1
- Swap LHS of Eq.~\ref{eq:#1} with RHS; yields Eq.~\ref{eq:#2}.
|
- 4843995999
\(\frac{1}{2 i}\left(\exp(i x)-\exp(-i x) \right) = \sin(x)\)
|
|
- 2103023049
\(\sin(x) = \frac{1}{2i}\left(\exp(i x)-\exp(-i x) \right)\)
|
valid |
d3js visualization of steps and expressions in Euler equation: trigonometric relations