|
(physical_clocks
(drift_TCC1 0
(drift_TCC1-1 nil 3315953243
("" (isolate 1 l 1)
(("" (assert)
(("" (cross-mult)
(("" (expand "rate") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
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)
(div_mult_pos_ge2 formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(rate const-decl "posreal" physical_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, 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)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(drift_def 0
(drift_def-1 nil 3260711120
("" (expand "drift")
(("" (isolate 1 l 1) (("" (cross-mult 1) nil nil)) nil)) nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" 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)
(>= 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)
(rate const-decl "posreal" physical_clocks nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil))
(drift_bound 0
(drift_bound-2 "" 3495547725
("" (expand "drift")
(("" (expand "rate") (("" (field) nil nil)) nil)) nil)
((posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(rate const-decl "posreal" physical_clocks nil)
(rho formal-const-decl "nonneg_real" physical_clocks 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_times_pos_le1 formula-decl nil real_props 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)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types 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_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
shostak)
(drift_bound-1 nil 3260711120
("" (expand "drift")
(("" (expand "rate") (("" (field) nil nil)) nil)) nil)
nil nil))
(good_clock_TCC1 0
(good_clock_TCC1-1 nil 3260711120
("" (expand "rate")
(("" (skosimp*)
(("" (assert)
(("" (assert) (("" (cross-mult) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rho formal-const-decl "nonneg_real" physical_clocks nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(div_mult_pos_le1 formula-decl nil real_props 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)
(rate const-decl "posreal" physical_clocks nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil))
nil))
(drift_left_nat 0
(drift_left_nat-1 nil 3399245613
("" (induct-and-simplify "X")
(("" (typepred "c!1")
(("" (inst - "T!1") (("" (assert) nil nil)) nil)) nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_plus_int_is_int application-judgement "int" integers 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)
(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)
(pred type-eq-decl nil defined_types 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)
(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)
(nat_induction formula-decl nil naturalnumbers nil))
shostak))
(drift_right_nat 0
(drift_right_nat-1 nil 3399245696
("" (induct-and-simplify "X")
(("" (typepred "c!1")
(("" (inst - "T!1") (("" (assert) nil nil)) nil)) nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_plus_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)
(pred type-eq-decl nil defined_types 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)
(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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nat_induction formula-decl nil naturalnumbers nil))
shostak))
(drift_left 0
(drift_left-1 nil 3260711120
("" (skosimp*)
(("" (name "n" "T2!1 - T1!1")
(("" (isolate -1 l 1)
(("" (replace*)
(("" (assert)
(("" (hide -1 -2)
(("" (generalize "n" "n" "nat")
(("" (induct "n")
(("1" (assert) nil nil)
("2" (skosimp*)
(("2" (typepred "c!1")
(("2" (inst - "T1!1 + j!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(rate const-decl "posreal" physical_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)
(<= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil))
(drift_right 0
(drift_right-2 nil 3367681272
("" (skosimp*)
(("" (name "n" "T2!1 - T1!1")
(("" (isolate -1 l 1)
(("" (replace*)
(("" (assert)
(("" (hide -1 -2)
(("" (generalize "n" "n" "nat")
(("" (induct "n")
(("1" (assert) nil nil)
("2" (skosimp*)
(("2" (typepred "c!1")
(("2" (inst - "T1!1 + j!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(rate const-decl "posreal" physical_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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil)
(drift_right-1 nil 3260711120
("" (skosimp*)
(("" (typepred "c!1")
(("" (inst - "T1!1" "T2!1") (("" (assert) nil nil)) nil)) nil))
nil)
nil nil))
(abs_drift_lb 0
(abs_drift_lb-1 nil 3495923150
("" (skosimp*)
(("" (lemma "drift_left")
(("" (case "T1!1 <= T2!1")
(("1" (inst - "T1!1" "T2!1" "c!1")
(("1" (assert)
(("1" (expand "abs")
(("1" (lift-if)
(("1" (assert)
(("1" (lift-if) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (inst?)
(("2" (assert)
(("2" (expand "abs")
(("2" (assert)
(("2" (lift-if) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((drift_left formula-decl nil physical_clocks nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs 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)
(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)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(clock_nondecreasing 0
(clock_nondecreasing-1 nil 3260711120
("" (skosimp*)
(("" (lemma "drift_left")
(("" (inst - "T1!1" "T2!1" "c!1")
(("" (assert)
(("" (invoke (then (case "0 <= %1") (assert)) (! -1 l))
(("" (cross-mult 1) nil nil)) nil))
nil))
nil))
nil))
nil)
((drift_left formula-decl nil physical_clocks nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals 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)
(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))
nil))
(clock_increasing 0
(clock_increasing-1 nil 3260711120
("" (skosimp*)
(("" (lemma "drift_left")
(("" (inst - "T1!1" "T2!1" "c!1")
(("" (assert)
(("" (invoke (then (case "0 < %1") (assert)) (! -1 l))
(("" (cross-mult 1) nil nil)) nil))
nil))
nil))
nil))
nil)
((drift_left formula-decl nil physical_clocks nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(< const-decl "bool" reals 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)
(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))
nil))
(clock_nondecreasing_alt 0
(clock_nondecreasing_alt-1 nil 3271175309
("" (skosimp*)
(("" (lemma "clock_increasing")
(("" (inst - "T2!1" "T1!1" "c!1") (("" (assert) nil nil)) nil))
nil))
nil)
((clock_increasing formula-decl nil physical_clocks 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)
(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)
(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))
shostak))
(clock_eq_arg 0
(clock_eq_arg-1 nil 3356444490
("" (skosimp*)
(("" (lemma "clock_nondecreasing_alt")
(("" (inst-cp - "T1!1" "T2!1" "c!1")
(("" (inst - "T2!1" "T1!1" "c!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((clock_nondecreasing_alt formula-decl nil physical_clocks nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(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))
shostak))
(relative_drift 0
(relative_drift-1 nil 3281817151
("" (skosimp*)
(("" (lemma "drift_left_nat")
(("" (inst - "T2!1" "X!1" "c2!1")
(("" (lemma "drift_right_nat")
(("" (inst - "T1!1" "X!1" "c1!1")
(("" (expand "drift") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((drift_left_nat formula-decl nil physical_clocks nil)
(drift_right_nat formula-decl nil physical_clocks nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(drift const-decl "nonneg_real" physical_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_plus_int_is_int application-judgement "int" integers nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(nonoverlap_basis 0
(nonoverlap_basis-1 nil 3399589965
("" (skosimp*)
(("" (lemma "drift_left")
(("" (inst-cp - "T1!1" "T!1" "c1!1")
(("" (inst - "T!1" "T2!1" "c2!1")
(("" (prop)
(("" (div-by (-4 -5 -6) "rate") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((drift_left formula-decl nil physical_clocks nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(both_sides_div_pos_gt1 formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(times_div_cancel1 formula-decl nil extra_real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_div_pos_le1 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(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)
(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))
shostak))
(skew_basis_0 0
(skew_basis_0-1 nil 3399621083
("" (skosimp*)
(("" (lemma "drift_left")
(("" (inst-cp - "T1!1" "T!1" "c1!1")
(("" (inst - "T!1" "T2!1" "c2!1")
(("" (prop)
(("" (div-by (1 -5 -6) "rate") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((drift_left formula-decl nil physical_clocks nil)
(both_sides_div_pos_le1 formula-decl nil real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(both_sides_div_pos_lt1 formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(times_div_cancel1 formula-decl nil extra_real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(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))
nil))
(skew_bound_1 0
(skew_bound_1-1 nil 3399621221
("" (skosimp*)
(("" (lemma "nonoverlap_basis")
((""
(inst - _ "T1!1" "T2!1" "skew!1 + drift * X!1" "c1!1" "c2!1")
(("" (assert)
(("" (lemma "relative_drift")
(("" (inst - "T!1" "T!1" "T1!1 - T!1" "c1!1" "c2!1")
(("1" (inst - "T1!1")
(("1" (mult-by -4 "drift") (("1" (assert) nil nil))
nil))
nil)
("2" (lemma "relative_drift")
(("2" (inst - "T2!1" "T2!1" "T!1 - T2!1" "c2!1" "c1!1")
(("1" (inst - "T2!1")
(("1" (mult-by -5 "drift") (("1" (assert) nil nil))
nil))
nil)
("2" (inst - "T!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonoverlap_basis formula-decl nil physical_clocks nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T1!1 skolem-const-decl "int" physical_clocks nil)
(T!1 skolem-const-decl "int" physical_clocks nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(T2!1 skolem-const-decl "int" physical_clocks nil)
(relative_drift formula-decl nil physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(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)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal 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)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil))
(skew_bound_2 0
(skew_bound_2-1 nil 3399621476
("" (skosimp*)
(("" (lemma "skew_basis_0")
((""
(inst - _ "T1!1" "T2!1" "skew!1 + drift * X!1" "c1!1" "c2!1")
(("" (assert)
(("" (lemma "relative_drift")
(("" (inst - "T!1" "T!1" "T1!1 - T!1" "c1!1" "c2!1")
(("1" (inst - "T1!1")
(("1" (mult-by -4 "drift") (("1" (assert) nil nil))
nil))
nil)
("2" (lemma "relative_drift")
(("2" (inst - "T2!1" "T2!1" "T!1 - T2!1" "c2!1" "c1!1")
(("1" (inst - "T2!1")
(("1" (mult-by -5 "drift") (("1" (assert) nil nil))
nil))
nil)
("2" (inst - "T!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((skew_basis_0 formula-decl nil physical_clocks nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T1!1 skolem-const-decl "int" physical_clocks nil)
(T!1 skolem-const-decl "int" physical_clocks nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(T2!1 skolem-const-decl "int" physical_clocks nil)
(relative_drift formula-decl nil physical_clocks nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rate const-decl "posreal" physical_clocks nil)
(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)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(drift const-decl "nonneg_real" physical_clocks nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal 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)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil))
(skew_bound 0
(skew_bound-6 "" 3399573371
("" (skosimp*)
(("" (rewrite "le_ceiling")
(("" (isolate 1 l 1)
(("" (expand "abs" 1)
(("" (lift-if)
(("" (prop)
(("1" (lemma "skew_bound_2")
(("1"
(inst - "T!1" "T1!1 + 1" "T2!1" "X!1" "c1!1" "c2!1"
"skew!1")
(("1" (assert) nil nil)) nil))
nil)
("2" (lemma "skew_bound_1")
(("2"
(inst - "T!1" "T2!1" "T1!1" "X!1" "c2!1" "c1!1"
"skew!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(int_plus_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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(/= 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(good_clock nonempty-type-eq-decl nil physical_clocks nil)
(nnreal type-eq-decl nil 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)
(minus_int_is_int application-judgement "int" integers nil)
(nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(skew_bound_2 formula-decl nil physical_clocks nil)
(skew_bound_1 formula-decl nil physical_clocks nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak)
(skew_bound-5 "" 3399573363
(";;; Proof skew_bound_alt-1 for formula physical_clocks.skew_bound_alt"
(skosimp*)
((";;; Proof skew_bound_alt-1 for formula physical_clocks.skew_bound_alt"
(rewrite "le_ceiling")
((";;; Proof skew_bound_alt-1 for formula physical_clocks.skew_bound_alt"
(isolate 1 l 1)
((";;; Proof skew_bound_alt-1 for formula physical_clocks.skew_bound_alt"
(expand "abs" 1)
((";;; Proof skew_bound_alt-1 for formula physical_clocks.skew_bound_alt"
(lift-if)
((";;; Proof skew_bound_alt-1 for formula physical_clocks.skew_bound_alt"
(prop)
(("1" (lemma "separation_basis")
(("1"
(inst - "T!1" "T1!1 + 1" "T2!1" "X!1" "c1!1" "c2!1"
"skew!1")
(("1" (assert) nil)))))
("2" (lemma "proper_separation_basis")
(("2"
(inst - "T!1" "T2!1" "T1!1" "X!1" "c2!1" "c1!1"
"skew!1")
(("2" (assert) nil))))))))))))))))
";;; developed with shostak decision procedures")
nil nil)
(skew_bound-4 "" 3399165625
("" (skosimp*)
(("" (expand "abs" 1 1)
(("" (lift-if +)
(("" (prop)
(("1" (lemma "separation")
(("1"
(inst - "T!1" "T1!1 + 1" "T2!1" "c1!1" "c2!1" "0"
"skew!1")
(("1" (assert)
(("1"
(invoke (then (case "%1 <= %2") (assert)) (! 1 r)
(! 2 r))
(("1" (hide-all-but (1 -1 -3))
(("1" (rewrite "ceiling_monotone")
(("1" (hide 2)
(("1" (cancel)
(("1" (cancel)
(("1" (cancel)
(("1"
(rewrite "max_le")
(("1" (rewrite "max_le") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "proper_separation")
(("2"
(inst - "T!1" "T2!1" "T1!1" "c2!1" "c1!1" "0" "skew!1")
(("2" (rewrite "abs_diff_commutes" -)
(("2" (assert)
(("2" (use "gt_floor_r")
(("2" (replace 1 :hide? t)
(("2" (prop)
(("2" (use "le_ceiling_r")
(("2" (prop)
(("2"
(invoke (then (case "%1 <= %2") (assert))
(! 3 r) (! 1 r))
(("2"
(hide-all-but (1 5 -2))
(("2"
(cancel)
(("2"
(cancel)
(("2"
(cancel)
(("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)
((ceiling_monotone formula-decl nil floor_ceiling_ineq nil)
(max_le formula-decl nil minmax_ineq nil)
(le_ceiling_r formula-decl nil floor_ceiling_ineq nil)
(gt_floor_r formula-decl nil floor_ceiling_ineq nil)
(abs_diff_commutes formula-decl nil abs_props nil))
nil)
(skew_bound-3 "" 3282503705
("" (skosimp*)
(("" (expand "abs" 1 1)
(("" (lift-if +)
(("" (prop)
(("1" (lemma "separation")
(("1"
(inst - "T!1" "T1!1 + 1" "T2!1" "c1!1" "c2!1" "0"
"skew!1")
(("1" (assert)
(("1"
(invoke (then (case "%1 <= %2") (assert)) (! 1 r)
(! 2 r))
(("1" (hide-all-but (1 -1))
(("1" (rewrite "ceiling_monotone")
(("1" (hide 2)
(("1" (cancel)
(("1" (cancel)
(("1" (cancel)
(("1"
(rewrite "max_le")
(("1"
(rewrite "max_le")
(("1"
(assert)
(("1"
(expand "abs")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "proper_separation")
(("2"
(inst - "T!1" "T2!1" "T1!1" "c2!1" "c1!1" "0" "skew!1")
(("2" (rewrite "abs_diff_commutes" -)
(("2" (assert)
(("2" (use "gt_floor_r")
(("2" (replace 1 :hide? t)
(("2" (prop)
(("2" (use "le_ceiling_r")
(("2" (prop)
(("2"
(invoke (then (case "%1 <= %2") (assert))
(! 3 r) (! 1 r))
(("2"
(hide-all-but (1 5))
(("2"
(cancel)
(("2"
(cancel)
(("2"
(cancel)
(("2"
(rewrite "max_le")
(("2"
(rewrite "max_le")
(("2"
(assert)
(("2"
(expand "abs")
(("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))
nil)
((ceiling_monotone formula-decl nil floor_ceiling_ineq nil)
(max_le formula-decl nil minmax_ineq nil)
(le_ceiling_r formula-decl nil floor_ceiling_ineq nil)
(gt_floor_r formula-decl nil floor_ceiling_ineq nil)
(abs_diff_commutes formula-decl nil abs_props nil))
shostak)
(skew_bound-2 nil 3282503659
("" (skosimp*)
(("" (expand "abs" 1 1)
(("" (lift-if +)
(("" (prop)
(("1" (lemma "separation")
(("1"
(inst - "T!1" "T1!1 + 1" "T2!1" "c1!1" "c2!1" "0"
"skew!1")
(("1" (assert)
(("1"
(invoke (then (case "%1 <= %2") (assert)) (! 1 r)
(! 2 r))
(("1" (hide-all-but (1 -1))
(("1" (rewrite "ceiling_monotone")
(("1" (hide 2)
(("1" (div-by 1 "id(1 + rho)")
(("1" (expand "id")
(("1" (move-terms 1 l 2)
(("1"
(assert)
(("1"
(div-by 1 "drift")
(("1"
(rewrite "max_le")
(("1"
(rewrite "max_le")
(("1"
(assert)
(("1"
(expand "abs")
(("1"
(assert)
nil)))))))))))))))))))))))))))))))))
("2" (lemma "proper_separation")
(("2"
(inst - "T!1" "T2!1" "T1!1" "c2!1" "c1!1" "0" "skew!1")
(("2" (rewrite "abs_diff_commutes" -)
(("2" (assert)
(("2"
(invoke (then (case "%1 <= %2") (assert)) (! 1 r)
(! 3 r))
(("2" (hide-all-but (3 1))
(("2" (rewrite "ceiling_monotone")
(("2" (hide 2)
(("2" (div-by 1 "id(1 + rho)")
(("2" (expand "id")
(("2"
(move-terms 1 l 2)
(("2"
(assert)
(("2"
(div-by 1 "drift")
(("2"
(rewrite "max_le")
(("2"
(rewrite "max_le")
(("2"
(assert)
(("2"
(expand "abs")
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))
nil)
((abs_diff_commutes formula-decl nil abs_props nil)
(ceiling_monotone formula-decl nil floor_ceiling_ineq nil))
nil)
(skew_bound-1 nil 3282477056
("" (skosimp*)
(("" (expand "abs" 1 1)
(("" (lift-if +)
(("" (prop)
(("1" (lemma "separation")
(("1"
(inst - "T!1" "T1!1 + 1" "T2!1" "c1!1" "c2!1" "0"
"skew!1")
(("1" (assert)
(("1"
(invoke (then (case "%1 <= %2") (assert)) (! 1 r)
(! 2 r))
(("1" (hide-all-but (1 -1))
(("1" (rewrite "ceiling_monotone")
(("1" (hide 2)
(("1" (div-by 1 "id(1 + rho)")
(("1" (expand "id")
(("1" (move-terms 1 l 2)
(("1"
(assert)
(("1"
(div-by 1 "drift")
(("1"
(rewrite "max_le")
(("1"
(rewrite "max_le")
(("1"
(rewrite "le_max")
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand "abs")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "proper_separation")
(("2"
(inst - "T!1" "T2!1" "T1!1" "c2!1" "c1!1" "0" "skew!1")
(("2" (rewrite "abs_diff_commutes" -)
(("2" (assert)
(("2"
(invoke (then (case "%1 <= %2") (assert)) (! 1 r)
(! 3 r))
(("2" (hide-all-but (3 1))
(("2" (rewrite "ceiling_monotone")
(("2" (hide 2)
(("2" (div-by 1 "id(1 + rho)")
(("2" (expand "id")
(("2"
(move-terms 1 l 2)
(("2"
(assert)
(("2"
(div-by 1 "drift")
(("2"
(rewrite "max_le")
(("2"
(rewrite "max_le")
(("2"
(rewrite "le_max")
(("2"
(flatten)
(("2"
(assert)
(("2"
(expand "abs")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.80 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
