| products/Sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: physical_clocks.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.34 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
