| products/sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: synch_constant_definitions.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(synch_constant_definitions
(P_bound 0 (P_bound-1 nil 3292973572 ("" (auto-rewrite-defs) (("" (typepred "pi_0") (("" (assert) nil nil)) nil)) nil) ((pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" synch_constant_definitions nil) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (rho formal-const-decl "nnreal" synch_constant_definitions nil) (nnreal type-eq-decl nil real_types nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (P_bound? const-decl "bool" synch_parameter_constraints 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_ge_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) (real_times_real_is_real application-judgement "real" reals nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (real_minus_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) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (drift const-decl "nonneg_real" physical_clocks nil) (rate const-decl "posreal" physical_clocks nil)) shostak)) (rho_bound 0 (rho_bound-1 nil 3292974283 ("" (lemma "P_bound") (("" (mult-by 1 "P") (("" (invoke (then (case "%1 <= %2") (assert)) (! 1 l) (! -1 l)) (("" (hide-all-but 1) (("" (expand* "drift" "rate" "id") (("" (field 1) nil nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rho formal-const-decl "nnreal" synch_constant_definitions nil) (nnreal type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (nonneg_real nonempty-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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (< const-decl "bool" reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_plus_le2 formula-decl nil real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (rate const-decl "posreal" physical_clocks nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" 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) (drift const-decl "nonneg_real" physical_clocks nil) (P_bound formula-decl nil synch_constant_definitions nil)) shostak)) (ADJ_ineq 0 (ADJ_ineq-1 nil 3381419890 ("" (swap-rel +) (("" (expand "ADJ") (("" (rewrite "floor_monotone") nil nil)) nil)) nil) ((nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (floor_monotone formula-decl nil floor_ceiling_ineq nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rate const-decl "posreal" physical_clocks nil) (pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" synch_constant_definitions nil) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (posreal nonempty-type-eq-decl nil real_types nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (drift const-decl "nonneg_real" physical_clocks nil) (rho formal-const-decl "nnreal" synch_constant_definitions nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (ADJ const-decl "nat" synch_constant_definitions 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) (>= 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) (IFF const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (ADJ_ineq_l 0 (ADJ_ineq_l-1 nil 3381419661 ("" (swap-rel +) (("" (expand "ADJ") (("" (rewrite "floor_monotone") (("" (hide 2) (("" (cancel-by 1 "rate") nil nil)) nil)) nil)) nil)) nil) ((nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (floor_monotone formula-decl nil floor_ceiling_ineq nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rate const-decl "posreal" physical_clocks nil) (pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" synch_constant_definitions nil) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (posreal nonempty-type-eq-decl nil real_types nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (drift const-decl "nonneg_real" physical_clocks nil) (rho formal-const-decl "nnreal" synch_constant_definitions nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (ADJ const-decl "nat" synch_constant_definitions 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) (>= 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) (IFF const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posreal_times_posreal_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)) nil)) (ADJ_ineq_h 0 (ADJ_ineq_h-1 nil 3381419694 ("" (swap-rel +) (("" (expand "ADJ") (("" (rewrite "floor_monotone") (("" (hide 2) (("" (cancel-by 1 "rate") nil nil)) nil)) nil)) nil)) nil) ((nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (floor_monotone formula-decl nil floor_ceiling_ineq nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rate const-decl "posreal" physical_clocks nil) (pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" synch_constant_definitions nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (posreal nonempty-type-eq-decl nil real_types nil) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (drift const-decl "nonneg_real" physical_clocks nil) (rho formal-const-decl "nnreal" synch_constant_definitions nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (ADJ const-decl "nat" synch_constant_definitions 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) (>= 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) (IFF const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posreal_times_posreal_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)) nil)) (ADJ_bound 0 (ADJ_bound-1 nil 3292973792 ("" (lemma "P_bound") (("" (expand* "ADJ" "id") (("" (assert) nil nil)) nil)) nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (ADJ const-decl "nat" synch_constant_definitions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (P_bound formula-decl nil synch_constant_definitions nil)) shostak)) (P_min_TCC1 0 (P_min_TCC1-1 nil 3292975885 ("" (use "ADJ_bound") (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_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) (ADJ_bound formula-decl nil synch_constant_definitions nil)) shostak)) (p_min_bound 0 (p_min_bound-1 nil 3292982433 ("" (lemma "P_bound") (("" (assert) (("" (assert) nil nil)) nil)) nil) ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" 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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (P_bound formula-decl nil synch_constant_definitions nil)) shostak)) (p_lower_TCC1 0 (p_lower_TCC1-1 nil 3292982874 ("" (invoke (then (case "%1") (assert)) (! 1 2)) (("" (hide 2) (("" (move-terms 1 l 2) (("" (cross-mult) (("" (lemma "p_min_bound") (("" (assert) (("" (expand "max") (("" (lift-if) (("" (prop) (("1" (div-by (-2 1) "rate") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_gt1 formula-decl nil extra_real_props 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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" synch_constant_definitions nil) (both_sides_div_pos_gt1 formula-decl nil real_props nil) (times_div_cancel2 formula-decl nil extra_real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (p_min_bound formula-decl nil synch_constant_definitions nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_constant_definitions nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (p_min_TCC1 0 (p_min_TCC1-1 nil 3292983076 ("" (invoke (then (case "%1") (assert)) (! 1 2)) (("" (hide 2) (("" (isolate 1 l 1) (("" (cross-mult) (("" (lemma "p_min_bound") (("" (expand "id") (("" (assert) (("" (expand "max") (("" (lift-if) (("" (assert) (("" (prop) (("" (div-by (-2 1) "rate") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_gt1 formula-decl nil extra_real_props 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_div_pos_gt1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (p_min_bound formula-decl nil synch_constant_definitions nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" synch_constant_definitions nil) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_constant_definitions nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (p_min_lower 0 (p_min_lower-1 nil 3399247956 ("" (expand "p_min") (("" (expand "p_lower") (("" (propax) nil nil)) nil)) nil) ((p_lower const-decl "posreal" synch_constant_definitions nil) (p_min const-decl "posreal" synch_constant_definitions nil)) shostak)) (p_max_upper 0 (p_max_upper-1 nil 3399247972 ("" (expand "p_max") (("" (expand "p_upper") (("" (propax) nil nil)) nil)) nil) ((p_upper const-decl "posreal" synch_constant_definitions nil) (p_max const-decl "posreal" synch_constant_definitions nil)) shostak)) (drift_P_bound 0 (drift_P_bound-1 nil 3293977788 ("" (expand "p_min") (("" (lemma "P_bound") (("" (isolate 1 r 1) (("" (cross-mult) (("" (invoke (then (case "%1 <= %2") (assert)) (! 1 l) (! -1 l)) (("" (hide-all-but 1) (("" (assert) (("" (expand "max") (("" (lift-if) (("" (assert) (("" (expand "id") (("" (prop) (("" (assert) (("" (isolate 1 l 2) (("" (assert) (("" (cancel) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((P_bound formula-decl nil synch_constant_definitions nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" synch_constant_definitions nil) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (rate const-decl "posreal" physical_clocks nil) (posreal 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (drift const-decl "nonneg_real" physical_clocks nil) (rho formal-const-decl "nnreal" synch_constant_definitions nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (IFF const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (p_min const-decl "posreal" synch_constant_definitions nil)) nil)) (Pi_TCC1 0 (Pi_TCC1-1 nil 3293064140 ("" (rewrite "gt_ceiling_l") (("" (expand "id") (("" (assert) nil nil)) nil)) 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (integer nonempty-type-from-decl nil integers nil) (P_max const-decl "posnat" synch_constant_definitions nil) (drift const-decl "nonneg_real" physical_clocks nil) (pi_0 formal-const-decl "{pi: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi)}" synch_constant_definitions nil) (P formal-const-decl "posnat" synch_constant_definitions nil) (P_bound? const-decl "bool" synch_parameter_constraints 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) (alpha_u formal-const-decl "nnreal" synch_constant_definitions nil) (alpha_l formal-const-decl "nnreal" synch_constant_definitions nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_constant_definitions 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 "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (gt_ceiling_l formula-decl nil floor_ceiling_ineq nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak))) ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
