ArchiveEntry "05: Short Bouncing Ball: single hop" Description "5.4: A Proof of a Short Bouncing Ball single-hop without loop". Definitions /* function symbols cannot change their value */ Real H; /* initial height */ Real g; /* gravity */ Real c; /* damping coefficient */ End. ProgramVariables /* program variables may change their value over time */ Real x, v; /* height and velocity */ End. Problem x>=0 & x=H & v=0 & g>0 & 1>=c&c>=0 -> [ {x'=v,v'=-g} {?x=0; v:=-c*v; ++ ?x>=0;} ] (x>=0 & x<=H) End. Tactic "05: Short Bouncing Ball: single hop: Proof 1" implyR(1) ; composeb(1) ; choiceb(1.1) ; composeb(1.1.0) ; testb(1.1.0) ; testb(1.1.1) ; assignb(1.1.0.1) ; solve(1) ; QE End. Illustration "https://lfcps.org/info/fig-bouncing-ball-dark1ghost.png". End.