ODE Conditions

The post-condition is an invariant of the ODE iff each of the following two formulas are valid (validity is necessary and sufficient):

  • {{fml.text}}

The ODE safety question is true only if each of the following three formulas are valid (validity is necessary but not sufficient):

  • {{fml.text}}