ArchiveEntry "Recitation 7 Proof - Parachute".
Functions.
R c.
R g.
End.
ProgramVariables.
R v.
End.
Problem.
c > 0 & g > 0 &
v + (g/c)^(1/2) < 0
->
[{v' = c*v^2 - g}]
(v + (g/c)^(1/2)) < 0
End.
Tactic "Recitation 7: Proof 1".
unfold; /* Expand propositional connective*/
/* c()>0 needed for well-definedness of g()/c(), else dG will fail */
dC({`c()>0`}, 1) ; <(
/* N.B. As of this writing dG has a bug that often blows up if you try to
* change the postcondition - to workaround, write out dG as a Bellerophon tactic
* but leave off the fourth argument and then change the postcondition manually */
dG({`y'=-1/2*c()*(v-(g()/c())^(1/2))*y`}, 1); /* */
/* Unlike the dA rule presented in notes, explicitly construct the initial value of y,
* derived by setting y^2*e = -1 and solving for y. */
existsR({`(-1/(v+(g()/c())^(1/2)))^(1/2)`}, 1);
/* Cut in a new invariant that now works because of the new ghost variable */
dC({`y^2*(v+(g()/c())^(1/2))=-1`}, 1) ; <(
dW(1) ; QE({`Mathematica`}), /* New inv -> original post */
dI(1) /* Invariant is inductive */
),
master /* c() > 0 trivial by vacuity axiom V */
)
End.
End.