/* 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: 20617
Branches: 2701
Interactive steps: 52
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;
}

/* Prove that the ball stays in bounds when bouncing off the walls */

\problem{

/* INITIAL CONDITIONS */
/* Linear non-zero velocity and non-empty playing space with ball inside */

(Width > 0 & Height > 0 & bx > 0 & by > 0 & bx < Width & by < Height & vx^2 + vy^2 = vel^2 & vel > 0)
->
\[
  (
    /* CONTROL */
    /* Bouncing off the walls. We check velocity to avoid oscillating
    in control forever */

    (
       if (bx = 0 & vx < 0) then (vx := -vx) fi;
       if (bx = Width & vx > 0) then (vx := -vx) fi;
       if (by = 0 & vy < 0) then (vy := -vy) fi;
       if (by = Height & vy > 0) then (vy := -vy) fi
    );

    /* CONTINUOUS DYNAMICS */
    /* The nine evolution domains correspond to the middle area of the 
    field and the areas directly above, below, to the left, to the right,
    and the four corners outside the field. We need these
    separate domains in order for the proof to work. */

    ({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 <= 0 & by <= 0} ++
     {bx' = vx, by' = vy & bx <= 0 & by >= Height} ++
    {bx' = vx, by' = vy & bx >= Width & by >= 0 & by <= Height} ++
    {bx' = vx, by' = vy & bx >= Width & by <= 0} ++
    {bx' = vx, by' = vy & bx >= Width & by >= Height} ++
    {bx' = vx, by' = vy & bx >= 0 & bx <= Width & by <= 0} ++
    {bx' = vx, by' = vy & bx >= 0 & bx <= Width & 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 */
}
