|
(timing_imprecision
(mid_latency_ge_one_half 0
(mid_latency_ge_one_half-1 nil 3393765710
("" (expand "mid_latency")
(("" (expand "epsilon") (("" (assert) nil nil)) nil)) nil)
((posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(epsilon const-decl "posreal" timing_imprecision 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)
(mid_latency const-decl "posreal" timing_imprecision nil))
nil))
(W_TCC1 0
(W_TCC1-1 nil 3393765366 ("" (subtype-tcc) nil nil)
((epsilon const-decl "posreal" timing_imprecision nil)
(mid_latency const-decl "posreal" timing_imprecision nil)
(fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(W_TCC2 0
(W_TCC2-1 nil 3393765366 ("" (subtype-tcc) nil nil)
((nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(epsilon const-decl "posreal" timing_imprecision nil)
(mid_latency const-decl "posreal" timing_imprecision nil)
(fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(drift_relation_alt 0
(drift_relation_alt-1 nil 3393765728
("" (skosimp*)
(("" (splash 1)
(("1" (cross-mult) nil nil)
("2" (cross-mult)
(("2" (expand "rate") (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
((nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types 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)
(bool nonempty-type-eq-decl nil 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)
(>= 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)
(rho formal-const-decl "nonneg_real" timing_imprecision nil)
(rate const-decl "posreal" physical_clocks nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil))
(W_bound 0
(W_bound-1 nil 3393765744
("" (auto-rewrite-defs)
(("" (assert)
(("" (expand "W")
(("" (lift-if)
(("" (assert)
(("" (prop)
(("1" (use "ceiling_def") (("1" (assert) nil nil)) nil)
("2"
(invoke (then (case "%1 >= %2") (assert)) (! 1 l)
(! 1 r))
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(epsilon const-decl "posreal" timing_imprecision nil)
(mid_latency const-decl "posreal" timing_imprecision nil)
(fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
(max_latency const-decl "posreal" timing_imprecision nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
(int_minus_int_is_int application-judgement "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)
(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 "[numfield, numfield -> numfield]" 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(rho formal-const-decl "nonneg_real" timing_imprecision nil)
(var_latency formal-const-decl "nonneg_real" timing_imprecision
nil)
(min_latency formal-const-decl "nonneg_real" timing_imprecision
nil)
(ceiling_def formula-decl nil floor_ceil nil)
(ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil 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)
(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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(W const-decl "posint" timing_imprecision nil))
nil))
(W_bound_alt 0
(W_bound_alt-1 nil 3393765758
("" (use "W_bound")
(("" (use "drift_relation_alt")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil)
((drift_relation_alt formula-decl nil timing_imprecision nil)
(W const-decl "posint" timing_imprecision nil)
(posint 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)
(posreal_div_posreal_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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(W_bound formula-decl nil timing_imprecision nil))
nil))
(epsilon_l_TCC1 0
(epsilon_l_TCC1-2 nil 3393765840
("" (use "W_bound_alt") (("" (flatten) (("" (assert) nil nil)) nil))
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)
(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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(W_bound_alt formula-decl nil timing_imprecision nil))
nil)
(epsilon_l_TCC1-1 nil 3393765366 ("" (subtype-tcc) nil nil) nil nil))
(epsilon_u_TCC1 0
(epsilon_u_TCC1-2 nil 3393765860
("" (use "W_bound_alt") (("" (flatten) (("" (assert) nil nil)) nil))
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)
(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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(W_bound_alt formula-decl nil timing_imprecision nil))
nil)
(epsilon_u_TCC1-1 nil 3393765366 ("" (subtype-tcc) nil nil) nil nil))
(max_error_TCC1 0
(max_error_TCC1-1 nil 3393765366 ("" (subtype-tcc) nil nil)
((epsilon const-decl "posreal" timing_imprecision nil)
(mid_latency const-decl "posreal" timing_imprecision nil)
(fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
(rho formal-const-decl "nonneg_real" timing_imprecision 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)
(rate const-decl "posreal" physical_clocks nil)
(epsilon_l const-decl "posreal" timing_imprecision nil)
(max_latency const-decl "posreal" timing_imprecision nil)
(epsilon_u const-decl "nnreal" timing_imprecision nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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_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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil))
(epsilon_relation 0
(epsilon_relation-1 nil 3393765810
("" (expand "epsilon_l")
(("" (expand "epsilon_u")
(("" (expand "max_latency")
(("" (expand "drift") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(epsilon_u const-decl "nnreal" timing_imprecision nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(max_latency const-decl "posreal" timing_imprecision nil)
(epsilon_l const-decl "posreal" timing_imprecision nil))
nil))
(event_observation_error 0
(event_observation_error-1 nil 3393765420
("" (skosimp*)
(("" (prop)
(("1" (expand "Timestamp")
(("1" (use "Clock_upper") (("1" (assert) nil nil)) nil)) nil)
("2" (expand "Timestamp")
(("2" (use "Clock_lower")
(("2" (lemma "drift_right")
(("2" (invoke (inst - "%1" "%2" _) (! -2 l 1) (! 1 l 1))
(("2" (inst?)
(("2" (expand "rate") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Clock_upper formula-decl nil inverse_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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(rho formal-const-decl "nonneg_real" timing_imprecision 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals 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)
(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)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Timestamp const-decl "integer" timing_imprecision nil)
(Clock_lower formula-decl nil inverse_clocks nil)
(C const-decl "int" inverse_clocks nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(drift_right formula-decl nil physical_clocks nil))
nil))
(link_lower_range 0
(link_lower_range-1 nil 3393765446
("" (skosimp*)
(("" (expand* "good_range" "Timestamp")
(("" (use "Clock_upper")
(("" (flatten)
((""
(invoke (then (case "%1 <= %2") (assert)) (! 1 l) (! -2 l))
(("" (hide-all-but 1)
(("" (isolate 1 l 1)
(("" (move-terms 1 r 1)
(("" (expand "epsilon_l")
(("" (lemma "drift_right")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Timestamp const-decl "integer" timing_imprecision nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(good_range const-decl "set[real]" timing_imprecision nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(drift_right formula-decl nil physical_clocks nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(IFF const-decl "[bool, bool -> bool]" booleans 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)
(integer nonempty-type-from-decl nil integers nil)
(epsilon_l const-decl "posreal" timing_imprecision nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posint nonempty-type-eq-decl nil integers nil)
(W const-decl "posint" timing_imprecision nil)
(min_latency formal-const-decl "nonneg_real" timing_imprecision
nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(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)
(> const-decl "bool" reals 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(rho formal-const-decl "nonneg_real" timing_imprecision 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)
(Clock_upper formula-decl nil inverse_clocks nil))
nil))
(link_upper_range 0
(link_upper_range-1 nil 3393765471
("" (skosimp*)
(("" (expand* "good_range" "Timestamp")
(("" (use "Clock_lower")
(("" (flatten)
(("" (lemma "drift_right")
(("" (invoke (inst - "%1" "%2" _) (! -2 l 1) (! 1 l 1))
(("" (inst?)
(("" (assert)
((""
(invoke (then (case "%1 + %2 <= %3") (assert))
(! -4 r) (! -1 r) (! 1 r))
(("" (hide-all-but 1)
(("" (isolate 1 r 1)
(("" (move-terms 1 l 1)
((""
(expand* "epsilon_u" "max_latency"
"epsilon" "rate")
(("" (lemma "drift_left")
((""
(inst?)
((""
(expand*
"epsilon_u"
"max_latency"
"epsilon"
"rate")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Timestamp const-decl "integer" timing_imprecision nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(good_range const-decl "set[real]" timing_imprecision nil)
(C const-decl "int" inverse_clocks nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(drift_left formula-decl nil physical_clocks nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(epsilon const-decl "posreal" timing_imprecision nil)
(max_latency const-decl "posreal" timing_imprecision nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(integer nonempty-type-from-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posint nonempty-type-eq-decl nil integers nil)
(W const-decl "posint" timing_imprecision nil)
(min_latency formal-const-decl "nonneg_real" timing_imprecision
nil)
(var_latency formal-const-decl "nonneg_real" timing_imprecision
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(epsilon_u const-decl "nnreal" timing_imprecision nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(drift_right formula-decl nil physical_clocks 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)
(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)
(> const-decl "bool" reals 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(rho formal-const-decl "nonneg_real" timing_imprecision 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)
(Clock_lower formula-decl nil inverse_clocks nil))
nil))
(link_abs_bound 0
(link_abs_bound-1 nil 3495923645
("" (skosimp*)
(("" (use "link_lower_range")
(("" (use "link_upper_range")
(("" (expand "max_error")
(("" (expand "abs")
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((link_lower_range formula-decl nil timing_imprecision 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 "nonneg_real" timing_imprecision 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)
(/ 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)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer nonempty-type-from-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)
(int_plus_int_is_int application-judgement "int" integers nil)
(max_error const-decl "posreal" timing_imprecision nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(minus_real_is_real application-judgement "real" reals 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(link_upper_range formula-decl nil timing_imprecision nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(link_relative_range 0
(link_relative_range-1 nil 3393765492
("" (skosimp*)
(("" (lemma "event_observation_error")
(("" (inst-cp - "c2!1" "ev2r!1")
(("" (inst - "c1!1" "ev1r!1")
(("" (expand "good_range")
(("" (flatten)
(("" (rewrite "abs_max")
(("" (rewrite "max_le")
(("" (expand "epsilon") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((event_observation_error formula-decl nil timing_imprecision nil)
(epsilon const-decl "posreal" timing_imprecision nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(max_le formula-decl nil minmax_ineq 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)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(abs_max formula-decl nil abs_props nil)
(integer nonempty-type-from-decl nil integers nil)
(Timestamp const-decl "integer" timing_imprecision nil)
(good_range const-decl "set[real]" timing_imprecision 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 "nonneg_real" timing_imprecision 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)
(/ 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)
(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_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(link_relative_symmetry 0
(link_relative_symmetry-1 nil 3393765545
("" (skosimp*)
(("" (use "link_relative_range") (("" (assert) nil nil)) nil)) nil)
((link_relative_range formula-decl nil timing_imprecision 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 "nonneg_real" timing_imprecision 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)
(/ 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)
(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_plus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(good_range_bounded 0
(good_range_bounded-1 nil 3393765575
("" (skosimp*)
(("" (expand "good_range")
(("" (flatten)
(("" (rewrite "abs_max")
(("" (rewrite "max_le") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(good_range const-decl "set[real]" timing_imprecision nil)
(abs_max formula-decl nil abs_props 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 "[numfield, numfield -> numfield]" number_fields nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(var_latency formal-const-decl "nonneg_real" timing_imprecision
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]" number_fields nil)
(max_le formula-decl nil minmax_ineq nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(link_symmetry 0
(link_symmetry-1 nil 3393765592
("" (skosimp*)
(("" (rewrite "abs_max")
(("" (rewrite "max_le")
(("" (rewrite "abs_max")
(("" (rewrite "max_le")
(("" (lemma "event_observation_error")
(("" (inst-cp - "c1!1" "ev1!1")
(("" (inst - "c2!1" "ev2!1")
(("" (expand "epsilon")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_max formula-decl nil abs_props 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 "[numfield, numfield -> numfield]" number_fields nil)
(minus_real_is_real application-judgement "real" 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)
(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)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(rho formal-const-decl "nonneg_real" timing_imprecision 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)
(integer nonempty-type-from-decl nil integers nil)
(Timestamp const-decl "integer" timing_imprecision nil)
(event_observation_error formula-decl nil timing_imprecision 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)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(epsilon const-decl "posreal" timing_imprecision nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(var_latency formal-const-decl "nonneg_real" timing_imprecision
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]" number_fields nil)
(max_le formula-decl nil minmax_ineq nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)))
¤ Dauer der Verarbeitung: 0.32 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.
|
