| products/Sources/formale Sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: fundamental_theorem.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(virtual_clock_2
(t_increasing 0 (t_increasing-1 nil 3399251935 ("" (expand "increasing?") (("" (skosimp*) (("" (typepred "ac!1") (("" (expand "weakly_accurate?") (("" (expand "adjustment_lower_bound?") (("" (flatten) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (adjustment_lower_bound? const-decl "bool" interval_clocks nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (>= 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" virtual_clock_2 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (interval_clock type-eq-decl nil interval_clocks nil) (weakly_accurate? const-decl "bool" interval_clocks nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (p_min const-decl "posreal" synch_constant_definitions nil) (p_max const-decl "posreal" synch_constant_definitions nil) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (increasing? const-decl "bool" event_sequences nil)) nil)) (t_unbounded 0 (t_unbounded-1 nil 3399251950 ("" (expand "unbounded?") (("" (skosimp*) (("" (lemma "axiom_of_archimedes") (("" (inst - "(t!1 - t(ac!1)(0))/ p_min") (("" (skosimp*) (("" (cross-mult) (("" (isolate -1 l 1) (("" (case "i!1 >= 0") (("1" (inst + "i!1") (("1" (typepred "ac!1") (("1" (expand "weakly_accurate?") (("1" (flatten) (("1" (lemma "lower_interval_accuracy") (("1" (inst - "pi_0 + alpha_l" "ac!1" "i!1" "p_min" 0) (("1" (expand "lower_accuracy_bound?") (("1" (expand "p_min") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + 0) (("2" (mult-by 1 "p_min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals 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) (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) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (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" virtual_clock_2 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (interval_clock type-eq-decl nil interval_clocks nil) (t const-decl "real" interval_clocks nil) (weakly_accurate? const-decl "bool" interval_clocks nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (p_min const-decl "posreal" synch_constant_definitions nil) (p_max const-decl "posreal" synch_constant_definitions nil) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (lower_accuracy_bound? const-decl "bool" interval_clocks nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (lower_interval_accuracy formula-decl nil interval_clocks nil) (i!1 skolem-const-decl "int" virtual_clock_2 nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (axiom_of_archimedes formula-decl nil real_props nil) (unbounded? const-decl "bool" event_sequences nil)) nil)) (t_event_sequence 0 (t_event_sequence-2 nil 3399251964 ("" (skosimp*) (("" (rewrite "t_increasing") (("" (rewrite "t_unbounded") nil nil)) nil)) nil) ((t_increasing formula-decl nil virtual_clock_2 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" virtual_clock_2 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (interval_clock type-eq-decl nil interval_clocks nil) (weakly_accurate? const-decl "bool" interval_clocks nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (p_min const-decl "posreal" synch_constant_definitions nil) (p_max const-decl "posreal" synch_constant_definitions nil) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (t_unbounded formula-decl nil virtual_clock_2 nil)) nil) (t_event_sequence-1 nil 3399251877 ("" (judgement-tcc) nil nil) nil nil)) (t_nonoverlap 0 (t_nonoverlap-1 nil 3399251981 ("" (expand* "compatible?" "nonoverlap?") (("" (skosimp*) (("" (expand "adjustment_lower_bound?") (("" (inst?) (("" (use "p_min_bound") (("" (div-by -1 "rate") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (rate const-decl "posreal" physical_clocks 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (t_event_sequence application-judgement "event_sequence" virtual_clock_2 nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (rho formal-const-decl "nnreal" virtual_clock_2 nil) (nnreal type-eq-decl nil real_types nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (p_min_bound formula-decl nil synch_constant_definitions nil) (adjustment_lower_bound? const-decl "bool" interval_clocks nil) (compatible? const-decl "bool" interval_clocks nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (nonoverlap? const-decl "bool" event_sequences nil)) nil)) (t_early 0 (t_early-1 nil 3399251996 ("" (expand "earliest_adjustment?") (("" (skosimp*) (("" (expand "t") (("" (assert) nil nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (t const-decl "real" interval_clocks nil) (earliest_adjustment? const-decl "bool" virtual_clocks nil)) nil)) (t_self 0 (t_self-1 nil 3399252014 ("" (expand "self_adjustment?") (("" (expand "t") (("" (skosimp*) (("" (prop) (("1" (expand "earliest_adjustment?") (("1" (skosimp*) (("1" (rewrite "clock_nondecreasing") nil nil)) nil)) nil) ("2" (expand "latest_adjustment?") (("2" (skosimp*) (("2" (typepred "ac!1") (("2" (expand "weakly_accurate?") (("2" (lemma "nonoverlap_upper") (("2" (expand "p_max") (("2" (inst - _ "1 + ADJ" _ _ _ _) (("2" (inst?) (("2" (inst?) (("2" (use "ADJ_ineq_h") (("2" (expand "id") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((t const-decl "real" interval_clocks nil) (rho formal-const-decl "nnreal" virtual_clock_2 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) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (p_max const-decl "posreal" synch_constant_definitions nil) (p_min const-decl "posreal" synch_constant_definitions nil) (weakly_accurate? const-decl "bool" 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) (rate const-decl "posreal" physical_clocks nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (ADJ const-decl "nat" synch_constant_definitions nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (T const-decl "int" interval_clocks nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (clock_nondecreasing formula-decl nil physical_clocks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (earliest_adjustment? const-decl "bool" virtual_clocks nil) (int_minus_int_is_int application-judgement "int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ADJ_ineq_h formula-decl nil synch_constant_definitions nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (nonoverlap_upper formula-decl nil interval_clocks nil) (NOT const-decl "[bool -> bool]" booleans nil) (latest_adjustment? const-decl "bool" virtual_clocks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (self_adjustment? const-decl "bool" virtual_clocks nil) (t_event_sequence application-judgement "event_sequence" virtual_clock_2 nil)) nil)) (t_cross 1 (t_cross-2 "" 3400002086 ("" (expand "cross_adjustment?") (("" (expand "t") (("" (skosimp*) (("" (prop) (("1" (expand "earliest_cross_adjustment?") (("1" (skosimp*) (("1" (expand "compatible?") (("1" (lemma "nonoverlap_lower") (("1" (inst - _ "1 + ADJ" _ _ _ "max(alpha_l, alpha_u) + pi_0") (("1" (inst?) (("1" (inst?) (("1" (expand* "ADJ") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil) nil shostak) (t_cross-1 nil 3399252034 ("" (expand "cross_adjustment?") (("" (expand "t") (("" (skosimp*) (("" (prop) (("1" (expand "earliest_cross_adjustment?") (("1" (skosimp*) (("1" (expand "compatible?") (("1" (lemma "nonoverlap_lower") (("1" (inst - _ "1 + ADJ" _ _ _ "max(alpha_l, alpha_u) + pi_0") (("1" (inst?) (("1" (expand* "id" "ADJ") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "latest_cross_adjustment?") (("2" (skosimp*) (("2" (lemma "nonoverlap_peers") (("2" (expand "compatible?") (("2" (inst - "T(k!1)" "1 + ADJ" _ _ _ "max(alpha_l, alpha_u) + pi_0") (("2" (inst?) (("2" (expand* "id" "ADJ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((t const-decl "real" interval_clocks nil) (rho formal-const-decl "nnreal" virtual_clock_2 nil) (nnreal type-eq-decl nil real_types nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (nonoverlap_lower formula-decl nil interval_clocks nil) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (p_max const-decl "posreal" synch_constant_definitions nil) (p_min const-decl "posreal" synch_constant_definitions nil) (weakly_accurate? const-decl "bool" interval_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (rate const-decl "posreal" physical_clocks nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (<= const-decl "bool" reals nil) (T const-decl "int" interval_clocks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(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) (nonneg_floor_is_nat application-judgement "nat" floor_ceil 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) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (ADJ const-decl "nat" synch_constant_definitions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (compatible? const-decl "bool" interval_clocks nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (earliest_cross_adjustment? const-decl "bool" virtual_clocks nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nonoverlap_peers formula-decl nil interval_clocks nil) (latest_cross_adjustment? const-decl "bool" virtual_clocks nil) (cross_adjustment? const-decl "bool" virtual_clocks nil) (t_event_sequence application-judgement "event_sequence" virtual_clock_2 nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil)) nil)) (VC_j 0 (VC_j-1 nil 3399368163 ("" (skosimp*) (("" (expand "VC2") (("" (expand "VC") (("" (rewrite "index_rewrite") (("" (expand "t") (("" (rewrite "Clock_rewrite") nil nil)) nil)) nil)) nil)) nil)) nil) ((VC2 const-decl "int" virtual_clock_2 nil) (t_event_sequence application-judgement "event_sequence" virtual_clock_2 nil) (index_rewrite formula-decl nil event_sequences 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) (increasing? const-decl "bool" event_sequences nil) (unbounded? const-decl "bool" event_sequences nil) (event_sequence type-eq-decl nil event_sequences 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" virtual_clock_2 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (interval_clock type-eq-decl nil interval_clocks nil) (t const-decl "real" interval_clocks nil) (weakly_accurate? const-decl "bool" interval_clocks nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (p_min const-decl "posreal" synch_constant_definitions nil) (p_max const-decl "posreal" synch_constant_definitions nil) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (T const-decl "int" interval_clocks nil) (Clock_rewrite formula-decl nil inverse_clocks nil) (VC const-decl "int" virtual_clocks nil)) shostak)) (VC2_precision_TCC1 0 (VC2_precision_TCC1-3 nil 3399248158 ("" (skosimp*) (("" (hide -4) (("" (use "trace_weakly_accurate") (("" (assert) nil nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (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) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (interval_clock type-eq-decl nil interval_clocks nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (rho formal-const-decl "nnreal" virtual_clock_2 nil) (nnreal type-eq-decl nil real_types nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (trace_weakly_accurate formula-decl nil synch_protocol_invariants nil)) nil) (VC2_precision_TCC1-2 nil 3399070466 ("" (skosimp*) (("" (use "trace_weakly_accurate") (("" (assert) nil nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets 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) (P_bound? const-decl "bool" synch_parameter_constraints nil) (p_lower const-decl "posreal" synch_constant_definitions nil) (p_upper const-decl "posreal" synch_constant_definitions nil)) nil) (VC2_precision_TCC1-1 nil 3399070054 ("" (subtype-tcc) nil nil) nil nil)) (VC2_precision_TCC2 0 (VC2_precision_TCC2-3 nil 3399248168 ("" (skosimp*) (("" (use "trace_weakly_accurate") (("" (assert) nil nil)) nil)) nil) ((trace_weakly_accurate formula-decl nil synch_protocol_invariants 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) (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" virtual_clock_2 nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (nnreal type-eq-decl nil real_types nil) (rho formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (interval_clock type-eq-decl nil interval_clocks nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets 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) (/ 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (VC2_precision_TCC2-2 nil 3399070478 ("" (skosimp*) (("" (use "trace_weakly_accurate") (("" (assert) nil nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets 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) (P_bound? const-decl "bool" synch_parameter_constraints nil) (p_lower const-decl "posreal" synch_constant_definitions nil) (p_upper const-decl "posreal" synch_constant_definitions nil)) nil) (VC2_precision_TCC2-1 nil 3399070054 ("" (subtype-tcc) nil nil) nil nil)) (VC2_precision 0 (VC2_precision-1 nil 3399070370 ("" (skosimp*) (("" (lemma "trace_weakly_accurate") (("" (inst-cp - _ "ic2!1") (("" (inst - _ "ic1!1") (("" (inst?) (("" (inst?) (("" (assert) (("" (expand "VC2") (("" (lemma "VC_precision") (("" (inst - "ADJ + 1" "max(alpha_l, alpha_u) + pi_0" "t(ic1!1)" "t(ic2!1)" "ic1!1" "ic2!1" "t1!1") (("" (expand "Pi") (("" (expand "P_max") (("" (assert) (("" (hide 2) (("" (lemma "traces_compatible") (("" (inst - "alpha_l" "alpha_u" "hst!1" _ _ "pi_0") (("" (inst-cp - "ic1!1" "ic2!1") (("" (inst - "ic2!1" "ic1!1") (("" (assert) (("" (expand "p_lower") (("" (expand "p_upper") (("" (assert) (("" (rewrite "t_self") (("" (rewrite "t_self") (("" (rewrite "t_cross") (("" (rewrite "t_cross") (("" (rewrite "t_nonoverlap") (("" (rewrite "t_nonoverlap") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (rho formal-const-decl "nnreal" virtual_clock_2 nil) (nnreal type-eq-decl nil real_types nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (trace_weakly_accurate formula-decl nil synch_protocol_invariants nil) (VC2 const-decl "int" virtual_clock_2 nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (t const-decl "real" interval_clocks nil) (event_sequence type-eq-decl nil event_sequences nil) (unbounded? const-decl "bool" event_sequences nil) (increasing? const-decl "bool" event_sequences nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (ADJ const-decl "nat" synch_constant_definitions nil) (P_max const-decl "posnat" synch_constant_definitions nil) (p_lower const-decl "posreal" synch_constant_definitions nil) (t_nonoverlap formula-decl nil virtual_clock_2 nil) (t_cross formula-decl nil virtual_clock_2 nil) (t_self formula-decl nil virtual_clock_2 nil) (weakly_accurate? const-decl "bool" interval_clocks nil) (p_min const-decl "posreal" synch_constant_definitions nil) (p_max const-decl "posreal" synch_constant_definitions nil) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (p_upper const-decl "posreal" synch_constant_definitions nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (traces_compatible formula-decl nil synch_protocol_invariants nil) (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (Pi const-decl "int" virtual_clocks nil) (Pi const-decl "posnat" synch_constant_definitions nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (VC_precision formula-decl nil virtual_clocks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets 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) (/ 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_minus_int_is_int application-judgement "int" integers nil)) nil)) (VC2_accuracy_lower_TCC1 0 (VC2_accuracy_lower_TCC1-3 nil 3399248179 ("" (skosimp*) (("" (use "trace_weakly_accurate") (("" (assert) nil nil)) nil)) nil) ((trace_weakly_accurate formula-decl nil synch_protocol_invariants 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) (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" virtual_clock_2 nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (nnreal type-eq-decl nil real_types nil) (rho formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (interval_clock type-eq-decl nil interval_clocks nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets 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) (/ 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (VC2_accuracy_lower_TCC1-2 nil 3399070488 ("" (skosimp*) (("" (use "trace_weakly_accurate") (("" (assert) nil nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets 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) (P_bound? const-decl "bool" synch_parameter_constraints nil) (p_lower const-decl "posreal" synch_constant_definitions nil) (p_upper const-decl "posreal" synch_constant_definitions nil)) nil) (VC2_accuracy_lower_TCC1-1 nil 3399070054 ("" (subtype-tcc) nil nil) nil nil)) (VC2_accuracy_lower 0 (VC2_accuracy_lower-1 nil 3399070391 ("" (skosimp*) (("" (typepred "p_lower") (("" (use "trace_weakly_accurate") (("" (assert) (("" (assert) (("" (expand "p_lower") (("" (expand "p_upper") (("" (use "trace_lower_accuracy") (("" (use "trace_upper_accuracy") (("" (prop) (("" (expand "VC2") (("" (use "t_early") (("" (lemma "VC_lower_accuracy") (("" (inst?) (("" (inst - "0" "alpha_l" "alpha_u" "p_lower" "pi_0") (("" (rewrite "p_lower" :dir rl) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((p_lower const-decl "posreal" synch_constant_definitions nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (rho formal-const-decl "nnreal" virtual_clock_2 nil) (nnreal type-eq-decl nil real_types nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (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 "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (trace_lower_accuracy formula-decl nil synch_protocol_invariants nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (t_early formula-decl nil virtual_clock_2 nil) (weakly_accurate? const-decl "bool" interval_clocks nil) (p_min const-decl "posreal" synch_constant_definitions nil) (p_max const-decl "posreal" synch_constant_definitions nil) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (t const-decl "real" interval_clocks nil) (event_sequence type-eq-decl nil event_sequences nil) (unbounded? const-decl "bool" event_sequences nil) (increasing? const-decl "bool" event_sequences nil) (VC_lower_accuracy formula-decl nil virtual_clocks nil) (VC2 const-decl "int" virtual_clock_2 nil) (trace_upper_accuracy formula-decl nil synch_protocol_invariants nil) (p_upper const-decl "posreal" synch_constant_definitions 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) (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) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (interval_clock type-eq-decl nil interval_clocks nil) (trace_weakly_accurate formula-decl nil synch_protocol_invariants nil)) nil)) (VC2_optimal_accuracy_lower 0 (VC2_optimal_accuracy_lower-1 nil 3399070405 ("" (skosimp*) (("" (use "VC2_accuracy_lower") (("" (assert) nil nil)) nil)) nil) ((VC2_accuracy_lower formula-decl nil virtual_clock_2 nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (P formal-const-decl "posnat" virtual_clock_2 nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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" virtual_clock_2 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) (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) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (VC2_accuracy_upper 0 (VC2_accuracy_upper-1 nil 3399070420 ("" (skosimp*) (("" (use "p_lower") (("" (use "trace_weakly_accurate") (("" (assert) (("" (expand "VC2") (("" (expand "p_lower" -5) (("" (use "trace_lower_accuracy") (("" (assert) (("" (use "t_early") (("" (lemma "VC_upper_accuracy") (("" (inst?) (("" (inst - "0" "alpha_l" "p_lower" "pi_0") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((p_lower const-decl "posreal" synch_constant_definitions 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) (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" virtual_clock_2 nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (nnreal type-eq-decl nil real_types nil) (rho formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_l formal-const-decl "nnreal" virtual_clock_2 nil) (alpha_u formal-const-decl "nnreal" virtual_clock_2 nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" virtual_clock_2 nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (VC_upper_accuracy formula-decl nil virtual_clocks nil) (increasing? const-decl "bool" event_sequences nil) (unbounded? const-decl "bool" event_sequences nil) (event_sequence type-eq-decl nil event_sequences nil) (t const-decl "real" interval_clocks nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (weakly_accurate_clock type-eq-decl nil synch_protocol_invariants nil) (p_max const-decl "posreal" synch_constant_definitions nil) (p_min const-decl "posreal" synch_constant_definitions nil) (weakly_accurate? const-decl "bool" interval_clocks nil) (t_early formula-decl nil virtual_clock_2 nil) (p_upper const-decl "posreal" synch_constant_definitions nil) (trace_lower_accuracy formula-decl nil synch_protocol_invariants nil) (VC2 const-decl "int" virtual_clock_2 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) (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) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (interval_clock type-eq-decl nil interval_clocks nil) (trace_weakly_accurate formula-decl nil synch_protocol_invariants nil)) nil)) (VC2_optimal_accuracy_upper 0 (VC2_optimal_accuracy_upper-1 nil 3399070440 ("" (skosimp*) (("" (use "VC2_accuracy_upper") (("" (assert) nil nil)) nil)) nil) ((VC2_accuracy_upper formula-decl nil virtual_clock_2 nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" virtual_clock_2 nil) (P formal-const-decl "posnat" virtual_clock_2 nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.91 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 |
