|
(interval_clocks
(T_def 0
(T_def-1 nil 3381399668 ("" (expand "T") (("" (propax) nil nil)) nil)
((T const-decl "int" interval_clocks nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_plus_int_is_int application-judgement "int" integers nil))
shostak))
(T_rounds 0
(T_rounds-1 nil 3381399683
("" (expand "T") (("" (propax) nil nil)) nil)
((T const-decl "int" interval_clocks nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil))
shostak))
(handover_precision_lower 0
(handover_precision_lower-1 nil 3399129068
("" (skosimp*)
(("" (expand "adjustment_lower_bound?")
(("" (expand "t")
(("" (inst?)
(("" (lemma "drift_right")
(("" (inst - "T(j!1)" "T(j!1+1)" "ic1!1(j!1)")
(("" (rewrite "T_def")
(("" (rewrite "drift") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(adjustment_lower_bound? const-decl "bool" interval_clocks nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T const-decl "int" interval_clocks nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(rate const-decl "posreal" physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(T_def formula-decl nil interval_clocks nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(nnreal type-eq-decl nil real_types nil)
(drift_right formula-decl nil physical_clocks nil)
(t const-decl "real" interval_clocks nil))
nil))
(handover_precision_upper 0
(handover_precision_upper-1 nil 3399129088
("" (skosimp*)
(("" (expand "adjustment_upper_bound?")
(("" (expand "t")
(("" (inst?)
(("" (lemma "drift_left")
(("" (inst - "T(j!1)" "T(j!1+1)" "ic1!1(j!1)")
(("" (rewrite "T_def")
(("" (rewrite "drift") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(adjustment_upper_bound? const-decl "bool" interval_clocks nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T const-decl "int" interval_clocks nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(rate const-decl "posreal" physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(T_def formula-decl nil interval_clocks nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(nnreal type-eq-decl nil real_types nil)
(drift_left formula-decl nil physical_clocks nil)
(t const-decl "real" interval_clocks nil))
nil))
(handover_precision 0
(handover_precision-1 nil 3399129148
("" (skosimp*)
(("" (expand "abs")
(("" (lift-if)
(("" (rewrite "handover_precision_lower")
(("" (use "handover_precision_upper") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(handover_precision_lower formula-decl nil interval_clocks nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(rate const-decl "posreal" physical_clocks nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(minus_real_is_real application-judgement "real" reals nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(handover_precision_upper formula-decl nil interval_clocks nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(nonoverlap_peers 0
(nonoverlap_peers-3 "" 3381397883
("" (skosimp*)
(("" (expand "peer_precision?")
(("" (expand "t")
(("" (inst?)
(("" (lemma "skew_bound_1")
((""
(inst - "T(j!1)" "T1!1" "T1!1 + X!1" "P" "ic1!1(j!1)"
"ic2!1(j!1)" "pi!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((peer_precision? const-decl "bool" interval_clocks nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(T const-decl "int" interval_clocks nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(P formal-const-decl "posnat" interval_clocks nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(rate const-decl "posreal" physical_clocks nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(nnreal type-eq-decl nil real_types nil)
(skew_bound_1 formula-decl nil physical_clocks nil)
(t const-decl "real" interval_clocks nil))
shostak)
(nonoverlap_peers-2 nil 3315403635
("" (skosimp*)
(("" (expand "peer_precision?")
(("" (inst?)
(("" (rewrite "T_def")
(("" (lemma "proper_separation")
((""
(inst - "T(j!1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1)"
"0" "pi_0")
(("" (assert)
(("" (hide 2 -1)
((""
(invoke (then (case "%1 <= ADJ") (assert)) (! 1 r))
(("" (hide 2 -3)
(("" (expand "ADJ")
(("" (rewrite "floor_monotone")
(("" (hide 2)
(("" (cancel)
((""
(invoke
(then (case "%1 <= %2") (assert))
(! 1 l)
(! 1 r 2))
((""
(hide 2)
((""
(cancel)
((""
(cancel)
((""
(rewrite "max_le")
((""
(rewrite "max_le")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rate const-decl "posreal" physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(floor_monotone formula-decl nil floor_ceiling_ineq nil)
(max_le formula-decl nil minmax_ineq nil)
(drift const-decl "nonneg_real" physical_clocks nil))
nil)
(nonoverlap_peers-1 nil 3294485333
("" (skosimp*)
(("" (lemma "proper_separation")
((""
(inst - "T(j!1)" "T1!1" "T2!1" "ic1!1(j!1)" "ic2!1(j!1)" "0"
"delta_0")
(("" (assert)
(("" (prop)
(("1" (expand "peer_precision?")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2 -1)
(("2" (invoke (then (case "%1 <=ADJ") (assert)) (! 1 r))
(("2" (hide 2 -3)
(("2" (expand "ADJ")
(("2" (rewrite "floor_monotone")
(("2" (hide 2)
(("2" (div-by 1 "id(1 + rho)")
(("2" (expand "id")
(("2" (move-terms 1 l 2)
(("2"
(assert)
(("2"
(invoke
(then (case "%1 <= %2") (assert))
(! 1 l)
(! 1 r 2))
(("2"
(hide 2)
(("2"
(div-by 1 "drift")
(("2"
(rewrite "max_le")
(("2"
(rewrite "max_le")
(("2"
(rewrite "T_def")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((good_clock nonempty-type-eq-decl nil physical_clocks nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(floor_monotone formula-decl nil floor_ceiling_ineq nil))
nil))
(nonoverlap_lower 0
(nonoverlap_lower-3 nil 3365507387
("" (skosimp*)
(("" (use "handover_precision_lower")
(("" (assert)
(("" (lemma "nonoverlap_basis")
((""
(inst - _ "T1!1" "T1!1 + X!1" _ "ic1!1(j!1)"
"ic2!1(1 + j!1)")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((handover_precision_lower formula-decl nil interval_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonoverlap_basis formula-decl nil physical_clocks nil)
(P formal-const-decl "posnat" interval_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T const-decl "int" interval_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil)
(nonoverlap_lower-2 nil 3315403714
("" (skosimp*)
(("" (lemma "proper_separation")
((""
(inst - "T(j!1 + 1)" "T1!1" "T2!1" "ic1!1(j!1)"
"ic2!1(j!1 + 1)" "0" "drift * P + pi_0 + alpha_l")
(("" (assert)
(("" (prop)
(("1" (forward-chain "handover_precision_lower")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2 -1)
(("2" (invoke (then (case "%1 <= ADJ") (assert)) (! 1 r))
(("2" (hide 2 -3)
(("2" (expand "ADJ")
(("2" (rewrite "floor_monotone")
(("2" (hide 2)
(("2" (expand "id")
(("2" (cancel)
(("2" (isolate 1 l 1)
(("2"
(assert)
(("2"
(factor 1)
(("2"
(div-by 1 "rate")
(("2"
(invoke
(case "%1 <= 0")
(! 1 l 1))
(("1"
(mult-by -1 "drift")
(("1" (assert) nil nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "max_le")
(("2"
(rewrite "max_le")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((floor_monotone formula-decl nil floor_ceiling_ineq nil)
(max_le formula-decl nil minmax_ineq nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(rate const-decl "posreal" physical_clocks nil))
nil)
(nonoverlap_lower-1 nil 3294485363
("" (skosimp*)
(("" (lemma "proper_separation")
((""
(inst - "T(j!1 + 1)" "T1!1" "T2!1" "ic1!1(j!1)"
"ic2!1(j!1 + 1)" "0" "drift * P + delta_0 + epsilon_l")
(("" (assert)
(("" (prop)
(("1" (forward-chain "handover_precision_lower")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2 -1)
(("2" (invoke (then (case "%1 <= ADJ") (assert)) (! 1 r))
(("2" (hide 2 -3)
(("2" (expand "ADJ")
(("2" (rewrite "floor_monotone")
(("2" (hide 2)
(("2" (div-by 1 "id(1 + rho)")
(("2" (expand "id")
(("2" (move-terms 1 l (2 3))
(("2"
(assert)
(("2"
(invoke (case "%1 <= 0") (! 1 l 1 2))
(("1"
(mult-by -1 "drift")
(("1" (assert) nil nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "max_le")
(("2"
(rewrite "max_le")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((good_clock nonempty-type-eq-decl nil physical_clocks nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(floor_monotone formula-decl nil floor_ceiling_ineq nil))
nil))
(nonoverlap_upper 0
(nonoverlap_upper-2 nil 3365507440
("" (skosimp*)
(("" (use "handover_precision_upper")
(("" (assert)
(("" (lemma "nonoverlap_basis")
((""
(inst - _ "T1!1" "T1!1 + X!1" _ "ic2!1(1 + j!1)"
"ic1!1(j!1)")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((handover_precision_upper formula-decl nil interval_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonoverlap_basis formula-decl nil physical_clocks nil)
(P formal-const-decl "posnat" interval_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T const-decl "int" interval_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil)
(nonoverlap_upper-1 nil 3294485393
("" (skosimp*)
(("" (lemma "proper_separation")
((""
(inst - "T(j!1 + 1)" "T1!1" "T2!1" "ic2!1(j!1 + 1)"
"ic1!1(j!1)" "0" "drift * P + pi_0 + alpha_u")
(("" (assert)
(("" (prop)
(("1" (forward-chain "handover_precision_upper")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2 -1)
(("2" (invoke (then (case "%1 <= ADJ") (assert)) (! 1 r))
(("2" (hide 2 -3)
(("2" (expand "ADJ")
(("2" (rewrite "floor_monotone")
(("2" (hide 2)
(("2" (expand "id")
(("2" (isolate 1 l 1)
(("2" (assert)
(("2"
(factor 1 r)
(("2"
(div-by 1 "rate")
(("2"
(invoke (case "%1 <= 0") (! 1 l 1))
(("1"
(mult-by -1 "drift")
(("1" (assert) nil nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "max_le")
(("2"
(rewrite "max_le")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((floor_monotone formula-decl nil floor_ceiling_ineq nil)
(max_le formula-decl nil minmax_ineq nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(rate const-decl "posreal" physical_clocks nil))
nil))
(nonoverlap_round 0
(nonoverlap_round-3 "" 3400004207
("" (skosimp*)
(("" (use "handover_precision_lower")
(("" (assert)
(("" (use "nonoverlap_basis")
(("" (rewrite "T_def") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((handover_precision_lower formula-decl nil interval_clocks nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nonoverlap_basis formula-decl nil physical_clocks nil)
(T const-decl "int" interval_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(P formal-const-decl "posnat" interval_clocks nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(T_def formula-decl nil interval_clocks nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil)
(nonoverlap_round-2 "" 3400004192
("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak)
(nonoverlap_round-1 nil 3294485429
("" (skosimp*)
(("" (rewrite "T_def")
(("" (use "nonoverlap_lower")
(("" (rewrite "T_def") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((rate const-decl "posreal" physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil))
nil))
(lower_interval_accuracy 0
(lower_interval_accuracy-2 nil 3399233072
("" (induct "j")
(("1" (assert)
(("1" (skosimp*)
(("1" (expand "lower_accuracy_bound?")
(("1" (skosimp*)
(("1" (inst -2 0) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "lower_accuracy_bound?" -2)
(("2" (skosimp*)
(("2" (inst - "alpha!1" "ic1!1" "p!1" 0)
(("2" (prop)
(("1" (replace -5 :dir rl)
(("1" (expand "adjustment_lower_bound?")
(("1" (inst - "j!1")
(("1" (inst - "1 + j!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "lower_accuracy_bound?")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((adjustment_lower_bound? const-decl "bool" interval_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(t const-decl "real" interval_clocks nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(P formal-const-decl "posnat" interval_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(lower_accuracy_bound? const-decl "bool" interval_clocks nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(nnreal type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil)
(lower_interval_accuracy-1 nil 3399232999
("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak))
(upper_interval_accuracy 0
(upper_interval_accuracy-2 nil 3399237520
("" (induct "j")
(("1" (assert)
(("1" (expand "upper_accuracy_bound?")
(("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "upper_accuracy_bound?" -2)
(("2" (skosimp*)
(("2" (inst - "alpha!1" "ic1!1" "p!1" 0)
(("2" (prop)
(("1" (replace -5 :dir rl)
(("1" (expand "adjustment_upper_bound?")
(("1" (inst - "j!1")
(("1" (inst - "1 + j!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "upper_accuracy_bound?")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((adjustment_upper_bound? const-decl "bool" interval_clocks nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(t const-decl "real" interval_clocks nil)
(P formal-const-decl "posnat" interval_clocks nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(upper_accuracy_bound? const-decl "bool" interval_clocks nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(interval_clock type-eq-decl nil interval_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nnreal" interval_clocks nil)
(nnreal type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil)
(upper_interval_accuracy-1 nil 3399233266
("" (expand "upper_accuracy_bound?")
(("" (skosimp*)
(("" (lemma "upper_adjustment")
(("" (inst - "ic1!1" "j!1" "p!1")
(("" (assert)
(("" (expand "t")
(("" (inst - "T(j!1)" "j!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rate const-decl "posreal" physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil))
nil)))
[ Original von:0.21Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen.
Man kann per Verzeichnistruktur darin navigieren.
Der Code wird farblich markiert angezeigt.
Datei übertragen
]
|
