Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
products/sources/formale Sprachen/PVS/sigma_set/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: LimitModsTest.java   Sprache: Lisp

Original von: PVS©
(denumerable_enumeration
 (denumerable_enumeration_TCC1 0
  (denumerable_enumeration_TCC1-1 nil 3322365875
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "is_countably_infinite")
        (("" (skosimp)
          (("" (typepred "f!1")
            (("" (lemma "bijective_inverse_exists" ("f" "f!1"))
              (("" (expand "exists1")
                (("" (flatten)
                  (("" (skolem - "g")
                    ((""
                      (lemma "bij_inv_is_bij_alt" ("f" "f!1" "g" "g"))
                      (("1" (expand "nonempty?")
                        (("1" (expand "empty?")
                          (("1" (inst - "g")
                            (("1" (expand "member")
                              (("1" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil denumerable_enumeration nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (exists1 const-decl "bool" exists1 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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (bijective? const-decl "bool" functions nil))
   shostak))
 (denumerable_enumeration_bij 0
  (denumerable_enumeration_bij-1 nil 3322366032
   ("" (skosimp)
    (("" (expand "denumerable_enumeration") (("" (propax) nil nil))
      nil))
    nil)
   ((denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil))
   shostak))
 (denumerable_enumeration_image 0
  (denumerable_enumeration_image-1 nil 3322366048
   ("" (skosimp)
    (("" (expand "restrict")
      (("" (expand "fullset")
        (("" (expand "image")
          (("" (apply-extensionality :hide? t)
            (("" (lemma "denumerable_enumeration_bij" ("X" "X!1"))
              (("" (expand "bijective?")
                (("" (flatten)
                  (("" (expand "surjective?")
                    (("" (inst - "x!1")
                      (("" (skosimp)
                        (("" (inst + "x!2") (("" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((restrict const-decl "R" restrict nil)
    (image const-decl "set[R]" function_image nil)
    (denumerable_enumeration_bij formula-decl nil
     denumerable_enumeration nil)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions 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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (TRUE const-decl "bool" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil denumerable_enumeration nil)
    (fullset const-decl "set" sets nil))
   shostak)))


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



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
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