Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: clock_shift.prf Sprache: Lisp

Original von: PVS^©

(clock_shift
(offset_left_edge 0
  (offset_left_edge-1 nil 3403541539
   ("" (skosimp*)
    (("" (expand "offset")
      (("" (expand "clock_edge?")
        (("" (skosimp*)
          (("" (replace -1 :hide? t)
            (("" (rewrite "Clock_rewrite")
              (("" (use "drift_left") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((offset const-decl "real" clock_shift nil)
    (Clock_rewrite formula-decl nil inverse_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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (N formal-const-decl "posnat" clock_shift nil)
    (below type-eq-decl nil naturalnumbers 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" clock_shift nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (drift_left formula-decl nil physical_clocks nil)
    (clock_edge? const-decl "bool" physical_clocks nil))
   nil))
(offset_left 0
  (offset_left-1 nil 3356340049
   ("" (skosimp*)
    (("" (expand "offset")
      (("" (use "Clock_upper")
        (("" (lemma "drift_right_nat")
          (("" (inst?)
            (("" (lemma "drift_left_nat")
              (("" (inst - _ "X!1" "c!1(n!1)")
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((offset const-decl "real" clock_shift nil)
    (drift_right_nat formula-decl nil physical_clocks nil)
    (drift_left_nat formula-decl nil physical_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (C const-decl "int" inverse_clocks nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (int_plus_int_is_int application-judgement "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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (N formal-const-decl "posnat" clock_shift nil)
    (below type-eq-decl nil naturalnumbers nil)
    (rho formal-const-decl "nonneg_real" clock_shift 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))
   shostak))
(offset_right_edge 0
  (offset_right_edge-1 nil 3403542544
   ("" (skosimp*)
    (("" (expand "offset")
      (("" (expand "clock_edge?")
        (("" (skosimp*)
          (("" (replace -1 :hide? t)
            (("" (rewrite "Clock_rewrite")
              (("" (use "drift_right") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((offset const-decl "real" clock_shift nil)
    (Clock_rewrite formula-decl nil inverse_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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (N formal-const-decl "posnat" clock_shift nil)
    (below type-eq-decl nil naturalnumbers 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" clock_shift nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (drift_right formula-decl nil physical_clocks nil)
    (clock_edge? const-decl "bool" physical_clocks nil))
   nil))
(offset_right 0
  (offset_right-2 nil 3356340177
   ("" (skosimp*)
    (("" (expand "offset")
      (("" (use "Clock_lower")
        (("" (lemma "drift_right")
          ((""
            (invoke (inst - "%1" "%2" "c!1(n!1)") (! -2 l 1)
             (! 1 l 1 1))
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((offset const-decl "real" clock_shift nil)
    (drift_right formula-decl nil physical_clocks nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (C const-decl "int" inverse_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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (N formal-const-decl "posnat" clock_shift nil)
    (below type-eq-decl nil naturalnumbers nil)
    (rho formal-const-decl "nonneg_real" clock_shift 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)
  (offset_right-1 nil 3356340147
   ("" (induct "k")
    (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil)))))
     ("2" (skosimp*)
      (("2" (rewrite "sigma_last")
        (("2" (inst?)
          (("2" (inst?)
            (("2" (inst?)
              (("2" (inst?)
                (("2" (prop)
                  (("1" (rewrite "+")
                    (("1" (move-terms 1 l (2 3))
                      (("1"
                        (invoke
                         (then (case "%1 <= %2") (assert) (hide -1 2))
                         (! -1 r) (! 1 r))
                        (("1" (expand* "*" "synch_protocol" "v_min")
                          (("1" (inst?)
                            (("1" (assert)
                              (("1"
                                (replace -1 :hide? t)
                                (("1"
                                  (isolate 1 r 2)
                                  (("1"
                                    (expand*
                                     "clock_relation?"
                                     "nominal"
                                     "epsilon_lower")
                                    (("1"
                                      (inst?)
                                      (("1"
                                        (expand*
                                         "majority_synch?"
                                         "majority?"
                                         "correct_denotation"
                                         "conforms"
                                         "received")
                                        (("1"
                                          (inst?)
                                          (("1"
                                            (assert)
                                            (("1"
                                              (use
                                               "lower_synch_validity[source_error(j!1+j!2), rho, min_latency(j!1 + j!2), var_latency(j!1 + j!2), stage(j!1 + j!2), stage(1 + j!1 + j!2)]")
                                              (("1"
                                                (expand
                                                 "majority_synch?")
                                                (("1"
                                                  (propax)
                                                  nil)))))))))))))))))))))))))))))))
                   ("2" (hide-all-but (-1 1))
                    (("2" (expand "synch_protocol")
                      (("2" (skosimp*)
                        (("2" (inst?) (("2" (assert) nil)))))))))
                   ("3" (hide-all-but (-2 1))
                    (("3" (expand "majority_synch?")
                      (("3" (expand "majority?")
                        (("3" (skosimp*)
                          (("3" (inst?)
                            (("3" (assert)
                              nil))))))))))))))))))))))))))
    nil)
   nil nil))
(offset_zero 0
  (offset_zero-1 nil 3357289330
   ("" (skosimp*)
    (("" (apply-extensionality :hide? t)
      (("" (expand "all_clock_edge?")
        (("" (inst?)
          (("" (expand "clock_edge?")
            (("" (skosimp*)
              (("" (expand "offset")
                (("" (replace -1 :hide? t)
                  (("" (rewrite "Clock_rewrite") nil nil)) 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)
    (< 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)
    (N formal-const-decl "posnat" clock_shift nil)
    (below type-eq-decl nil naturalnumbers nil)
    (offset const-decl "real" clock_shift nil)
    (integer nonempty-type-from-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 "nonneg_real" clock_shift nil)
    (posreal nonempty-type-eq-decl nil real_types 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)
    (Clock_rewrite formula-decl nil inverse_clocks nil)
    (clock_edge? const-decl "bool" physical_clocks nil)
    (all_clock_edge? const-decl "bool" clock_shift nil))
   shostak))
(offset_drift 0
  (offset_drift-1 nil 3356340216
   ("" (skosimp*)
    (("" (expand "offset")
      (("" (use "relative_drift")
        (("" (assert)
          (("" (move-terms 1 r 3)
            (("" (move-terms -1 r 3)
              ((""
                (invoke (then (case "%1 < %2") (assert) (hide -1 2))
                 (! -1 r) (! 1 r))
                (("" (use "Clock_lower")
                  (("" (lemma "Clock_upper")
                    (("" (inst - "c!1(n1!1)" "local_event!1(n1!1)")
                      (("" (use "drift_right_nat")
                        (("" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((offset const-decl "real" clock_shift 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)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Clock_lower formula-decl nil inverse_clocks nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (drift_right_nat formula-decl nil physical_clocks nil)
    (Clock_upper formula-decl nil inverse_clocks nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (drift const-decl "nonneg_real" physical_clocks nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_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)
    (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)
    (C const-decl "int" inverse_clocks nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (N formal-const-decl "posnat" clock_shift nil)
    (below type-eq-decl nil naturalnumbers nil)
    (rho formal-const-decl "nonneg_real" clock_shift 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)
    (relative_drift formula-decl nil physical_clocks nil))
   shostak))
(offset_nondecreasing 0
  (offset_nondecreasing-1 nil 3403617770
   ("" (skosimp*)
    (("" (expand "offset")
      (("" (rewrite "clock_nondecreasing")
        (("" (isolate 1 r 1)
          (("" (assert) (("" (rewrite "Clock_nondecreasing") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((offset const-decl "real" clock_shift nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (Clock_nondecreasing formula-decl nil inverse_clocks nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (rho formal-const-decl "nonneg_real" clock_shift 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)
    (integer nonempty-type-from-decl nil integers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "posnat" clock_shift nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (C const-decl "int" inverse_clocks nil)
    (good_clock nonempty-type-eq-decl nil physical_clocks nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rate const-decl "posreal" physical_clocks nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (clock_nondecreasing formula-decl nil physical_clocks nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   shostak))
(offset_drift_edge 0
  (offset_drift_edge-1 nil 3403544266
   ("" (skosimp*)
    (("" (expand "offset")
      (("" (expand "clock_edge?")
        (("" (skosimp*)
          (("" (replace*)
            (("" (hide -1 -2)
              (("" (rewrite "Clock_rewrite")
                (("" (rewrite "Clock_rewrite")
                  (("" (use "relative_drift") (("" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((offset const-decl "real" clock_shift nil)
    (relative_drift formula-decl nil physical_clocks nil)
    (rho formal-const-decl "nonneg_real" clock_shift 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)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "posnat" clock_shift nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (Clock_rewrite formula-decl nil inverse_clocks nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (clock_edge? const-decl "bool" physical_clocks nil))
   nil))
(double_offset 0
  (double_offset-1 nil 3356340325
   ("" (skosimp*)
    (("" (apply-extensionality :hide? t)
      (("" (expand "offset")
        (("" (assert)
          (("" (rewrite "Clock_rewrite") (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (< 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)
    (N formal-const-decl "posnat" clock_shift nil)
    (below type-eq-decl nil naturalnumbers nil)
    (offset const-decl "real" clock_shift nil)
    (integer nonempty-type-from-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 "nonneg_real" clock_shift nil)
    (posreal nonempty-type-eq-decl nil real_types 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)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (C const-decl "int" inverse_clocks nil)
    (Clock_rewrite formula-decl nil inverse_clocks nil))
   shostak))
(offset_same 0
  (offset_same-1 nil 3356422620
   ("" (skosimp*)
    (("" (prop)
      (("1" (lemma "congruence[below(N), real]")
        (("1" (inst?)
          (("1" (apply-extensionality :hide? t)
            (("1" (inst - "x!1" "x!1")
              (("1" (hide -2)
                (("1" (expand "offset")
                  (("1" (expand "same_edges?")
                    (("1" (inst?)
                      (("1" (expand "offset_clocks?")
                        (("1" (skosimp*)
                          (("1" (invoke (inst-cp - "%1") (! -1 l 1))
                            (("1" (invoke (inst - "%1") (! 1 l 1))
                              (("1"
                                (replace*)
                                (("1"
                                  (hide -1 -2)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (forward-chain "clock_eq_arg")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "double_offset")
        (("2" (inst-cp - "T1!1" "T2!1" "c1!1" "le1!1")
          (("2" (inst - "T1!1" "T2!1" "c2!1" "le2!1")
            (("2" (assert)
              (("2" (replace -1 :dir rl :hide? t)
                (("2" (replace -1 :dir rl :hide? t)
                  (("2" (replace -1 :dir rl :hide? t)
                    (("2" (expand "offset")
                      (("2" (apply-extensionality :hide? t)
                        (("2" (rewrite "Clock_rewrite")
                          (("2" (expand "same_edges?")
                            (("2" (inst?)
                              (("2"
                                (expand "offset_clocks?")
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (invoke
                                     (inst-cp - "%1")
                                     (! 1 r 1 1 1 1))
                                    (("2"
                                      (replace*)
                                      (("2"
                                        (rewrite "Clock_rewrite")
                                        (("2"
                                          (hide -2)
                                          (("2"
                                            (inst?)
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((int_plus_int_is_int application-judgement "int" 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (rho formal-const-decl "nonneg_real" clock_shift 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)
    (integer nonempty-type-from-decl nil integers nil)
    (offset const-decl "real" clock_shift nil)
    (clock_eq_arg formula-decl nil physical_clocks nil)
    (C const-decl "int" inverse_clocks nil)
    (offset_clocks? const-decl "bool" physical_clocks nil)
    (same_edges? const-decl "bool" clock_shift nil)
    (congruence formula-decl nil functions 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)
    (< 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)
    (N formal-const-decl "posnat" clock_shift nil)
    (below type-eq-decl nil naturalnumbers nil)
    (Clock_rewrite formula-decl nil inverse_clocks nil)
    (double_offset formula-decl nil clock_shift nil))
   shostak))
(offset_same2 0
  (offset_same2-1 nil 3356696194
   ("" (skosimp*)
    (("" (lemma "offset_same")
      (("" (inst - "T1!1" 0 "c1!1" "c2!1" "le1!1" "le2!1")
        (("" (assert)
          (("" (replace -1 :hide? t)
            (("" (rewrite "offset_zero")
              (("" (rewrite "offset_zero") (("" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((offset_same formula-decl nil clock_shift nil)
    (offset_zero formula-decl nil clock_shift 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" clock_shift nil)
    (posreal nonempty-type-eq-decl nil real_types 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)
    (below type-eq-decl nil naturalnumbers nil)
    (N formal-const-decl "posnat" clock_shift nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_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)
    (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))
   shostak)))

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.