Figure 3: The condition for rule G6 should also require that F be a closed set, because the soundness proof requires F to have been reached before leaving the negation or its weak negation where the premise and antecedent apply. Thanks to Andrew Sogokon and Paul Jackson for identifying this bug. The antecedent of the conclusion of rule G6 should also assume \chi. Thanks to Yong Kiam Tan for identifying this bug. The most comprehensive approach to ODE liveness is in:
Yong Kiam Tan and AndrĂ© Platzer. An axiomatic approach to existence and liveness for differential equations. Formal Aspects of Computing. DOI 10.1007/s00165-020-00525-0