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

products/sources/formale sprachen/PVS/groups/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: parallel_3D.prf   Sprache: PVS

Original von: PVS©
(bounded_sets
 (least_bounded_above_is_bounded_above 0
  (least_bounded_above_is_bounded_above-1 nil 3315154466
   ("" (skolem-typepred)
    ((""
      (expand* "least_bounded_above?" "bounded_above?"
       "least_upper_bound?")
      (("" (skosimp) (("" (inst? +) nil nil)) nil)) nil))
    nil)
   ((bounded_above? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (greatest_bounded_below_is_bounded_below 0
  (greatest_bounded_below_is_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    ((""
      (expand* "greatest_bounded_below?" "bounded_below?"
       "greatest_lower_bound?")
      (("" (skosimp) (("" (inst? +) nil nil)) nil)) nil))
    nil)
   ((bounded_below? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (bounded_is_bounded_above 0
  (bounded_is_bounded_above-1 nil 3315154466
   ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil bounded_sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (bounded_above? const-decl "bool" bounded_orders nil))
   nil))
 (bounded_is_bounded_below 0
  (bounded_is_bounded_below-1 nil 3315154466
   ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil bounded_sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (bounded_below? const-decl "bool" bounded_orders nil))
   nil))
 (tightly_bounded_is_bounded 0
  (tightly_bounded_is_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "tightly_bounded?" "bounded?")
      (("" (rewrite "least_bounded_above_is_bounded_above")
        (("" (rewrite "greatest_bounded_below_is_bounded_below") nil
          nil))
        nil))
      nil))
    nil)
   ((bounded? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below_is_bounded_below judgement-tcc nil
     bounded_sets nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (least_bounded_above_is_bounded_above judgement-tcc nil
     bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (tightly_bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (tightly_bounded_above 0
  (tightly_bounded_above-1 nil 3315154466 ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (tightly_bounded? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil bounded_sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil))
   nil))
 (tightly_bounded_below 0
  (tightly_bounded_below-1 nil 3315154466 ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (tightly_bounded? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (least_bounded_above? const-decl "bool" bounded_orders nil)
    (least_upper_bound? const-decl "bool" bounded_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (T formal-type-decl nil bounded_sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_lower_bound? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below? const-decl "bool" bounded_orders nil))
   nil))
 (intersection1_preserves_bounded_above 0
  (intersection1_preserves_bounded_above-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "bounded_above?" "upper_bound?")
      (("" (skolem!)
        (("" (inst? +)
          (("" (skolem-typepred)
            (("" (expand* "intersection" "member")
              (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (Su!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (S!1 skolem-const-decl "set[T]" bounded_sets nil)
    (r!1 skolem-const-decl "(intersection[T](Su!1, S!1))" bounded_sets
     nil)
    (intersection const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (intersection2_preserves_bounded_above 0
  (intersection2_preserves_bounded_above-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "bounded_above?" "upper_bound?")
      (("" (skolem!)
        (("" (inst? +)
          (("" (skolem-typepred)
            (("" (expand* "intersection" "member")
              (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (Su!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (S!1 skolem-const-decl "set[T]" bounded_sets nil)
    (r!1 skolem-const-decl "(intersection[T](S!1, Su!1))" bounded_sets
     nil)
    (intersection const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (difference_preserves_bounded_above 0
  (difference_preserves_bounded_above-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (rewrite "difference_intersection")
      (("" (rewrite "intersection1_preserves_bounded_above") nil nil))
      nil))
    nil)
   ((difference_intersection formula-decl nil sets_lemmas nil)
    (intersection1_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (intersection1_preserves_bounded_above judgement-tcc nil
     bounded_sets nil)
    (complement const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (remove_preserves_bounded_above 0
  (remove_preserves_bounded_above-1 nil 3315154466
   ("" (skolem!)
    (("" (rewrite "remove_as_difference")
      (("" (rewrite "difference_preserves_bounded_above") nil nil))
      nil))
    nil)
   ((remove_as_difference formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bounded_above? const-decl "bool" bounded_orders nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" bounded_sets nil)
    (difference_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (difference_preserves_bounded_above judgement-tcc nil bounded_sets
     nil))
   nil))
 (intersection1_preserves_bounded_below 0
  (intersection1_preserves_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "bounded_below?" "lower_bound?")
      (("" (skolem!)
        (("" (inst? +)
          (("" (skolem-typepred)
            (("" (expand* "intersection" "member")
              (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (Sl!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (S!1 skolem-const-decl "set[T]" bounded_sets nil)
    (r!1 skolem-const-decl "(intersection[T](Sl!1, S!1))" bounded_sets
     nil)
    (intersection const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (intersection2_preserves_bounded_below 0
  (intersection2_preserves_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand* "bounded_below?" "lower_bound?")
      (("" (skolem!)
        (("" (inst? +)
          (("" (skolem-typepred)
            (("" (expand* "intersection" "member")
              (("" (flatten) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (Sl!1 skolem-const-decl
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (S!1 skolem-const-decl "set[T]" bounded_sets nil)
    (r!1 skolem-const-decl "(intersection[T](S!1, Sl!1))" bounded_sets
     nil)
    (intersection const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (difference_preserves_bounded_below 0
  (difference_preserves_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (rewrite "difference_intersection")
      (("" (rewrite "intersection1_preserves_bounded_below") nil nil))
      nil))
    nil)
   ((difference_intersection formula-decl nil sets_lemmas nil)
    (intersection1_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (intersection1_preserves_bounded_below judgement-tcc nil
     bounded_sets nil)
    (complement const-decl "set" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (remove_preserves_bounded_below 0
  (remove_preserves_bounded_below-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (rewrite "remove_as_difference")
      (("" (rewrite "difference_preserves_bounded_below") nil nil))
      nil))
    nil)
   ((remove_as_difference formula-decl nil sets_lemmas nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" bounded_sets nil)
    (difference_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (difference_preserves_bounded_below judgement-tcc nil bounded_sets
     nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (intersection1_preserves_bounded 0
  (intersection1_preserves_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand "bounded?") (("" (ground) nil nil)) nil)) nil)
   ((intersection1_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (intersection1_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (intersection2_preserves_bounded 0
  (intersection2_preserves_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand "bounded?") (("" (ground) nil nil)) nil)) nil)
   ((intersection2_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (intersection2_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (difference_preserves_bounded 0
  (difference_preserves_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand "bounded?") (("" (ground) nil nil)) nil)) nil)
   ((difference_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (difference_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (remove_preserves_bounded 0
  (remove_preserves_bounded-1 nil 3315154466
   ("" (skolem-typepred)
    (("" (expand "bounded?") (("" (ground) nil nil)) nil)) nil)
   ((remove_preserves_bounded_above application-judgement
     "(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_sets nil)
    (remove_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_sets nil)
    (R formal-const-decl "pred[[T, T]]" bounded_sets nil)
    (bounded? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil bounded_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)))


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


Eine klare Vorstellung vom Zielzustand

                                                                                                                                                                                                                                                                                                                                                                                                     

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