Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: denumerable_enumeration.prf 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)))

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