sum2_why: THEORY
BEGIN

  % Why obligation from file "sum2.c", line 10, characters 20-26: 
  sum_ensures_default_po_1: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    0 <= i

  % Why obligation from file "sum2.c", line 10, characters 25-31: 
  sum_ensures_default_po_2: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    i <= n

  % Why obligation from file "sum2.c", line 10, characters 35-49: 
  sum_ensures_default_po_3: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    s_0 <= i * (i + 1)

  % Why obligation from file "sum2.c", line 10, characters 20-26: 
  sum_ensures_default_po_4: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    FORALL (i0: int) :
    FORALL (s_0_0: int) :
    (0 <= i0 AND (i0 <= n AND
    s_0_0 <= i0 * (i0 + 1))) IMPLIES
    i0 < n IMPLIES
    FORALL (s_0_1: int) :
    s_0_1 = s_0_0 + (i0 + 1) IMPLIES
    FORALL (i1: int) :
    i1 = i0 + 1 IMPLIES
    0 <= i1

  % Why obligation from file "sum2.c", line 10, characters 25-31: 
  sum_ensures_default_po_5: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    FORALL (i0: int) :
    FORALL (s_0_0: int) :
    (0 <= i0 AND (i0 <= n AND
    s_0_0 <= i0 * (i0 + 1))) IMPLIES
    i0 < n IMPLIES
    FORALL (s_0_1: int) :
    s_0_1 = s_0_0 + (i0 + 1) IMPLIES
    FORALL (i1: int) :
    i1 = i0 + 1 IMPLIES
    i1 <= n

  % Why obligation from file "sum2.c", line 10, characters 35-49: 
  sum_ensures_default_po_6: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    FORALL (i0: int) :
    FORALL (s_0_0: int) :
    (0 <= i0 AND (i0 <= n AND
    s_0_0 <= i0 * (i0 + 1))) IMPLIES
    i0 < n IMPLIES
    FORALL (s_0_1: int) :
    s_0_1 = s_0_0 + (i0 + 1) IMPLIES
    FORALL (i1: int) :
    i1 = i0 + 1 IMPLIES
    s_0_1 <= i1 * (i1 + 1)

  % Why obligation from file "sum2.c", line 4, characters 12-32: 
  sum_ensures_default_po_7: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    FORALL (i0: int) :
    FORALL (s_0_0: int) :
    (0 <= i0 AND (i0 <= n AND
    s_0_0 <= i0 * (i0 + 1))) IMPLIES
    i0 >= n IMPLIES
    FORALL (return: int) :
    return = s_0_0 IMPLIES
    return <= n * (n + 1)

  % Why obligation from file "sum2.c", line 11, characters 18-21: 
  sum_safety_po_1: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    FORALL (i0: int) :
    FORALL (s_0_0: int) :
    True IMPLIES
    (0 <= i0 AND (i0 <= n AND
    s_0_0 <= i0 * (i0 + 1))) IMPLIES
    i0 < n IMPLIES
    FORALL (s_0_1: int) :
    s_0_1 = s_0_0 + (i0 + 1) IMPLIES
    FORALL (i1: int) :
    i1 = i0 + 1 IMPLIES
    0 <= (n - i0)

  % Why obligation from file "sum2.c", line 11, characters 18-21: 
  sum_safety_po_2: LEMMA
    FORALL (n: int) :
    n > 1 IMPLIES
    FORALL (s_0: int) :
    s_0 = 0 IMPLIES
    FORALL (i: int) :
    i = 0 IMPLIES
    FORALL (i0: int) :
    FORALL (s_0_0: int) :
    True IMPLIES
    (0 <= i0 AND (i0 <= n AND
    s_0_0 <= i0 * (i0 + 1))) IMPLIES
    i0 < n IMPLIES
    FORALL (s_0_1: int) :
    s_0_1 = s_0_0 + (i0 + 1) IMPLIES
    FORALL (i1: int) :
    i1 = i0 + 1 IMPLIES
    (n - i1) < (n - i0)

END sum2_why