\programVariables {
  R h;
  R v;
  
  R H;
  R g;
  R c;
}

\problem {
  0<=h & h=H
  & v=0 & g>0 & 1>=c&c>=0   & c=1
 ->
  \[(
      {h'=v,v'=-g,h>=0};
      ((?h=0; v:=-c*v) ++ ?h!=0)
    )*@invariant(2*g*h=2*g*H-v^2 & h>=0
                 & c=1 & g>0)
  \] (0<=h & h<=H)
}