sum3_why: THEORY BEGIN % Why obligation from file "sum3.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 "sum3.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 "sum3.c", line 10, characters 36-42: 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 >= 0 % Why obligation from file "sum3.c", line 10, characters 46-74: 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 ((i > 0 IMPLIES s_0 * s_0 <= i * (i + 1))) % Why obligation from file "sum3.c", line 10, characters 20-26: 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 >= 0 AND ((i0 > 0 IMPLIES s_0_0 * 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 "sum3.c", line 10, characters 25-31: 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 >= 0 AND ((i0 > 0 IMPLIES s_0_0 * 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 "sum3.c", line 10, characters 36-42: 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 >= 0 AND ((i0 > 0 IMPLIES s_0_0 * 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 >= 0 % Why obligation from file "sum3.c", line 10, characters 46-74: sum_ensures_default_po_8: 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 >= 0 AND ((i0 > 0 IMPLIES s_0_0 * 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 > 0 IMPLIES s_0_1 * s_0_1 <= i1 * (i1 + 1))) % Why obligation from file "sum3.c", line 4, characters 12-40: sum_ensures_default_po_9: 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 >= 0 AND ((i0 > 0 IMPLIES s_0_0 * s_0_0 <= i0 * (i0 + 1)))))) IMPLIES i0 >= n IMPLIES FORALL (return: int) : return = s_0_0 IMPLIES return * return <= n * (n + 1) % Why obligation from file "sum3.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 >= 0 AND ((i0 > 0 IMPLIES s_0_0 * 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 "sum3.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 >= 0 AND ((i0 > 0 IMPLIES s_0_0 * 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 sum3_why