/* 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: 34285
Branches: 3846
Interactive steps: 1227
Arithmetic Solver: 2958.415
Time: 2469.39
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 Pvmax;
//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 & Pvmax^2 > vy^2 & Pvmax > 0 & by >= Py - paddleWidth & 
            by <= Py + paddleWidth) /* & 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 */
    if (by > Py) then (Pvy := Pvmax)
    else (Pvy := -Pvmax) 
    fi;
    /* Opponent Paddle moves non-deterministically to be where it needs to be */
    Oy := by;
    
  
    /* PADDLE PHYSICS EVENTS */    
    if (bx = 0 & by >= Py - paddleWidth & 
            by <= Py + paddleWidth & vx < 0) then (vx := -vx)
            /* rebound off of the player paddle */
       else (if (bx = Width & by >= Oy - paddleWidth & 
            by <= Oy + paddleWidth & vx > 0) then (vx := -vx) 
            /* rebound off the opponent paddle */
           fi)
        fi;

    /* CONTINUOUS DYNAMICS */
    (
/* first three diff eqs are the ones that govern real behavior */
     {bx' = vx, by' = vy, Py' = Pvy & bx >= 0 & bx <= Width & by >= 0 & by <= Py - paddleWidth} ++
     {bx' = vx, by' = vy, Py' = Pvy & bx >= 0 & bx <= Width & by >= Py - paddleWidth & by <= Py + paddleWidth} ++
     {bx' = vx, by' = vy, Py' = Pvy & bx >= 0 & bx <= Width & by >= Py + paddleWidth & by <= Height} ++
/* These three diff eqs govern behavior past the player paddle. Nothing 
     happens in them, cause the ball provably never ends up there. */
     {bx' = vx, by' = vy, Py' = Pvy & bx <= 0 & by >= 0 & by <= Py - paddleWidth} ++
     {bx' = vx, by' = vy, Py' = Pvy & bx <= 0 & by >= Py - paddleWidth & by <= Py + paddleWidth} ++
     {bx' = vx, by' = vy, Py' = Pvy & bx <= 0 & by >= Py + paddleWidth & by <= Height} ++
/* These three diff eqs govern behavior past the opponent paddle. Nothing 
     happens in them, cause the ball provably never ends up there. */
     {bx' = vx, by' = vy, Py' = Pvy & bx >= Width & by >= 0 & by <= Py - paddleWidth} ++
     {bx' = vx, by' = vy, Py' = Pvy & bx >= Width & by >= Py - paddleWidth & by <= Py + paddleWidth} ++
     {bx' = vx, by' = vy, Py' = Pvy & bx >= Width & by >= Py + paddleWidth & by <= Height}
     )@invariant(by >= Py - paddleWidth & by <= Py + paddleWidth & Pvmax^2 > vy^2) /* Diff Invariant*/
    
    )*@invariant(bx >= 0 & bx <= Width & by >= Py - paddleWidth & by <= Py + paddleWidth & Pvmax^2 > vy^2)  /* Loop Invariant */
\]
(bx >= 0 & bx <= Width) /* Safety Condition */
}
