| products/Sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: synch_protocol_invariants.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(synch_protocol_invariants
(all_periodic_precision_iff_peer_precision 0 (all_periodic_precision_iff_peer_precision-1 nil 3399068668 ("" (expand* "peer_precision?" "all_periodic_precision?" "periodic_precision?") nil nil) ((periodic_precision? const-decl "bool" synch_protocol_invariants nil) (all_periodic_precision? const-decl "bool" synch_protocol_invariants nil) (peer_precision? const-decl "bool" interval_clocks nil)) nil)) (all_periodic_precision 0 (all_periodic_precision-1 nil 3399068683 ("" (expand "all_periodic_precision?") (("" (skosimp*) (("" (generalize-skolem-constants) (("" (induct "j_1") (("1" (skosimp*) (("1" (expand "initial_precision?") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (expand "periodic_precision_enhancement?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (rho formal-const-decl "nnreal" synch_protocol_invariants 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) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (initial_precision? const-decl "bool" synch_protocol_invariants nil) (periodic_precision_enhancement? const-decl "bool" synch_protocol_invariants nil) (periodic_precision? const-decl "bool" synch_protocol_invariants nil) (all_periodic_precision? const-decl "bool" synch_protocol_invariants nil)) nil)) (minmax_adjustment_lower_bound 0 (minmax_adjustment_lower_bound-1 nil 3399068699 ("" (expand "adjustment_lower_bound?") (("" (skosimp*) (("" (expand* "all_periodic_precision?" "periodic_precision?") (("" (inst?) (("" (expand* "lower_accuracy_preservation?" "adjustment_lower_bound?") (("" (inst?) (("" (assert) nil 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (lower_accuracy_preservation? const-decl "bool" synch_protocol_invariants nil) (all_periodic_precision? const-decl "bool" synch_protocol_invariants nil) (periodic_precision? const-decl "bool" synch_protocol_invariants nil) (adjustment_lower_bound? const-decl "bool" interval_clocks nil)) nil)) (minmax_adjustment_upper_bound 0 (minmax_adjustment_upper_bound-1 nil 3399068717 ("" (expand "adjustment_upper_bound?") (("" (skosimp*) (("" (expand* "upper_accuracy_preservation?" "adjustment_upper_bound?") (("" (inst?) (("" (expand* "all_periodic_precision?" "periodic_precision?") (("" (inst - "j!1") (("" (assert) nil 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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (all_periodic_precision? const-decl "bool" synch_protocol_invariants nil) (periodic_precision? const-decl "bool" synch_protocol_invariants nil) (upper_accuracy_preservation? const-decl "bool" synch_protocol_invariants nil) (adjustment_upper_bound? const-decl "bool" interval_clocks nil)) nil)) (min_le_trace 0 (min_le_trace-1 nil 3399068739 ("" (skosimp*) (("" (expand* "t" "ic_min" "trace?") (("" (inst?) (("" (rewrite "clock_min_is_min") nil nil)) nil)) nil)) nil) ((ic_min const-decl "good_clock" clock_minmax nil) (trace? const-decl "bool" synch_protocol_invariants nil) (t const-decl "real" interval_clocks nil) (clock_min_is_min formula-decl nil clock_minmax nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (T const-decl "int" interval_clocks 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) (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) (interval_clock type-eq-decl nil interval_clocks nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (nnreal type-eq-decl nil real_types nil) (rho formal-const-decl "nnreal" synch_protocol_invariants 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)) nil)) (trace_le_max 0 (trace_le_max-1 nil 3399068754 ("" (skosimp*) (("" (expand* "t" "ic_max" "trace?") (("" (inst?) (("" (rewrite "clock_max_is_max") nil nil)) nil)) nil)) nil) ((ic_max const-decl "good_clock" clock_minmax nil) (trace? const-decl "bool" synch_protocol_invariants nil) (t const-decl "real" interval_clocks nil) (clock_max_is_max formula-decl nil clock_minmax nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (T const-decl "int" interval_clocks 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) (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) (interval_clock type-eq-decl nil interval_clocks nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (nnreal type-eq-decl nil real_types nil) (rho formal-const-decl "nnreal" synch_protocol_invariants 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)) nil)) (trace_diff 0 (trace_diff-1 nil 3399068776 ("" (skosimp*) (("" (lemma "min_le_trace") (("" (inst - _ "ic2!1" _) (("" (inst?) (("" (lemma "trace_le_max") (("" (inst - _ "ic1!1" _) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((min_le_trace formula-decl nil synch_protocol_invariants nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (trace_le_max formula-decl nil synch_protocol_invariants nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_protocol_invariants nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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)) nil)) (traces_peer_precision 0 (traces_peer_precision-1 nil 3399068794 ("" (skosimp*) (("" (expand "peer_precision?") (("" (skosimp*) (("" (use "trace_diff") (("" (forward-chain "all_periodic_precision") (("" (expand "all_periodic_precision?") (("" (inst - "j!1") (("" (expand "periodic_precision?") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((peer_precision? const-decl "bool" interval_clocks nil) (trace_diff formula-decl nil synch_protocol_invariants nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_protocol_invariants nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (all_periodic_precision? const-decl "bool" synch_protocol_invariants nil) (periodic_precision? const-decl "bool" synch_protocol_invariants nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (all_periodic_precision formula-decl nil synch_protocol_invariants nil)) nil)) (traces_lower 0 (traces_lower-1 nil 3399068823 ("" (skosimp*) (("" (expand "adjustment_lower_bound?") (("" (skosimp*) (("" (lemma "trace_diff") (("" (inst - _ _ "ic1!1" "ic2!1" "j!1" "1 + j!1") (("" (inst?) (("" (inst?) (("" (forward-chain "all_periodic_precision") (("" (forward-chain "minmax_adjustment_lower_bound") (("" (expand "adjustment_lower_bound?") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((adjustment_lower_bound? const-decl "bool" interval_clocks nil) (trace_diff formula-decl nil synch_protocol_invariants nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (all_periodic_precision formula-decl nil synch_protocol_invariants nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minmax_adjustment_lower_bound formula-decl nil synch_protocol_invariants nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_protocol_invariants nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (traces_upper 0 (traces_upper-1 nil 3399068850 ("" (skosimp*) (("" (expand "adjustment_upper_bound?") (("" (skosimp*) (("" (use "trace_diff") (("" (forward-chain "all_periodic_precision") (("" (forward-chain "minmax_adjustment_upper_bound") (("" (expand "adjustment_upper_bound?") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((adjustment_upper_bound? const-decl "bool" interval_clocks nil) (trace_diff formula-decl nil synch_protocol_invariants nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_protocol_invariants nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (minmax_adjustment_upper_bound formula-decl nil synch_protocol_invariants 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_plus_real_is_real application-judgement "real" reals nil) (all_periodic_precision formula-decl nil synch_protocol_invariants nil)) nil)) (traces_compatible 0 (traces_compatible-1 nil 3399068885 ("" (expand "synch_protocol_invariants?") (("" (expand "compatible?") (("" (skosimp*) (("" (prop) (("1" (lemma "traces_peer_precision") (("1" (inst - _ _ _ "pi!1") (("1" (inst?) (("1" (inst - "ic2!1") (("1" (assert) (("1" (expand "peer_precision?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "traces_lower") (("2" (inst - _ _ _ "pi!1" _) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (expand "lower_accuracy_preservation?") (("2" (expand "adjustment_lower_bound?") (("2" (hide 2) (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "traces_upper") (("3" (inst - _ _ _ "pi!1" _) (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (expand "upper_accuracy_preservation?") (("3" (expand "adjustment_upper_bound?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (compatible? const-decl "bool" interval_clocks nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (peer_precision? const-decl "bool" interval_clocks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_protocol_invariants nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (traces_peer_precision formula-decl nil synch_protocol_invariants nil) (lower_accuracy_preservation? const-decl "bool" synch_protocol_invariants nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (adjustment_lower_bound? const-decl "bool" interval_clocks nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (traces_lower formula-decl nil synch_protocol_invariants nil) (upper_accuracy_preservation? const-decl "bool" synch_protocol_invariants nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (adjustment_upper_bound? const-decl "bool" interval_clocks nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (traces_upper formula-decl nil synch_protocol_invariants nil) (synch_protocol_invariants? const-decl "bool" synch_protocol_invariants nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (trace_lower_accuracy 0 (trace_lower_accuracy-1 nil 3399068900 ("" (expand* "synch_protocol_invariants?" "lower_accuracy_preservation?" "lower_accuracy_bound?") (("" (skosimp*) (("" (inst?) (("" (prop) (("1" (skosimp*) (("1" (rewrite "min_le_trace") nil nil)) nil) ("2" (expand* "initial_precision?" "periodic_precision?") (("2" (use "trace_le_max") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((min_le_trace formula-decl nil synch_protocol_invariants nil) (trace_le_max formula-decl nil synch_protocol_invariants nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (initial_precision? const-decl "bool" synch_protocol_invariants nil) (periodic_precision? const-decl "bool" synch_protocol_invariants nil) (ic_min const-decl "good_clock" clock_minmax nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_protocol_invariants nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (synch_protocol_invariants? const-decl "bool" synch_protocol_invariants nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (lower_accuracy_bound? const-decl "bool" interval_clocks nil) (lower_accuracy_preservation? const-decl "bool" synch_protocol_invariants nil)) nil)) (trace_upper_accuracy 0 (trace_upper_accuracy-1 nil 3399068915 ("" (expand* "synch_protocol_invariants?" "upper_accuracy_bound?" "upper_accuracy_preservation?") (("" (skosimp*) (("" (inst?) (("" (prop) (("1" (skosimp*) (("1" (rewrite "trace_le_max") nil nil)) nil) ("2" (expand* "initial_precision?" "periodic_precision?") (("2" (lemma "min_le_trace") (("2" (inst?) (("2" (inst - "ic!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trace_le_max formula-decl nil synch_protocol_invariants nil) (min_le_trace formula-decl nil synch_protocol_invariants nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (initial_precision? const-decl "bool" synch_protocol_invariants nil) (periodic_precision? const-decl "bool" synch_protocol_invariants nil) (ic_max const-decl "good_clock" clock_minmax nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (interval_clock type-eq-decl nil interval_clocks nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nnreal" synch_protocol_invariants nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (synch_protocol_invariants? const-decl "bool" synch_protocol_invariants nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (upper_accuracy_preservation? const-decl "bool" synch_protocol_invariants nil) (upper_accuracy_bound? const-decl "bool" interval_clocks nil)) nil)) (trace_weakly_accurate 0 (trace_weakly_accurate-2 nil 3399278786 ("" (expand "synch_protocol_invariants?") (("" (expand "weakly_accurate?") (("" (skosimp*) (("" (rewrite "p_min_lower") (("" (rewrite "p_max_upper") (("" (use "traces_lower") (("" (prop) (("" (use "traces_upper") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((weakly_accurate? const-decl "bool" interval_clocks nil) (p_min_lower formula-decl nil synch_constant_definitions 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (P formal-const-decl "posnat" synch_protocol_invariants nil) (T0 formal-const-decl "int" synch_protocol_invariants nil) (nnreal type-eq-decl nil real_types nil) (rho formal-const-decl "nnreal" synch_protocol_invariants nil) (alpha_l formal-const-decl "nnreal" synch_protocol_invariants nil) (alpha_u formal-const-decl "nnreal" synch_protocol_invariants nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (P_bound? const-decl "bool" synch_parameter_constraints nil) (pi_0 formal-const-decl "{pi_0: posreal | P_bound?(P, rho, alpha_l, alpha_u, pi_0)}" synch_protocol_invariants nil) (real_minus_real_is_real application-judgement "real" reals nil) (traces_lower formula-decl nil synch_protocol_invariants nil) (p_lower const-decl "posreal" synch_constant_definitions nil) (interval_clock type-eq-decl nil interval_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (/ 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) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (traces_upper formula-decl nil synch_protocol_invariants nil) (p_upper const-decl "posreal" synch_constant_definitions nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (p_max_upper formula-decl nil synch_constant_definitions nil) (synch_protocol_invariants? const-decl "bool" synch_protocol_invariants nil)) nil) (trace_weakly_accurate-1 nil 3399068869 ("" (expand "synch_protocol_invariants?") (("" (expand "weakly_accurate?") (("" (skosimp*) (("" (use "traces_lower") (("" (assert) (("" (lemma "traces_upper") (("" (inst - _ _ _ "pi!1" "pu!1") (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (rate const-decl "posreal" physical_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (interval_clock type-eq-decl nil interval_clocks nil)) nil))) ¤ Dauer der Verarbeitung: 0.25 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 |
