products/sources/formale Sprachen/PVS/fault_tolerance/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: clock_minmax.prf   Sprache: Lisp

Original von: PVS©
(clock_minmax
 (clock_min_witness 0
  (clock_min_witness-1 nil 3389336991
   ("" (skosimp*)
    (("" (expand "clock_min")
      (("" (typepred "min(image(t_at(T!1), participant!1))")
        (("" (hide -2)
          (("" (rewrite "image" -)
            (("" (expand "t_at")
              (("" (skosimp*)
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((clock_min const-decl "real" clock_minmax nil)
    (nonempty_image application-judgement "(nonempty?[R])" clock_minmax
     nil)
    (nonempty_finite_image application-judgement
     "non_empty_finite_set[real]" clock_minmax nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[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)
    (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)
    (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" clock_minmax 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)
    (image const-decl "set[R]" function_image nil)
    (t_at const-decl "real" clock_minmax nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (min const-decl
         "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}"
         finite_sets_minmax "finite_sets/"))
   shostak))
 (clock_max_witness 0
  (clock_max_witness-1 nil 3389337114
   ("" (skosimp*)
    (("" (expand "clock_max")
      (("" (typepred "max(image(t_at(T!1), participant!1))")
        (("" (hide -2)
          (("" (rewrite "image" -)
            (("" (expand "t_at")
              (("" (skosimp*)
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((clock_max const-decl "real" clock_minmax nil)
    (nonempty_image application-judgement "(nonempty?[R])" clock_minmax
     nil)
    (nonempty_finite_image application-judgement
     "non_empty_finite_set[real]" clock_minmax nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[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)
    (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)
    (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" clock_minmax 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)
    (image const-decl "set[R]" function_image nil)
    (t_at const-decl "real" clock_minmax nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (max const-decl
         "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
         finite_sets_minmax "finite_sets/"))
   shostak))
 (clock_min_is_min 0
  (clock_min_is_min-1 nil 3389337201
   ("" (skosimp*)
    (("" (expand "clock_min")
      (("" (typepred "min(image(t_at(T!1), participant!1))")
        (("" (hide -1)
          (("" (inst?)
            (("" (assert)
              (("" (rewrite "image")
                (("" (expand "t_at") (("" (inst?) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((clock_min const-decl "real" clock_minmax nil)
    (nonempty_image application-judgement "(nonempty?[R])" clock_minmax
     nil)
    (nonempty_finite_image application-judgement
     "non_empty_finite_set[real]" clock_minmax nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[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)
    (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)
    (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" clock_minmax 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)
    (image const-decl "set[R]" function_image nil)
    (t_at const-decl "real" clock_minmax nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (min const-decl
         "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}"
         finite_sets_minmax "finite_sets/"))
   shostak))
 (clock_max_is_max 0
  (clock_max_is_max-1 nil 3389337260
   ("" (skosimp*)
    (("" (expand "clock_max")
      (("" (invoke (typepred "%1") (! 1 r))
        (("" (hide -1)
          (("" (inst?)
            (("" (assert)
              (("" (hide 2)
                (("" (expand* "image" "t_at") (("" (inst?) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((clock_max const-decl "real" clock_minmax nil)
    (max const-decl
         "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
         finite_sets_minmax "finite_sets/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (t_at const-decl "real" clock_minmax nil)
    (image const-decl "set[R]" function_image 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 "nonneg_real" clock_minmax 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)
    (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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonempty_finite_image application-judgement
     "non_empty_finite_set[real]" clock_minmax nil)
    (nonempty_image application-judgement "(nonempty?[R])" clock_minmax
     nil))
   shostak))
 (clock_min_clock 0
  (clock_min_clock-1 nil 3389336989
   ("" (skosimp*)
    (("" (prop)
      (("1" (use "clock_min_witness")
        (("1" (skosimp*)
          (("1" (replace -2 :hide? t)
            (("1" (use "clock_min_is_min")
              (("1" (typepred "c!1")
                (("1" (inst - "T!1")
                  (("1" (flatten) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "clock_min_witness")
        (("2" (inst - "T!1" _)
          (("2" (inst?)
            (("2" (skosimp*)
              (("2" (replace -2 :hide? t)
                (("2" (use "clock_min_is_min")
                  (("2" (typepred "c!1")
                    (("2" (inst - "T!1")
                      (("2" (flatten) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((clock_min_is_min formula-decl nil clock_minmax nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (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)
    (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" clock_minmax 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)
    (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)
    (clock_min_witness formula-decl nil clock_minmax nil))
   nil))
 (clock_max_clock 0
  (clock_max_clock-1 nil 3389336989
   ("" (skosimp*)
    (("" (prop)
      (("1" (lemma "clock_max_witness")
        (("1" (inst - "T!1" _)
          (("1" (inst?)
            (("1" (skosimp*)
              (("1" (replace -2 :hide? t)
                (("1" (lemma "clock_max_is_max")
                  (("1" (inst - "1 + T!1" _ _)
                    (("1" (inst?)
                      (("1" (typepred "c!1")
                        (("1" (inst - "T!1")
                          (("1" (flatten) (("1" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (use "clock_max_witness")
        (("2" (skosimp*)
          (("2" (replace -2 :hide? t)
            (("2" (lemma "clock_max_is_max")
              (("2" (inst - "T!1" _ _)
                (("2" (inst?)
                  (("2" (typepred "c!1")
                    (("2" (inst - "T!1")
                      (("2" (flatten) (("2" (assert) nil nil)) nil))
                      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)
    (clock_max_is_max formula-decl nil clock_minmax nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" 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 "nonneg_real" clock_minmax 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)
    (clock_max_witness formula-decl nil clock_minmax nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   nil)))


¤ Dauer der Verarbeitung: 0.24 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.


Bot Zugriff