(|sigma| (|sigma_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sigma_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|sigma_sum| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (LIFT-IF) (("2" (GROUND) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (GROUND) NIL NIL)) NIL)) NIL) (|sigma_diff_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sigma_diff_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|sigma_diff| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1 1) (("2" (GROUND) (("2" (EXPAND "sigma" 1 3) (("2" (GROUND) (("2" (LIFT-IF) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (HIDE 2) (("5" (ASSERT) NIL NIL)) NIL)) NIL) (|sigma_diff_neg| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1 2) (("2" (GROUND) (("2" (EXPAND "sigma" 1 3) (("2" (LIFT-IF) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (HIDE 2) (("5" (ASSERT) NIL NIL)) NIL)) NIL) (|sigma_split| "" (CASE "(FORALL (F: [subrange(ii,jj) -> real]), low,m,rng: m >= low AND m < low+rng AND low+rng <= jj IMPLIES sigma(low, low+rng, F) = sigma(low, m, F) + sigma(m+1, low+rng, F))") (("1" (SKOSIMP*) (("1" (INST -1 "F!1" "low!1" "m!1" "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (EXPAND "sigma" 1 3) (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE-REPLACE "m!1 = 1 + j!1 + low!1") (("1" (HIDE -1) (("1" (EXPAND "sigma" + 3) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (INST -1 "F!1" "low!1" "m!1") (("2" (EXPAND "sigma" + 1) (("2" (EXPAND "sigma" + 2) (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (TYPEPRED "rng!2") (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (ASSERT) (("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("5" (HIDE 2) (("5" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (HIDE 2) (("4" (SKOSIMP*) (("4" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (HIDE 2) (("5" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_first_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sigma_first| "" (SKOSIMP*) (("" (LEMMA "sigma_split") (("" (INST?) (("" (INST -1 "low!1") (("" (ASSERT) (("" (EXPAND "sigma" -1 3) (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_eq_arg| "" (SKOSIMP*) (("" (EXPAND "sigma") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|sigma_const| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): low!1 + rng <= jj IMPLIES sigma(low!1, low!1+rng, (LAMBDA i: x!1)) = IF low!1+rng >= low!1 THEN (low!1+rng - low!1 + 1) * x!1 ELSE 0 ENDIF)") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT-AND-SIMPLIFY "rng") NIL NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) (|sigma_mult| "" (SKOSIMP*) (("" (CASE "(FORALL (rng:nat): low!1+rng <= jj IMPLIES sigma(low!1, low!1+rng, (LAMBDA i: x!1 * F!1(i))) = x!1 * sigma(low!1, low!1+rng, F!1))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (EXPAND "sigma") (("1" (PROPAX) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_bound| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): (FORALL i: i >= low!1 AND i <= low!1+rng IMPLIES F!1(i) <= B!1) AND low!1 + rng <= jj IMPLIES sigma(low!1, low!1+rng, F!1) <= B!1 * abs(low!1+rng - low!1 + 1))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (HIDE -2 2) (("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (REWRITE "sigma_eq_arg") (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (SPLIT -1) (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "abs") (("2" (ASSERT) (("2" (EXPAND "sigma") (("2" (ASSERT) (("2" (LIFT-IF) (("2" (GROUND) (("1" (REVEAL -1) (("1" (INST -1 "low!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REVEAL -1) (("2" (INST -1 "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_abs| "" (SKOSIMP*) (("" (CASE "(FORALL (rng: nat): low!1 + rng <= high!1 IMPLIES abs(sigma(low!1, low!1+rng, F!1)) <= sigma(low!1, low!1+rng, LAMBDA i: abs(F!1(i))))") (("1" (INST -1 "high!1-low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (EXPAND "sigma") (("2" (ASSERT) (("2" (EXPAND "abs") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "sigma") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (ASSERT) (("2" (LEMMA "triangle") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_restrict| "" (INDUCT "high") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (LIFT-IF) (("1" (GROUND) (("1" (EXPAND "restrict") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (EXPAND "restrict") (("2" (LIFT-IF) (("2" (LIFT-IF) (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) NIL NIL)) NIL) (|sigma_restrict_eq| "" (SKOSIMP*) (("" (LEMMA "sigma_restrict") (("" (INST?) (("" (INST -1 "high!1" "low!1") (("" (ASSERT) (("" (REPLACE -1) (("" (HIDE -1) (("" (LEMMA "sigma_restrict") (("" (INST -1 "G!1" "high!1" "high!1" "low!1" "low!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_eq_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|sigma_eq| "" (SKOSIMP*) (("" (LEMMA "sigma_restrict_eq") (("" (INST?) (("" (ASSERT) (("" (HIDE 2) (("" (EXPAND "restrict") (("" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("" (LIFT-IF) (("" (GROUND) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_nonneg| "" (CASE " FORALL (F: [subrange(ii, jj) -> real], rng:nat, low: subrange(ii, jj)): (FORALL i: F(i) >= 0) AND low + rng <= jj IMPLIES sigma(low, low+rng, F) >= 0") (("1" (SKOSIMP*) (("1" (INST?) (("1" (INST -1 "high!1-low!1" "low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (INST?) (("2" (INST?) (("1" (ASSERT) (("1" (REVEAL -1) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_nonpos| "" (CASE " FORALL (F: [subrange(ii, jj) -> real], rng:nat, low: subrange(ii, jj)): (FORALL i: F(i) <= 0) AND low + rng <= jj IMPLIES sigma(low, low+rng, F) <= 0") (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) (("1" (INST -1 "high!1-low!1" "low!1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "sigma") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (EXPAND "sigma") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "sigma" 1) (("2" (INST?) (("2" (INST?) (("1" (ASSERT) (("1" (REVEAL -1) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) (|sigma_TCC3| "" (SKOSIMP*) (("" (REWRITE "sigma_nonneg") (("" (HIDE 2) (("" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_TCC4| "" (SKOSIMP*) (("" (REWRITE "sigma_nonpos") (("" (HIDE 2) (("" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_TCC5| "" (AUTO-REWRITE-THEORY "integers") (("" (AUTO-REWRITE-THEORY "rationals") (("" (MEASURE-INDUCT+ "high~low" ("high" "low")) (("" (SKOSIMP*) (("" (EXPAND "sigma" 1) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "~") (("1" (GROUND) (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "~") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) (("2" (TYPEPRED "Fnat!1(x!1)") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LIFT-IF) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_TCC6| "" (AUTO-REWRITE-THEORY "integers") (("" (AUTO-REWRITE-THEORY "rationals") (("" (MEASURE-INDUCT+ "high~low" ("high" "low")) (("" (SKOSIMP*) (("" (EXPAND "sigma" 1) (("" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "~") (("1" (GROUND) (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) (("2" (EXPAND "~") (("2" (LIFT-IF) (("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LIFT-IF) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sigma_nonnegfun_eq_0| "" (SKOSIMP*) (("" (CASE "FORALL (Fnnr: [subrange(ii, jj) -> nonneg_real], rng:nat, low: subrange(ii, jj)): low + rng <= jj AND sigma(low, low+rng, Fnnr) = 0 AND low <= i!1 AND i!1 <= low + rng IMPLIES Fnnr(i!1) = 0") (("1" (INST?) (("1" (INST -1 "high!1-low!1" "low!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INDUCT "rng") (("1" (SKOSIMP*) (("1" (HIDE -5 2) (("1" (EXPAND "sigma") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST?) (("2" (EXPAND "sigma" -3) (("2" (CASE-REPLACE "i!1 = low!2 + (j!1 + 1)") (("1" (HIDE -1 -2 -3 -5 -6 -7 -8 -9 2) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST -1 "low!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 2) (("3" (SKOSIMP*) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) NIL NIL)) NIL)) NIL))