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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: DiagramScene.java   Sprache: Lisp

Original von: PVS©
(interval_reals
 (open_ball?_lem 0
  (open_ball?_lem-1 nil 3258223423 3292322828
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "open_ball?")
        (("1" (skosimp*)
          (("1" (expand "open_ball")
            (("1" (expand "subset?")
              (("1" (expand "member")
                (("1" (inst + "delta!1") nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "open_ball?")
        (("2" (skosimp*)
          (("2" (expand "subset?")
            (("2" (expand "member")
              (("2" (expand "open_ball") (("2" (inst + "r!1") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((subset? const-decl "bool" sets 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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (member const-decl "bool" sets nil)
    (open_ball const-decl "set[T]" open_sets nil)
    (open_ball? const-decl "bool" open_sets nil))
   30503 110 nil nil))
 (open?_lem 0
  (open?_lem-1 nil 3258223381 3292322828
   ("" (skosimp*) (("" (expand "open?") (("" (inst?) nil nil)) nil))
    nil)
   unchecked
   ((open? const-decl "bool" open_sets 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)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (T formal-subtype-decl nil open_sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) nil nil)
   20 20 t shostak))
 (Open_empty 0
  (Open_empty-1 nil 3320064681 3320064682 ("" (skosimp*) nil nil)
   proved nil 1331 130 t shostak))
 (open_intv_open 0
  (open_intv_open-1 nil 3258299476 3292322828
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (inst + "min(x!1 -a!1,b!1-x!1)")
            (("1" (skosimp*) (("1" (grind) nil nil)) nil)
             ("2" (grind) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((open? const-decl "bool" open_sets nil)
    (open_ball? const-decl "bool" open_sets nil)
    (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (T formal-subtype-decl nil open_sets nil)
    (< const-decl "bool" reals nil) nil nil nil
    (> const-decl "bool" reals nil))
   224 220 t shostak))
 (above_intv_open 0
  (above_intv_open-1 nil 3258299818 3292322829
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (inst + "x!1-a!1")
            (("" (skosimp*) (("" (grind) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((open? const-decl "bool" open_sets nil)
    (open_ball? const-decl "bool" open_sets nil)
    (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
    (T formal-subtype-decl nil open_sets nil)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (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))
   99 100 t shostak))
 (below_intv_open 0
  (below_intv_open-1 nil 3258299894 3292322829
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (inst + "a!1-x!1") (("" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   unchecked
   ((open? const-decl "bool" open_sets nil)
    (open_ball? const-decl "bool" open_sets nil)
    (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (T formal-subtype-decl nil open_sets nil)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (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))
   103 110 nil nil))
 (union_open 0
  (union_open-1 nil 3258299981 3292322829
   ("" (skosimp*)
    (("" (expand "open?")
      (("" (skosimp*)
        (("" (expand "open_ball?")
          (("" (typepred "x!1")
            (("" (expand "union")
              (("" (expand "member")
                (("" (split -2)
                  (("1" (hide -4)
                    (("1" (inst?)
                      (("1" (skosimp*)
                        (("1" (inst + "delta!1")
                          (("1" (skosimp*)
                            (("1" (inst - "y!1")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -3)
                    (("2" (inst?)
                      (("2" (skosimp*)
                        (("2" (inst + "delta!1")
                          (("2" (skosimp*)
                            (("2" (inst - "y!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((open? const-decl "bool" open_sets nil)
    (open_ball? const-decl "bool" open_sets nil) nil nil 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)
    (member const-decl "bool" sets 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)
    (T_pred const-decl "[real -> boolean]" open_sets nil)
    (T formal-subtype-decl nil open_sets nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil))
   165 170 t shostak))
 (closed_intv_closed 0
  (closed_intv_closed-1 nil 3258299631 3292322829
   ("" (skosimp*)
    (("" (expand "closed?")
      ((""
        (case-replace "complement(LAMBDA (x): a!1 <= x AND x <= b!1) =
             union(above_intv(b!1),below_intv(a!1))")
        (("1" (hide -1)
          (("1" (lemma "union_open")
            (("1" (inst?)
              (("1" (assert)
                (("1" (hide 2)
                  (("1" (lemma "above_intv_open ")
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (lemma "below_intv_open ")
                          (("1" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (apply-extensionality 1 :hide? t)
            (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((closed? const-decl "bool" open_sets nil)
    (member const-decl "bool" sets nil)
    (below_intv_open formula-decl nil open_sets nil)
    (above_intv_open formula-decl nil open_sets nil)
    (union_open formula-decl nil open_sets nil)
    (< const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (union const-decl "set" sets nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (complement const-decl "set" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil open_sets nil)
    (T_pred const-decl "[real -> boolean]" open_sets 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))
   203 160 t shostak)))


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