products/Sources/formale Sprachen/PVS/measure_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: HeartController.vdmpp   Sprache: Lisp

Original 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.36 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




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