dI proves a formula P to be a differential invariant, i.e., true locally in the direction of the dynamics by reducing it to its differential (P)' after assigning the right-hand side f(x) of the ODE to its left-hand side x'. Rule dI reduces a property of an ODE x'=f(x) to a property of a discrete assignment x':=f(x). The resulting formula [x':=f(x)](P)' is the Lie-derivative of P along the ODE x'=f(x).

See also

Learning resources