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

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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: HoTT.nix   Sprache: SML

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)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.29Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff

                                                                                                                                                                                                                                                                                                                                                                                                     

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