/* REQUIRED INFORMATION:

Statistics can be obtained from Proof -> Show Proof Statistics.

Name: Milda Zizyte & Felix Hutchison
AndrewID: mzizyte; fhutchin
KeYmaera version: 3.6.16
Backends used (Mathematica, Z3, ...): Mathematica
Nodes: 18832
Branches: 2236
Interactive steps: 0
Arithmetic Solver: 47.723
Time: 1077.339s
Proof completes (Y/N): Y

*/

\functions {
R Width;
R Height;
R vel;
}

\programVariables {
R bx;
R by;
R vx;
R vy;

R paddleWidth;
//R Px;
R Py;
//R Ox;
R Oy;
}

/* Prove that the paddles following the ball
keeps the ball in the play screen */

\problem{

/* INITIAL CONDITIONS */
(Width > 0 & Height > 0 & bx > 0 & by > 0 & bx < Width & by < Height & vx^2 + vy^2 = vel^2 & vel > 0 & paddleWidth > 0) /* & Px = 0 & Ox = Width) */
->
\[
  (
    /* CONTROL */
    Py := by;
    Oy := by;
  
    /* PHYSICS EVENTS */
    (
    /* Bounce off the paddles */ 
       if (bx = 0 & by > Py - paddleWidth & 
            by < Py + paddleWidth & vx < 0) then (vx := -vx) fi;
       if (bx = Width & by > Oy - paddleWidth & 
            by < Oy + paddleWidth & vx > 0) then (vx := -vx) fi;
    /* Bounce off the top and bottom walls */
       if (by = 0 & vy < 0) then (vy := -vy) fi;
       if (by = Height & vy > 0) then (vy := -vy) fi
    );

    /* CONTINUOUS DYNAMICS */
    /* Evolution domains correspond to play screen area and the areas
       Directly to the sides. We disregard the areas above and below
       for simplicity, as we proved wall bouncing in (1) */
    ({bx' = vx, by' = vy & bx >= 0 & bx <= Width & by >= 0 & by <= Height} ++
     {bx' = vx, by' = vy & bx <= 0 & by >= 0 & by <= Height} ++
    {bx' = vx, by' = vy & bx >= Width & by >= 0 & by <= Height}))*@invariant(vx^2 + vy^2 = vel^2 & bx >= 0 & bx <= Width & by >= 0 & by <= Height)  /* Loop Invariant */
\]
(bx >= 0 & bx <= Width & by >= 0 & by <= Height) /* Safety Condition */
}
