Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/sources/formale Sprachen/PVS/fault_tolerance/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 36 kB image not shown  

Quelle  timing_imprecision.prf   Sprache: Lisp

 
(timing_imprecision
 (mid_latency_ge_one_half 0
  (mid_latency_ge_one_half-1 nil 3393765710
   ("" (expand "mid_latency")
    (("" (expand "epsilon") (("" (assert) nil nil)) nil)) nil)
   ((posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (epsilon const-decl "posreal" timing_imprecision 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)
    (mid_latency const-decl "posreal" timing_imprecision nil))
   nil))
 (W_TCC1 0
  (W_TCC1-1 nil 3393765366 ("" (subtype-tcc) nil nil)
   ((epsilon const-decl "posreal" timing_imprecision nil)
    (mid_latency const-decl "posreal" timing_imprecision nil)
    (fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (W_TCC2 0
  (W_TCC2-1 nil 3393765366 ("" (subtype-tcc) nil nil)
   ((nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (epsilon const-decl "posreal" timing_imprecision nil)
    (mid_latency const-decl "posreal" timing_imprecision nil)
    (fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (drift_relation_alt 0
  (drift_relation_alt-1 nil 3393765728
   ("" (skosimp*)
    (("" (splash 1)
      (("1" (cross-mult) nil nil)
       ("2" (cross-mult)
        (("2" (expand "rate") (("2" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (bool nonempty-type-eq-decl nil 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)
    (>= 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)
    (rho formal-const-decl "nonneg_real" timing_imprecision nil)
    (rate const-decl "posreal" physical_clocks nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil))
 (W_bound 0
  (W_bound-1 nil 3393765744
   ("" (auto-rewrite-defs)
    (("" (assert)
      (("" (expand "W")
        (("" (lift-if)
          (("" (assert)
            (("" (prop)
              (("1" (use "ceiling_def") (("1" (assert) nil nil)) nil)
               ("2"
                (invoke (then (case "%1 >= %2") (assert)) (! 1 l)
                 (! 1 r))
                nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (epsilon const-decl "posreal" timing_imprecision nil)
    (mid_latency const-decl "posreal" timing_imprecision nil)
    (fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
    (max_latency const-decl "posreal" timing_imprecision nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (even_minus_odd_is_odd application-judgement "odd_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)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (rho formal-const-decl "nonneg_real" timing_imprecision nil)
    (var_latency formal-const-decl "nonneg_real" timing_imprecision
     nil)
    (min_latency formal-const-decl "nonneg_real" timing_imprecision
     nil)
    (ceiling_def formula-decl nil floor_ceil nil)
    (ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (integer nonempty-type-from-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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (W const-decl "posint" timing_imprecision nil))
   nil))
 (W_bound_alt 0
  (W_bound_alt-1 nil 3393765758
   ("" (use "W_bound")
    (("" (use "drift_relation_alt")
      (("" (flatten) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((drift_relation_alt formula-decl nil timing_imprecision nil)
    (W const-decl "posint" timing_imprecision nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (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)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     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)
    (W_bound formula-decl nil timing_imprecision nil))
   nil))
 (epsilon_l_TCC1 0
  (epsilon_l_TCC1-2 nil 3393765840
   ("" (use "W_bound_alt") (("" (flatten) (("" (assert) nil nil)) nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (W_bound_alt formula-decl nil timing_imprecision nil))
   nil)
  (epsilon_l_TCC1-1 nil 3393765366 ("" (subtype-tcc) nil nil) nil nil))
 (epsilon_u_TCC1 0
  (epsilon_u_TCC1-2 nil 3393765860
   ("" (use "W_bound_alt") (("" (flatten) (("" (assert) nil nil)) nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (W_bound_alt formula-decl nil timing_imprecision nil))
   nil)
  (epsilon_u_TCC1-1 nil 3393765366 ("" (subtype-tcc) nil nil) nil nil))
 (max_error_TCC1 0
  (max_error_TCC1-1 nil 3393765366 ("" (subtype-tcc) nil nil)
   ((epsilon const-decl "posreal" timing_imprecision nil)
    (mid_latency const-decl "posreal" timing_imprecision nil)
    (fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
    (rho formal-const-decl "nonneg_real" timing_imprecision 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)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (rate const-decl "posreal" physical_clocks nil)
    (epsilon_l const-decl "posreal" timing_imprecision nil)
    (max_latency const-decl "posreal" timing_imprecision nil)
    (epsilon_u const-decl "nnreal" timing_imprecision nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_real_max application-judgement
     "{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil))
 (epsilon_relation 0
  (epsilon_relation-1 nil 3393765810
   ("" (expand "epsilon_l")
    (("" (expand "epsilon_u")
      (("" (expand "max_latency")
        (("" (expand "drift") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (epsilon_u const-decl "nnreal" timing_imprecision nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (drift const-decl "nonneg_real" physical_clocks nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (max_latency const-decl "posreal" timing_imprecision nil)
    (epsilon_l const-decl "posreal" timing_imprecision nil))
   nil))
 (event_observation_error 0
  (event_observation_error-1 nil 3393765420
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "Timestamp")
        (("1" (use "Clock_upper") (("1" (assert) nil nil)) nil)) nil)
       ("2" (expand "Timestamp")
        (("2" (use "Clock_lower")
          (("2" (lemma "drift_right")
            (("2" (invoke (inst - "%1" "%2" _) (! -2 l 1) (! 1 l 1))
              (("2" (inst?)
                (("2" (expand "rate") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Clock_upper formula-decl nil inverse_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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (rho formal-const-decl "nonneg_real" timing_imprecision 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)
    (/ 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)
    (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)
    (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)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Timestamp const-decl "integer" timing_imprecision nil)
    (Clock_lower formula-decl nil inverse_clocks nil)
    (C const-decl "int" inverse_clocks 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_plus_real_is_real application-judgement "real" reals nil)
    (drift_right formula-decl nil physical_clocks nil))
   nil))
 (link_lower_range 0
  (link_lower_range-1 nil 3393765446
   ("" (skosimp*)
    (("" (expand* "good_range" "Timestamp")
      (("" (use "Clock_upper")
        (("" (flatten)
          ((""
            (invoke (then (case "%1 <= %2") (assert)) (! 1 l) (! -2 l))
            (("" (hide-all-but 1)
              (("" (isolate 1 l 1)
                (("" (move-terms 1 r 1)
                  (("" (expand "epsilon_l")
                    (("" (lemma "drift_right")
                      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Timestamp const-decl "integer" timing_imprecision nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (good_range const-decl "set[real]" timing_imprecision nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (drift_right formula-decl nil physical_clocks nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (IFF const-decl "[bool, bool -> bool]" booleans 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)
    (integer nonempty-type-from-decl nil integers nil)
    (epsilon_l const-decl "posreal" timing_imprecision nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (W const-decl "posint" timing_imprecision nil)
    (min_latency formal-const-decl "nonneg_real" timing_imprecision
     nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (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)
    (> 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)
    (rho formal-const-decl "nonneg_real" timing_imprecision 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)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (Clock_upper formula-decl nil inverse_clocks nil))
   nil))
 (link_upper_range 0
  (link_upper_range-1 nil 3393765471
   ("" (skosimp*)
    (("" (expand* "good_range" "Timestamp")
      (("" (use "Clock_lower")
        (("" (flatten)
          (("" (lemma "drift_right")
            (("" (invoke (inst - "%1" "%2" _) (! -2 l 1) (! 1 l 1))
              (("" (inst?)
                (("" (assert)
                  ((""
                    (invoke (then (case "%1 + %2 <= %3") (assert))
                     (! -4 r) (! -1 r) (! 1 r))
                    (("" (hide-all-but 1)
                      (("" (isolate 1 r 1)
                        (("" (move-terms 1 l 1)
                          ((""
                            (expand* "epsilon_u" "max_latency"
                             "epsilon" "rate")
                            (("" (lemma "drift_left")
                              ((""
                                (inst?)
                                ((""
                                  (expand*
                                   "epsilon_u"
                                   "max_latency"
                                   "epsilon"
                                   "rate")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Timestamp const-decl "integer" timing_imprecision nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (good_range const-decl "set[real]" timing_imprecision nil)
    (C const-decl "int" inverse_clocks nil)
    (int_plus_int_is_int application-judgement "int" integers 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)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (drift_left formula-decl nil physical_clocks nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (epsilon const-decl "posreal" timing_imprecision nil)
    (max_latency const-decl "posreal" timing_imprecision nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (integer nonempty-type-from-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (W const-decl "posint" timing_imprecision nil)
    (min_latency formal-const-decl "nonneg_real" timing_imprecision
     nil)
    (var_latency formal-const-decl "nonneg_real" timing_imprecision
     nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (epsilon_u const-decl "nnreal" timing_imprecision nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (drift_right formula-decl nil physical_clocks 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)
    (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)
    (> 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)
    (rho formal-const-decl "nonneg_real" timing_imprecision 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)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (Clock_lower formula-decl nil inverse_clocks nil))
   nil))
 (link_abs_bound 0
  (link_abs_bound-1 nil 3495923645
   ("" (skosimp*)
    (("" (use "link_lower_range")
      (("" (use "link_upper_range")
        (("" (expand "max_error")
          (("" (expand "abs")
            (("" (lift-if) (("" (ground) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((link_lower_range formula-decl nil timing_imprecision 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 "nonneg_real" timing_imprecision 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 nonempty-type-from-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)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (max_error const-decl "posreal" timing_imprecision nil)
    (nonneg_real_max application-judgement
     "{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (link_upper_range formula-decl nil timing_imprecision nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (link_relative_range 0
  (link_relative_range-1 nil 3393765492
   ("" (skosimp*)
    (("" (lemma "event_observation_error")
      (("" (inst-cp - "c2!1" "ev2r!1")
        (("" (inst - "c1!1" "ev1r!1")
          (("" (expand "good_range")
            (("" (flatten)
              (("" (rewrite "abs_max")
                (("" (rewrite "max_le")
                  (("" (expand "epsilon") (("" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((event_observation_error formula-decl nil timing_imprecision nil)
    (epsilon const-decl "posreal" timing_imprecision nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (max_le formula-decl nil minmax_ineq 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)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (abs_max formula-decl nil abs_props nil)
    (integer nonempty-type-from-decl nil integers nil)
    (Timestamp const-decl "integer" timing_imprecision nil)
    (good_range const-decl "set[real]" timing_imprecision 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 "nonneg_real" timing_imprecision 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (link_relative_symmetry 0
  (link_relative_symmetry-1 nil 3393765545
   ("" (skosimp*)
    (("" (use "link_relative_range") (("" (assert) nil nil)) nil)) nil)
   ((link_relative_range formula-decl nil timing_imprecision 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 "nonneg_real" timing_imprecision 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)
    (real_plus_real_is_real application-judgement "real" reals 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))
   nil))
 (good_range_bounded 0
  (good_range_bounded-1 nil 3393765575
   ("" (skosimp*)
    (("" (expand "good_range")
      (("" (flatten)
        (("" (rewrite "abs_max")
          (("" (rewrite "max_le") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (good_range const-decl "set[real]" timing_imprecision nil)
    (abs_max formula-decl nil abs_props 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (var_latency formal-const-decl "nonneg_real" timing_imprecision
     nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (max_le formula-decl nil minmax_ineq nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (link_symmetry 0
  (link_symmetry-1 nil 3393765592
   ("" (skosimp*)
    (("" (rewrite "abs_max")
      (("" (rewrite "max_le")
        (("" (rewrite "abs_max")
          (("" (rewrite "max_le")
            (("" (lemma "event_observation_error")
              (("" (inst-cp - "c1!1" "ev1!1")
                (("" (inst - "c2!1" "ev2!1")
                  (("" (expand "epsilon")
                    (("" (flatten) (("" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((abs_max formula-decl nil abs_props 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" 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)
    (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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (rho formal-const-decl "nonneg_real" timing_imprecision 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)
    (integer nonempty-type-from-decl nil integers nil)
    (Timestamp const-decl "integer" timing_imprecision nil)
    (event_observation_error formula-decl nil timing_imprecision nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (epsilon const-decl "posreal" timing_imprecision nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (var_latency formal-const-decl "nonneg_real" timing_imprecision
     nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (max_le formula-decl nil minmax_ineq nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)))

100%


¤ Dauer der Verarbeitung: 0.5 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.





                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge