| step |
inference rule |
input |
feed |
output |
step validity (as per SymPy) |
|
1
|
- 0000111299:
declare identity
- number of inputs: 0;
feeds: 0;
outputs: 1
- Eq.~\ref{eq:#1} is an identity.
|
|
|
- 7575859295
\(\vec{ \nabla} \times \vec{ \nabla} \times \vec{E} = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
no validation is available for declarations |
|
2
|
- 0000111935:
replace curl with LeviCevita summation contravariant
- number of inputs: 1;
feeds: 0;
outputs: 1
- Replace curl in Eq.~\ref{eq:#1} with Levi-Cevita contravariant; yields Eq.~\ref{eq:#2}.
|
- 7575859295
\(\vec{ \nabla} \times \vec{ \nabla} \times \vec{E} = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
|
- 7575859300
\(\epsilon^{i,j,k} \hat{x}_i \nabla_j ( \vec{ \nabla} \times \vec{E} )_k = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
recognized infrule but not yet supported |
|
3
|
- 0000111935:
replace curl with LeviCevita summation contravariant
- number of inputs: 1;
feeds: 0;
outputs: 1
- Replace curl in Eq.~\ref{eq:#1} with Levi-Cevita contravariant; yields Eq.~\ref{eq:#2}.
|
- 7575859300
\(\epsilon^{i,j,k} \hat{x}_i \nabla_j ( \vec{ \nabla} \times \vec{E} )_k = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
|
- 7575859302
\(\epsilon^{i,j,k} \epsilon_{n,j,k} \hat{x}_i \nabla_j \nabla^m E^n = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
recognized infrule but not yet supported |
|
4
|
- 0000111299:
declare identity
- number of inputs: 0;
feeds: 0;
outputs: 1
- Eq.~\ref{eq:#1} is an identity.
|
|
|
- 7575859304
\(\epsilon^{i,j,k} \epsilon_{n,j,k} = \delta^{l}_{\ \ j} \delta^{m}_{\ \ k} - \delta^{l}_{\ \ k} \delta^{m}_{\ \ h}\)
|
no validation is available for declarations |
|
5
|
- 0000111634:
substitute RHS of expr 1 into expr 2
- number of inputs: 2;
feeds: 0;
outputs: 1
- Substitute RHS of Eq.~\ref{eq:#1} into Eq.~\ref{eq:#2}; yields Eq.~\ref{eq:#3}.
|
- 7575859302
\(\epsilon^{i,j,k} \epsilon_{n,j,k} \hat{x}_i \nabla_j \nabla^m E^n = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
- 7575859304
\(\epsilon^{i,j,k} \epsilon_{n,j,k} = \delta^{l}_{\ \ j} \delta^{m}_{\ \ k} - \delta^{l}_{\ \ k} \delta^{m}_{\ \ h}\)
|
|
- 7575859306
\(\left( \delta^{l}_{\ \ j} \delta^{m}_{\ \ k} - \delta^{l}_{\ \ k} \delta^{m}_{\ \ h} \right) \hat{x}_i \nabla_j \nabla^m E^n = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
LHS diff is nabla**pdg0007930*nabla_{pdg0001552}*pdg0006238**pdg0001592*pdg0008349*(KroneckerDelta(h, pdg0007930)*KroneckerDelta(pdg0008304, pdg0009690) - KroneckerDelta(pdg0001552, pdg0008304)*KroneckerDelta(pdg0007930, pdg0009690)) + (-pdg0001552 + pdg0009690)**2*(pdg0001552 - pdg0001592)*(pdg0001552 - pdg0007984)*(-pdg0001592 + pdg0009690)*(-pdg0007984 + pdg0009690)/4
RHS diff is nabla**2*pdg0004326*(nabla - 1) - KroneckerDelta(h, pdg0007930)*KroneckerDelta(pdg0008304, pdg0009690) + KroneckerDelta(pdg0001552, pdg0008304)*KroneckerDelta(pdg0007930, pdg0009690) |
|
6
|
- 0000111457:
simplify
- number of inputs: 1;
feeds: 0;
outputs: 1
- Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.
|
- 7575859306
\(\left( \delta^{l}_{\ \ j} \delta^{m}_{\ \ k} - \delta^{l}_{\ \ k} \delta^{m}_{\ \ h} \right) \hat{x}_i \nabla_j \nabla^m E^n = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
|
- 7575859308
\(\left( \delta^{l}_{\ \ j} \delta^{m}_{\ \ k} \hat{x}_i \nabla_j \nabla^m E^n\right)-\left( \delta^{l}_{\ \ k} \delta^{m}_{\ \ h} \hat{x}_i \nabla_j \nabla^m E^n \right) = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
Not evaluated due to missing term in SymPy |
|
7
|
- 0000111457:
simplify
- number of inputs: 1;
feeds: 0;
outputs: 1
- Simplify Eq.~\ref{eq:#1}; yields Eq.~\ref{eq:#2}.
|
- 7575859308
\(\left( \delta^{l}_{\ \ j} \delta^{m}_{\ \ k} \hat{x}_i \nabla_j \nabla^m E^n\right)-\left( \delta^{l}_{\ \ k} \delta^{m}_{\ \ h} \hat{x}_i \nabla_j \nabla^m E^n \right) = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
|
- 7575859310
\(\hat{x}_m \nabla_n \nabla^m E^n - \hat{x}_n \nabla_m \nabla^m E^n = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
Not evaluated due to missing term in SymPy |
|
8
|
- 0000111894:
replace summation notation with vector notation
- number of inputs: 1;
feeds: 0;
outputs: 1
- Replace summation notation in Eq.~\ref{eq:#1} with vector notation; yields Eq.~\ref{eq:#2}.
|
- 7575859310
\(\hat{x}_m \nabla_n \nabla^m E^n - \hat{x}_n \nabla_m \nabla^m E^n = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
|
- 7575859312
\(\vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E}) = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
recognized infrule but not yet supported |
|
9
|
- 0000111345:
claim LHS equals RHS
- number of inputs: 1;
feeds: 0;
outputs: 0
- Thus we see that LHS of Eq.~\ref{eq:#1} is equal to RHS.
|
- 7575859312
\(\vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E}) = \vec{ \nabla}( \vec{ \nabla} \cdot \vec{E} - \nabla^2 \vec{E})\)
|
|
|
Not evaluated due to missing term in SymPy |
