/* REQUIRED INFORMATION:

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

Name: Milda Zizyte & Felix Hutchison
AndrewID: mzizyte; fhutchin
KeYmaera version: 3.6.12
Backends used (Mathematica, Z3, ...): Mathematica
Nodes: 
Branches: 
Interactive steps: 
Arithmetic Solver: 
Time: 
Proof completes (Y/N): N
Notes: This proof would be trivial if diff cuts and diff weaken were supported 
    for the <> modality. Gonna try a soundness proof of that for the paper, and
    if it works, y'all should totally add it. (As it is, it may be unprovable, 
    since differential equations with evolution domains can't guarantee 
    progress > delta for a fixed delta, which this would need for Diff Variant 
    to work.)

*/

\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 = Width & by > 0 & vx < 0 & by < Height & vx^2 + vy^2 = vel^2 & vel > 0 & paddleWidth > 0 & Pvmax^2 > vy^2 & Pvmax > 0 & (-Height * (Width/vel)) <= Pvmax & Py < Height & Py > 0) /* & 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;
    
    /* We don't need paddle interactions since it's only traveling on the court. */

    /* CONTINUOUS DYNAMICS */
    (
/* first three diff eqs are the ones that govern real behavior. since we're 
    only looking at the court , these are the only  */
    {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})
    )*
\>
(by >= Py - paddleWidth & by <= Py + paddleWidth) /* Termination Condition */
}
