| products/sources/formale sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: virtual_clock_2.pvs Sprache: VDMOriginal von: PVS© |
|
||||||
|
(interval_clocks
(T_def 0 (T_def-1 nil 3381399668 ("" (expand "T") (("" (propax) nil nil)) nil) ((T const-decl "int" interval_clocks nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil)) shostak)) (T_rounds 0 (T_rounds-1 nil 3381399683 ("" (expand "T") (("" (propax) nil nil)) nil) ((T const-decl "int" interval_clocks nil) (int_plus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (handover_precision_lower 0 (handover_precision_lower-1 nil 3399129068 ("" (skosimp*) (("" (expand "adjustment_lower_bound?") (("" (expand "t") (("" (inst?) (("" (lemma "drift_right") (("" (inst - "T(j!1)" "T(j!1+1)" "ic1!1(j!1)") (("" (rewrite "T_def") (("" (rewrite "drift") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (adjustment_lower_bound? const-decl "bool" interval_clocks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (T const-decl "int" interval_clocks nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (rate const-decl "posreal" physical_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil) (drift const-decl "nonneg_real" physical_clocks nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (T_def formula-decl nil interval_clocks nil) (rho formal-const-decl "nnreal" interval_clocks nil) (nnreal type-eq-decl nil real_types nil) (drift_right formula-decl nil physical_clocks nil) (t const-decl "real" interval_clocks nil)) nil)) (handover_precision_upper 0 (handover_precision_upper-1 nil 3399129088 ("" (skosimp*) (("" (expand "adjustment_upper_bound?") (("" (expand "t") (("" (inst?) (("" (lemma "drift_left") (("" (inst - "T(j!1)" "T(j!1+1)" "ic1!1(j!1)") (("" (rewrite "T_def") (("" (rewrite "drift") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (adjustment_upper_bound? const-decl "bool" interval_clocks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (T const-decl "int" interval_clocks nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (rate const-decl "posreal" physical_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil) (drift const-decl "nonneg_real" physical_clocks nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (T_def formula-decl nil interval_clocks nil) (rho formal-const-decl "nnreal" interval_clocks nil) (nnreal type-eq-decl nil real_types nil) (drift_left formula-decl nil physical_clocks nil) (t const-decl "real" interval_clocks nil)) nil)) (handover_precision 0 (handover_precision-1 nil 3399129148 ("" (skosimp*) (("" (expand "abs") (("" (lift-if) (("" (rewrite "handover_precision_lower") (("" (use "handover_precision_upper") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (handover_precision_lower formula-decl nil interval_clocks nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (rho formal-const-decl "nnreal" interval_clocks nil) (rate const-decl "posreal" physical_clocks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (handover_precision_upper formula-decl nil interval_clocks nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (nonoverlap_peers 0 (nonoverlap_peers-3 "" 3381397883 ("" (skosimp*) (("" (expand "peer_precision?") (("" (expand "t") (("" (inst?) (("" (lemma "skew_bound_1") (("" (inst - "T(j!1)" "T1!1" "T1!1 + X!1" "P" "ic1!1(j!1)" "ic2!1(j!1)" "pi!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((peer_precision? const-decl "bool" interval_clocks nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (T const-decl "int" interval_clocks nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" interval_clocks nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (rate const-decl "posreal" physical_clocks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (rho formal-const-decl "nnreal" interval_clocks nil) (nnreal type-eq-decl nil real_types nil) (skew_bound_1 formula-decl nil physical_clocks nil) (t const-decl "real" interval_clocks nil)) shostak) (nonoverlap_peers-2 nil 3315403635 ("" (skosimp*) (("" (expand "peer_precision?") (("" (inst?) (("" (rewrite "T_def") (("" (lemma "proper_separation") (("" (inst - "T(j!1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1)" "0" "pi_0") (("" (assert) (("" (hide 2 -1) (("" (invoke (then (case "%1 <= ADJ") (assert)) (! 1 r)) (("" (hide 2 -3) (("" (expand "ADJ") (("" (rewrite "floor_monotone") (("" (hide 2) (("" (cancel) (("" (invoke (then (case "%1 <= %2") (assert)) (! 1 l) (! 1 r 2)) (("" (hide 2) (("" (cancel) (("" (cancel) (("" (rewrite "max_le") (("" (rewrite "max_le") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rate const-decl "posreal" physical_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (floor_monotone formula-decl nil floor_ceiling_ineq nil) (max_le formula-decl nil minmax_ineq nil) (drift const-decl "nonneg_real" physical_clocks nil)) nil) (nonoverlap_peers-1 nil 3294485333 ("" (skosimp*) (("" (lemma "proper_separation") (("" (inst - "T(j!1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1)" "0" "delta_0") (("" (assert) (("" (prop) (("1" (expand "peer_precision?") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2 -1) (("2" (invoke (then (case "%1 <=ADJ") (assert)) (! 1 r)) (("2" (hide 2 -3) (("2" (expand "ADJ") (("2" (rewrite "floor_monotone") (("2" (hide 2) (("2" (div-by 1 "id(1 + rho)") (("2" (expand "id") (("2" (move-terms 1 l 2) (("2" (assert) (("2" (invoke (then (case "%1 <= %2") (assert)) (! 1 l) (! 1 r 2)) (("2" (hide 2) (("2" (div-by 1 "drift") (("2" (rewrite "max_le") (("2" (rewrite "max_le") (("2" (rewrite "T_def") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((good_clock nonempty-type-eq-decl nil physical_clocks nil) (drift const-decl "nonneg_real" physical_clocks nil) (floor_monotone formula-decl nil floor_ceiling_ineq nil)) nil)) (nonoverlap_lower 0 (nonoverlap_lower-3 nil 3365507387 ("" (skosimp*) (("" (use "handover_precision_lower") (("" (assert) (("" (lemma "nonoverlap_basis") (("" (inst - _ "T1!1" "T1!1 + X!1" _ "ic1!1(j!1)" "ic2!1(1 + j!1)") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((handover_precision_lower formula-decl nil interval_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" interval_clocks nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonoverlap_basis formula-decl nil physical_clocks nil) (P formal-const-decl "posnat" interval_clocks nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (drift const-decl "nonneg_real" physical_clocks nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (T const-decl "int" interval_clocks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (nonoverlap_lower-2 nil 3315403714 ("" (skosimp*) (("" (lemma "proper_separation") (("" (inst - "T(j!1 + 1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1 + 1)" "0" "drift * P + pi_0 + alpha_l") (("" (assert) (("" (prop) (("1" (forward-chain "handover_precision_lower") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2 -1) (("2" (invoke (then (case "%1 <= ADJ") (assert)) (! 1 r)) (("2" (hide 2 -3) (("2" (expand "ADJ") (("2" (rewrite "floor_monotone") (("2" (hide 2) (("2" (expand "id") (("2" (cancel) (("2" (isolate 1 l 1) (("2" (assert) (("2" (factor 1) (("2" (div-by 1 "rate") (("2" (invoke (case "%1 <= 0") (! 1 l 1)) (("1" (mult-by -1 "drift") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (rewrite "max_le") (("2" (rewrite "max_le") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((floor_monotone formula-decl nil floor_ceiling_ineq nil) (max_le formula-decl nil minmax_ineq nil) (drift const-decl "nonneg_real" physical_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (rate const-decl "posreal" physical_clocks nil)) nil) (nonoverlap_lower-1 nil 3294485363 ("" (skosimp*) (("" (lemma "proper_separation") (("" (inst - "T(j!1 + 1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1 + 1)" "0" "drift * P + delta_0 + epsilon_l") (("" (assert) (("" (prop) (("1" (forward-chain "handover_precision_lower") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2 -1) (("2" (invoke (then (case "%1 <= ADJ") (assert)) (! 1 r)) (("2" (hide 2 -3) (("2" (expand "ADJ") (("2" (rewrite "floor_monotone") (("2" (hide 2) (("2" (div-by 1 "id(1 + rho)") (("2" (expand "id") (("2" (move-terms 1 l (2 3)) (("2" (assert) (("2" (invoke (case "%1 <= 0") (! 1 l 1 2)) (("1" (mult-by -1 "drift") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (rewrite "max_le") (("2" (rewrite "max_le") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((good_clock nonempty-type-eq-decl nil physical_clocks nil) (drift const-decl "nonneg_real" physical_clocks nil) (floor_monotone formula-decl nil floor_ceiling_ineq nil)) nil)) (nonoverlap_upper 0 (nonoverlap_upper-2 nil 3365507440 ("" (skosimp*) (("" (use "handover_precision_upper") (("" (assert) (("" (lemma "nonoverlap_basis") (("" (inst - _ "T1!1" "T1!1 + X!1" _ "ic2!1(1 + j!1)" "ic1!1(j!1)") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((handover_precision_upper formula-decl nil interval_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" interval_clocks nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonoverlap_basis formula-decl nil physical_clocks nil) (P formal-const-decl "posnat" interval_clocks nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (drift const-decl "nonneg_real" physical_clocks nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (T const-decl "int" interval_clocks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (nonoverlap_upper-1 nil 3294485393 ("" (skosimp*) (("" (lemma "proper_separation") (("" (inst - "T(j!1 + 1)" "T1!1" "T2!1" "ic2!1(j!1 + 1)" "ic1!1(j!1)" "0" "drift * P + pi_0 + alpha_u") (("" (assert) (("" (prop) (("1" (forward-chain "handover_precision_upper") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2 -1) (("2" (invoke (then (case "%1 <= ADJ") (assert)) (! 1 r)) (("2" (hide 2 -3) (("2" (expand "ADJ") (("2" (rewrite "floor_monotone") (("2" (hide 2) (("2" (expand "id") (("2" (isolate 1 l 1) (("2" (assert) (("2" (factor 1 r) (("2" (div-by 1 "rate") (("2" (invoke (case "%1 <= 0") (! 1 l 1)) (("1" (mult-by -1 "drift") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (rewrite "max_le") (("2" (rewrite "max_le") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((floor_monotone formula-decl nil floor_ceiling_ineq nil) (max_le formula-decl nil minmax_ineq nil) (drift const-decl "nonneg_real" physical_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (rate const-decl "posreal" physical_clocks nil)) nil)) (nonoverlap_round 0 (nonoverlap_round-3 "" 3400004207 ("" (skosimp*) (("" (use "handover_precision_lower") (("" (assert) (("" (use "nonoverlap_basis") (("" (rewrite "T_def") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((handover_precision_lower formula-decl nil interval_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" interval_clocks nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nonoverlap_basis formula-decl nil physical_clocks nil) (T const-decl "int" interval_clocks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (drift const-decl "nonneg_real" physical_clocks nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" interval_clocks nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (T_def formula-decl nil interval_clocks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (nonoverlap_round-2 "" 3400004192 ("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak) (nonoverlap_round-1 nil 3294485429 ("" (skosimp*) (("" (rewrite "T_def") (("" (use "nonoverlap_lower") (("" (rewrite "T_def") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((rate const-decl "posreal" physical_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil)) nil)) (lower_interval_accuracy 0 (lower_interval_accuracy-2 nil 3399233072 ("" (induct "j") (("1" (assert) (("1" (skosimp*) (("1" (expand "lower_accuracy_bound?") (("1" (skosimp*) (("1" (inst -2 0) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "lower_accuracy_bound?" -2) (("2" (skosimp*) (("2" (inst - "alpha!1" "ic1!1" "p!1" 0) (("2" (prop) (("1" (replace -5 :dir rl) (("1" (expand "adjustment_lower_bound?") (("1" (inst - "j!1") (("1" (inst - "1 + j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "lower_accuracy_bound?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((adjustment_lower_bound? const-decl "bool" interval_clocks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (t const-decl "real" interval_clocks nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (P formal-const-decl "posnat" interval_clocks nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (lower_accuracy_bound? const-decl "bool" interval_clocks nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (interval_clock type-eq-decl nil interval_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" interval_clocks nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil) (lower_interval_accuracy-1 nil 3399232999 ("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak)) (upper_interval_accuracy 0 (upper_interval_accuracy-2 nil 3399237520 ("" (induct "j") (("1" (assert) (("1" (expand "upper_accuracy_bound?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "upper_accuracy_bound?" -2) (("2" (skosimp*) (("2" (inst - "alpha!1" "ic1!1" "p!1" 0) (("2" (prop) (("1" (replace -5 :dir rl) (("1" (expand "adjustment_upper_bound?") (("1" (inst - "j!1") (("1" (inst - "1 + j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_accuracy_bound?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((adjustment_upper_bound? const-decl "bool" interval_clocks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (t const-decl "real" interval_clocks nil) (P formal-const-decl "posnat" interval_clocks nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (upper_accuracy_bound? const-decl "bool" interval_clocks nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (interval_clock type-eq-decl nil interval_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" interval_clocks nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) nil) (upper_interval_accuracy-1 nil 3399233266 ("" (expand "upper_accuracy_bound?") (("" (skosimp*) (("" (lemma "upper_adjustment") (("" (inst - "ic1!1" "j!1" "p!1") (("" (assert) (("" (expand "t") (("" (inst - "T(j!1)" "j!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rate const-decl "posreal" physical_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil)) nil))) ¤ Dauer der Verarbeitung: 0.49 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
