/****************************  Aufg6_4.java  *********************************/
import AlgoTools.IO;

/**
 * Beweis der Korrektheit mit der Zusicherungsmethode
 */

public class Aufg6_4 {

  public static void main(String[] args) {

    int i = 0, h = 1, z = 0, n;

    do {
      n = IO.readInt("n= ");
    } while (n < 0);

 // z = i * i und h = 2 * i + 1 und i <= n ist Schleifeninvariante  = P 

    while (i < n) {
 //z=i*i und h=2*i+1 und i<n
      z =z+h;
//z=i*i + 2*i+1 und h=2*i+1 und i<n
      h =h+2;
//z=i*i + 2*i+1 und h=2*i+1+2 und i<n
//z=(i+1)^2 und h=2*i+3 und i<n
      i++;
//z=i^2 und h=2*i+1 und i<=n    = P


    }
//z=i^2 und h=2*i+1 und i>n = P und nicht_Q

//SOO, wie komme hier auf z=i^2  bzw. wieso fällt das andere weg??
    IO.println(z, 6);
//SOO, wie komme hier auf z=i^2  bzw. wieso fällt das andere weg??
  }
}

caioo