/* 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: 13692
Branches: 1223
Interactive steps: 0
Arithmetic Solver: 143.34
Time: 226.524
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 Pvy;
//R Ox;
R Oy;
}

\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 & Py = by) /* & Px = 0 & Ox = Width) */
->
\[
  (
  
    /* WALL PHYSICS EVENTS */
       if (by = 0 & vy < 0) then (vy := -vy)
       else (if (by = Height & vy > 0) then (vy := -vy) fi)
       fi;
       
    /* PADDLE CONTROL */
    /* Player paddle tracks the ball */
    Pvy := vy;
    Oy := by;
    
  
    /* PADDLE PHYSICS EVENTS */    
    if (bx = 0 & by > Py - paddleWidth & 
            by < Py + paddleWidth & vx < 0) then (vx := -vx)
       else (if (bx = Width & by > Oy - paddleWidth & 
            by < Oy + paddleWidth & vx > 0) then (vx := -vx) 
           fi)
        fi;

    /* CONTINUOUS DYNAMICS */
    ({bx' = vx, by' = vy, Py' = Pvy & bx >= 0 & bx <= Width & by >= 0 & by <= Height} ++
     {bx' = vx, by' = vy, Py' = Pvy & bx <= 0 & by >= 0 & by <= Height} ++
    {bx' = vx, by' = vy, Py' = Pvy & bx >= Width & by >= 0 & by <= Height})@invariant(Py = by) /* Diff Invariant*/
    )*@invariant(bx >= 0 & bx <= Width & Py = by)  /* Loop Invariant */
\]
(bx >= 0 & bx <= Width) /* Safety Condition */
}
