Return to navigation page

List of Inference Rules

 Case-insensitive dynamic search of latex as plain text:

The inference rule ID links to a page where you can edit the inference rule

name latex input count feed count output count used in derivation
LHS of expr 1 equals LHS of expr 2 LHS of Eq.~\\ref{eq:#1} is equal to LHS of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 2 0 1
RHS of expr 1 equals RHS of expr 2 RHS of Eq.~\\ref{eq:#1} is equal to RHS of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 2 0 1
X cross both sides by Take cross product of $#1$ and Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 1 1 1
X dot both sides Take inner product of $#1$ with Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 1 1 1
add X to both sides Add $#1$ to both sides of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 1 1 1
add expr 1 to expr 2 Add Eq.~\\ref{eq:#1} to Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#2}. 2 0 1
add zero to LHS Add zero to LHS of Eq.~\\ref{eq:#2}, where $0=#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
add zero to RHS Add zero to RHS of Eq.~\\ref{eq:#2}, where $0=#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
apply divergence Apply divergence to both sides of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
apply function to both sides of expression Apply function $#1$ with argument $#2$ to Eq.~\\ref{eq:#3}; yields Eq.~\\ref{eq:#4} 1 2 1
apply gradient to scalar function Apply gradient to both sides of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
apply operator to bra Apply operator in Eq.~\\ref{eq:#1} to bra; yields Eq.~\\ref{eq:#2}. 1 0 1
apply operator to ket Apply operator in Eq.~\\ref{eq:#1} to ket; yields Eq.~\\ref{eq:#2}. 1 0 1
assume N dimensions Assume $#1$ dimensions; decompose vector to be Eq.~\\ref{eq:#2}. 0 1 1
both sides cross X Take cross product of Eq.~\\ref{eq:#2} and $#1$; yields Eq.~\\ref{eq:#3} 1 1 1
both sides dot X Take inner product of Eq.~\\ref{eq:#2} with $#1$; yields Eq.~\\ref{eq:#3} 1 1 1
boundary condition Boundary condition: Eq.~\\ref{eq:#2} when Eq.~\\ref{eq#1}. 1 0 1
boundary condition for expression A boundary condition for Eq.~\\ref{eq:#1} is Eq.~\\ref{eq:#2} 1 0 1
change five variables in expression Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ and $#9$ to $#10$ in Eq.~\\ref{eq:#11}; yields Eq.~\\ref{eq:#12}. 1 10 1
change four variables in expression Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ in Eq.~\\ref{eq:#9}; yields Eq.~\\ref{eq:#10}. 1 8 1
change six variables in expression Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ and $#7$ to $#8$ and $#9$ to $#10$ and $#11$ to $#12$ in Eq.~\\ref{eq:#13}; yields Eq.~\\ref{eq:#14}. 1 12 1
change three variables in expression Change of variable $#1$ to $#2$ and $#3$ to $#4$ and $#5$ to $#6$ in Eq.~\\ref{eq:#7}; yields Eq.~\\ref{eq:#8}. 1 6 1
change two variables in expression Change variable $#1$ to $#2$ and $#3$ to $#4$ in Eq.~\\ref{eq:#5}; yields Eq.~\\ref{eq:#6}. 1 4 1
change variable X to Y Change variable $#1$ to $#2$ in Eq.~\\ref{eq:#3}; yields Eq.~\\ref{eq:#4}. 1 2 1
claim LHS equals RHS Thus we see that LHS of Eq.~\\ref{eq:#1} is equal to RHS. 1 0 0
claim expr 1 equals expr 2 Thus we see that Eq.~\\ref{eq:#1} is equivalent to Eq.~\\ref{eq:#2}. 2 0 0
combine like terms Combine like terms in Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
conjugate both sides Conjugate both sides of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
conjugate function X Conjugate $#1$ in Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 1 1 1
conjugate transpose both sides Conjugate transpose of both sides of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
declare assumption Eq.~\\ref{eq:#1} is an assumption. 0 0 1
declare final expression Eq.~\\ref{eq:#1} is one of the final equations. 1 0 0
declare guess solution Judicious choice as a guessed solution to Eq.~\\ref{eq:#1} is Eq.~\\ref{eq:#2}, 1 0 1
declare identity Eq.~\\ref{eq:#1} is an identity. 0 0 1
declare initial expression Eq.~\\ref{eq:#1} is an initial equation. 0 0 1
differentiate with respect to Differentiate Eq.~\\ref{eq:#2} with respect to $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
distribute conjugate to factors Distribute conjugate to factors in Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
distribute conjugate transpose to factors Distribute conjugate transpose to factors in Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
divide both sides by Divide both sides of Eq.~\\ref{eq:#2} by $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
divide expr 1 by expr 2 Divide Eq.~\\ref{eq:#1} by Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 2 0 1
drop non-dominant term Based on the assumption $#1$, drop non-dominant term in Eq.~\\ref{#2}; yeilds Eq.~\\ref{#3} 1 1 1
evaluate definite integral Evaluate definite integral Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
expand LHS Expand the LHS of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
expand RHS Expand the RHS of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
expand integrand Expand integrand of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
expand magnitude to conjugate Expand $#1$ in Eq.~\\ref{eq:#2} with conjugate; yields Eq.~\\ref{eq:#3}. 1 1 1
expr 1 is equivalent to expr 2 under the condition Eq.~\\ref{eq:#1} is equivalent to Eq.~\\ref{eq:#2} under the condition in Eq.~\\ref{eq:#3}. 2 0 1
expr 1 is true under condition expr 2 Eq.~\\ref{eq:#1} is valid when Eq.~\\ref{eq:#2} occurs; yields Eq.~\\ref{eq:#3}. 2 0 1
factor out X Factor $#1$ from Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 1 1 1
factor out X from LHS Factor $#1$ from the LHS of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 1 1 1
factor out X from RHS Factor $#1$ from the RHS of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 1 1 1
function is even $#1$ is even with respect to $#2$, so replace $#1$ with $#3$ in Eq.~\\ref{eq:#4}; yields Eq.~\\ref{eq:#5}. 1 3 1
function is odd $#1$ is odd with respect to $#2$, so replace $#1$ with $#3$ in Eq.~\\ref{eq:#4}; yields Eq.~\\ref{eq:#5}. 1 3 1
indefinite integral over Indefinite integral of both sides of Eq.~\\ref{eq:#2} over $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
indefinite integrate LHS over Indefinite integral of LHS of Eq.~\\ref{eq:#2} over $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
indefinite integrate RHS over Indefinite integral of RHS of Eq.~\\ref{eq:#2} over $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
indefinite integration Indefinite integral of both sides of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
integrate Integrate Eq.~ref{eq:#1}; yields Eq.~ref{eq:#2}. 1 0 1
integrate over from to Integrate Eq.~\\ref{eq:#4} over $#1$ from lower limit $#2$ to upper limit $#3$; yields Eq.~\\ref{eq:#5}. 1 3 1
make expr power Make Eq.~\\ref{eq:#2} the power of $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
maximum of expression The maximum of Eq.~\\ref{eq:#2} with respect to $#1$ is Eq.~\\ref{eq:#3} 1 1 1
multiply LHS by unity Multiply LHS of Eq.~\\ref{eq:#2} by 1, which in this case is $#1$; yields Eq.~\\ref{eq:#3} 1 1 1
multiply RHS by unity Multiply RHS of Eq.~\\ref{eq:#2} by 1, which in this case is $#1$; yields Eq.~\\ref{eq:#3} 1 1 1
multiply both sides by Multiply both sides of Eq.~\\ref{eq:#2} by $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
multiply expr 1 by expr 2 Multiply Eq.~\\ref{eq:#1} by Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 2 0 1
normalization condition Normalization condition is Eq.~\\ref{eq:#1}. 0 0 1
partially differentiate with respect to Partially differentiate Eq.~\\ref{eq:#2} with respect to $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
raise both sides to power Raise both sides of Eq.~\\ref{eq:#2} to $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
replace constant with value Replace constant $#1$ with value $#2$ and units $#3$ in Eq.~\\ref{eq:#4}; yields Eq.~\\ref{eq:#5} 1 3 1
replace curl with LeviCevita summation contravariant Replace curl in Eq.~\\ref{eq:#1} with Levi-Cevita contravariant; yields Eq.~\\ref{eq:#2}. 1 0 1
replace scalar with vector Replace scalar variables in Eq.~\\ref{eq:#1} with equivalent vector variables; yields Eq.~\\ref{eq:#2}. 1 0 1
replace summation notation with vector notation Replace summation notation in Eq.~\\ref{eq:#1} with vector notation; yields Eq.~\\ref{eq:#2}. 1 0 1
select imaginary parts Select imaginary parts of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
select real parts Select real parts of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
separate three vector components Separate three vector components in Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2} and Eq.~\\ref{eq:#3} and Eq.~\\ref{eq:#4}. 1 0 3
separate two vector components Separate two vector components in Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2} and Eq.~\\ref{eq:#3} 1 0 2
separate vector into two trigonometric ratios Separate vector in Eq.~\\ref{eq:#2} into components related by angle $#1$; yields Eq.~\\ref{eq:#3} and Eq.~\\ref{eq:#4}. 1 1 2
simplify Simplify Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
solve for X Solve Eq.~\\ref{eq:#2} for $#1$; yields Eq.~\\ref{eq:#3}. 1 1 1
square root both sides Take the square root of both sides of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2} and Eq.~\\ref{eq:#3}. 1 0 2
substitute LHS of expr 1 into expr 2 Substitute LHS of Eq.~\\ref{eq:#1} into Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 2 0 1
substitute LHS of five expressions into expression Substitute LHS of Eq.~\\ref{eq:#1} and LHS of Eq.~\\ref{eq:#2} and LHS of Eq.~\\ref{eq:#3} and LHS of Eq.~\\ref{eq:#4} and LHS of Eq.~\\ref{eq:#5} into Eq.~\\ref{eq:#6}; yields Eq.~\\ref{eq:#7}. 6 0 1
substitute LHS of four expressions into expression Substitute LHS of Eq.~\\ref{eq:#1} and LHS of Eq.~\\ref{eq:#2} and LHS of Eq.~\\ref{eq:#3} and LHS of Eq.~\\ref{eq:#4} into Eq.~\\ref{eq:#5}; yields Eq.~\\ref{eq:#6}. 5 0 1
substitute LHS of six expressions into expression Substitute LHS of Eq.~\\ref{eq:#1} and LHS of Eq.~\\ref{eq:#2} and LHS of Eq.~\\ref{eq:#3} and LHS of Eq.~\\ref{eq:#4} and LHS of Eq.~\\ref{eq:#5} and LHS of Eq.~\\ref{eq:#6} into Eq.~\\ref{eq:#7}; yields Eq.~\\ref{eq:#8}. 7 0 1
substitute LHS of three expressions into expression Substitute LHS of Eq.~\\ref{eq:#1} and LHS of Eq.~\\ref{eq:#2} and LHS of Eq.~\\ref{eq:#3} into Eq.~\\ref{eq:#4}; yields Eq.~\\ref{eq:#5}. 4 0 1
substitute LHS of two expressions into expression Substitute LHS of Eq.~\\ref{eq:#1} and LHS of Eq.~\\ref{eq:#2} into Eq.~\\ref{eq:#3}; yields Eq.~\\ref{eq:#4}. 3 0 1
substitute RHS of expr 1 into expr 2 Substitute RHS of Eq.~\\ref{eq:#1} into Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 2 0 1
subtract X from both sides Subtract $#1$ from both sides of Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#3}. 1 1 1
subtract expr 1 from expr 2 Subtract Eq.~\\ref{eq:#1} from Eq.~\\ref{eq:#2}; yields Eq.~\\ref{eq:#2}. 2 0 1
sum exponents Sum exponents on LHS and RHS of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
sum exponents LHS Sum exponents on LHS of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
sum exponents RHS Sum exponents on RHS of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1
swap LHS with RHS Swap LHS of Eq.~\\ref{eq:#1} with RHS; yields Eq.~\\ref{eq:#2}. 1 0 1
take curl of both sides Apply curl to both sides of Eq.~\\ref{eq:#1}; yields Eq.~\\ref{eq:#2}. 1 0 1

Actions for Inference Rules

add inference rule

timing of Neo4j queries: