%Patch files loaded: (patch2) version 2.175 $$$single.pvs single: THEORY BEGIN time: TYPE = int j, k, m, n, t, t1, t2: VAR time value: TYPE = {x: nat | x <= 1} signal: TYPE = [time -> value] i, o, x, a, b, y, f: VAR signal -((a: value)): value = (1 - a) ; delay(i, o): bool = (FORALL t: (o(t + 1) = i(t))) bubble_and(a, b, y): bool = (FORALL t: (y(t) = (-a(t)) * b(t))) inv(i, o): bool = (FORALL t: o(t) = -i(t)) env1(f): bool = (FORALL t: (EXISTS t1: t1 < t AND f(t1) = 0)) env2(f): bool = (FORALL t: (EXISTS t1: t < t1 AND f(t1) = 0)) imp(i, o): bool = (EXISTS x: (delay(i, x) AND bubble_and(i, x, o))) Pulse(f, n, m): bool = (n < m AND f(n - 1) = 0 AND f(m) = 0 AND (FORALL t: (n <= t AND t < m IMPLIES f(t) = 1))) SinglePulse(f, n): bool = Pulse(f, n, n + 1) spec1(i, o): bool = (FORALL n, m: Pulse(i, n, m) IMPLIES (EXISTS k: n <= k AND k <= m AND o(k) = 1 AND (FORALL j: (n <= j AND j <= m AND o(j) = 1 IMPLIES j = k)))) spec1_insufficient: lemma inv(i,o) => spec1(i,o) spec2(i, o): bool = (FORALL k: o(k) = 1 IMPLIES SinglePulse(o, k) AND (EXISTS n, m: n <= k AND k <= m AND Pulse(i, n, m))) IMPORTING bounds env1_lemma: LEMMA env1(f) IMPLIES (EXISTS (t1: time): t1 < t AND f(t1) = 0 AND (FORALL (t2: time): t1 < t2 AND t2 < t IMPLIES NOT (f(t2) = 0))) sp_in_lemma: LEMMA o(k) = 1 AND imp(i, o) IMPLIES i(k) = 0 AND i(k - 1) = 1 single_pulse1: LEMMA imp(i, o) IMPLIES spec1(i, o) single_pulse2: LEMMA env1(i) IMPLIES (imp(i, o) IMPLIES spec2(i, o)) single_pulse: LEMMA env1(i) AND imp(i, o) IMPLIES spec1(i, o) AND spec2(i, o) END single $$$single.prf (|single| (|difference_TCC1| "" (SUBTYPE-TCC) NIL) (|spec1_insufficient| "" (EXPAND "spec1") (("" (SKOSIMP*) (("" (INST + "m!1") (("" (EXPAND "Pulse") (("" (EXPAND "inv") (("" (ASSERT) (("" (FLATTEN) (("" (ASSERT) (("" (SPLIT) (("1" (INST?) (("1" (EXPAND "-") (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (INST?) (("2" (INST?) (("2" (EXPAND "-") (("2" (ASSERT) NIL))))))))))))))))))))))))))) (|env1_lemma| "" (APPLY (SKOSIMP*)) (("" (EXPAND "env1") (("" (INST * "t!1") (("" (LEMMA "bounded_max_int" ("p" "(lambda t: f!1(t)=0)" "j" "t!1")) (("" (BETA) (("" (APPLY (GROUND$)) NIL))))))))))) (|sp_in_lemma| "" (EXPAND "imp") (("" (EXPAND "delay") (("" (EXPAND "bubble_and") (("" (APPLY (SKOSIMP*)) (("" (EXPAND "-" -3) (("" (INST * "k!1-1") (("" (INST * "k!1") (("" (APPLY (THEN* (CASE "i!1(k!1)=1") (CASE "i!1(k!1-1)=0") (GROUND$))) NIL))))))))))))))) (|single_pulse1| "" (AUTO-REWRITE-EXPLICIT) (("" (ASSERT) (("" (SKOSIMP*) (("" (INST + "m!1") (("" (ASSERT) (("" (PROP) (("1" (INST - "m!1-1") (("1" (INST - "m!1") (("1" (INST - "m!1-1") (("1" (GROUND) NIL))))))) ("2" (SKOSIMP*) (("2" (INST - "j!1-1") (("2" (INST - "j!1") (("2" (INST - "j!1") (("2" (GROUND) NIL))))))))))))))))))))) (|single_pulse2| "" (EXPAND "spec2") (("" (APPLY (SKOSIMP*)) (("" (LEMMA "sp_in_lemma") (("" (INST * "oh!1" "i!1" "k!1") (("" (SPLIT) (("1" (EXPAND "SinglePulse") (("1" (EXPAND "Pulse") (("1" (EXPAND "imp") (("1" (EXPAND "delay") (("1" (EXPAND "bubble_and") (("1" (EXPAND "-" -3) (("1" (APPLY (SKOSIMP*)) (("1" (SPLIT) (("1" (INST -5 "k!1-1") (("1" (ASSERT) NIL))) ("2" (INST -5 "k!1+1") (("2" (INST -4 "k!1") (("2" (ASSERT) NIL))))) ("3" (APPLY (THEN* (SKOSIMP*) (ASSERT))) NIL) ("4" (LEMMA "env1_lemma") (("4" (INST * "i!1" "k!1-1") (("4" (SPLIT) (("1" (APPLY (SKOSIMP*)) (("1" (INST + "t1!1+1" "k!1") (("1" (APPLY (GROUND$)) (("1" (APPLY (SKOSIMP*)) (("1" (INST * "t!1") (("1" (ASSERT) NIL))))))))))) ("2" (PROPAX) NIL))))))))))))))))))))))) ("2" (PROPAX) NIL) ("3" (PROPAX) NIL))))))))))) (|single_pulse| "" (APPLY (SKOSIMP*)) (("" (SPLIT) (("1" (REWRITE "single_pulse1") NIL) ("2" (REWRITE "single_pulse2") NIL)))))) $$$bounds.pvs bounds: THEORY BEGIN l, m, n: VAR nat i, j, k: VAR integer p: VAR pred[integer] bounded_maximum2: LEMMA FORALL m: l < m AND p(l) => (EXISTS l: l < m AND p(l) AND (FORALL n: l < n AND n < m => NOT p(n))) bounded_maximum: LEMMA FORALL m: (EXISTS l: l < m AND p(l)) <=> (EXISTS l: l < m AND p(l) AND (FORALL n: l < n AND n < m => NOT p(n))) bounded_max2_int: LEMMA FORALL j: i < j AND p(i) => EXISTS i: i < j AND p(i) AND (FORALL k: i < k AND k < j => NOT p(k)) bounded_max_int: LEMMA FORALL j: (EXISTS i: i < j AND p(i)) <=> (EXISTS i: i < j AND p(i) AND (FORALL k: i < k AND k < j => NOT p(k))) bounded_minimum2: AXIOM FORALL m: m < l AND p(l) => (EXISTS l: m < l AND p(l) AND (FORALL n: m < n AND n < l => NOT p(n))) bounded_minimum: LEMMA FORALL m: (EXISTS l: m < l AND p(l)) <=> (EXISTS l: m < l AND p(l) AND (FORALL n: m < n AND n < l => NOT p(n))) bounded_min2_int: LEMMA FORALL j: j < i AND p(i) => EXISTS i: j < i AND p(i) AND (FORALL k: j < k AND k < i => NOT p(k)) bounded_min_int: LEMMA FORALL j: (EXISTS i: j < i AND p(i)) <=> (EXISTS i: j < i AND p(i) AND (FORALL k: j < k AND k < i => NOT p(k))) END bounds $$$bounds.prf (|bounds| (|bounded_maximum2| "" (APPLY (THEN (SKOLEM 1 ("l!1" "p!1" "_")) (INDUCT "m"))) (("1" (APPLY (GROUND$)) NIL) ("2" (APPLY (THEN* (SKOSIMP*) (GROUND$) (SKOSIMP*))) (("1" (CASE "p!1(j!1)") (("1" (INST + "j!1") (("1" (APPLY (THEN* (GROUND$) (SKOSIMP*) (GROUND$))) NIL))) ("2" (INST + "l!2") (("2" (APPLY (THEN* (GROUND$) (SKOSIMP*) (GROUND$))) (("2" (INST * "n!1") (("2" (APPLY (GROUND$)) NIL))))))))) ("2" (APPLY (THEN (INST + "j!1") (GROUND$))) (("2" (APPLY (THEN (SKOSIMP*) (GROUND))) NIL))))))) (|bounded_maximum| "" (APPLY (THEN* (SKOSIMP*) (GROUND$) (SKOSIMP*))) (("1" (LEMMA "bounded_maximum2" ("l" "l!1" "p" "p!1" "m" "m!1")) (("1" (APPLY (GROUND$)) NIL))) ("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL))))))) (|bounded_max2_int| "" (APPLY (SKOSIMP*)) (("" (LEMMA "bounded_maximum2" ("l" "i!1-i!1" "p" "(lambda i: p!1(i+i!1))" "m" "j!1-i!1")) (("1" (APPLY (THEN (GROUND$) (SKOSIMP*))) (("1" (INST + "l!1+i!1") (("1" (APPLY (THEN (GROUND$) (SKOSIMP*))) (("1" (APPLY (THEN (INST * "k!1-i!1") (GROUND$))) NIL))))))) ("2" (APPLY (GROUND$)) NIL))))) (|bounded_max_int| "" (APPLY (SKOSIMP*)) (("" (APPLY (THEN (SPLIT) (SKOSIMP*))) (("1" (LEMMA "bounded_max2_int" ("i" "i!1" "p" "p!1" "j" "j!1")) (("1" (ASSERT) NIL))) ("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL))))))))) (|bounded_minimum2| "" (INDUCT "l") (("3" (APPLY (SKOSIMP*)) (("3" (INST?) (("3" (CASE "m!1=j!1") (("1" (INST + "j!1+1") (("1" (ASSERT) (("1" (APPLY (THEN (SKOLEM!) (GROUND$))) NIL))))) ("2" (APPLY (GROUND$)) (("2" (POSTPONE) NIL))))))))))) (|bounded_minimum| "" (APPLY (THEN* (SKOSIMP*) (GROUND$) (SKOSIMP*))) (("1" (LEMMA "bounded_minimum2" ("l" "l!1" "p" "p!1" "m" "m!1")) (("1" (APPLY (GROUND$)) NIL))) ("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL))))))) (|bounded_min2_int| "" (APPLY (SKOSIMP*)) (("" (LEMMA "bounded_minimum2" ("l" "i!1-j!1" "p" "(lambda i: p!1(i+j!1))" "m" "j!1-j!1")) (("1" (APPLY (THEN (GROUND$) (SKOSIMP*))) (("1" (INST + "l!1+j!1") (("1" (APPLY (THEN (GROUND$) (SKOSIMP*))) (("1" (APPLY (THEN (INST * "k!1-j!1") (GROUND$))) NIL))))))) ("2" (APPLY (GROUND$)) NIL))))) (|bounded_min_int| "" (APPLY (SKOSIMP*)) (("" (APPLY (THEN (SPLIT) (SKOSIMP*))) (("1" (LEMMA "bounded_min2_int" ("i" "i!1" "p" "p!1" "j" "j!1")) (("1" (ASSERT) NIL))) ("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL))))))))))