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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: countable_indexed_sets.prf   Sprache: Lisp

Original von: PVS©
(countable_indexed_sets
 (Union_IUnion 0
  (Union_IUnion-1 nil 3423550499
   ("" (skosimp)
    (("" (expand "is_countable")
      (("" (skosimp)
        (("" (typepred "f!1")
          ((""
            (name "ZZ"
                  "lambda (n:nat): if (exists (X:(XS!1)): f!1(X) = n) then choose({X:(XS!1) | f!1(X) = n}) else emptyset[T] endif")
            (("1" (inst + "ZZ")
              (("1" (split 1)
                (("1" (hide -1)
                  (("1" (apply-extensionality :hide? t)
                    (("1" (case-replace "Union(XS!1)(x!1)")
                      (("1" (expand "Union")
                        (("1" (skosimp)
                          (("1" (typepred "a!1")
                            (("1" (expand "IUnion")
                              (("1"
                                (expand "ZZ")
                                (("1"
                                  (expand "emptyset")
                                  (("1"
                                    (inst + "f!1(a!1)")
                                    (("1"
                                      (case
                                       "nonempty?({X: (XS!1) | f!1(X) = f!1(a!1)})")
                                      (("1"
                                        (case-replace
                                         "EXISTS (X: (XS!1)): f!1(X) = f!1(a!1)")
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (lemma
                                             "choose_member[(XS!1)]"
                                             ("a"
                                              "{X: (XS!1) | f!1(X) = f!1(a!1)}"))
                                            (("1"
                                              (split -1)
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (expand "injective?")
                                                  (("1"
                                                    (inst
                                                     -
                                                     "choose({X: (XS!1) | f!1(X) = f!1(a!1)})"
                                                     "a!1")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (expand "nonempty?")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2" (inst + "a!1") nil nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (expand "nonempty?")
                                          (("2"
                                            (expand "empty?")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (inst - "a!1")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (replace 1 2)
                        (("2" (assert)
                          (("2" (expand "IUnion")
                            (("2" (skosimp)
                              (("2"
                                (expand "ZZ")
                                (("2"
                                  (expand "emptyset")
                                  (("2"
                                    (prop)
                                    (("2"
                                      (expand "Union")
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (typepred "X!1")
                                          (("2"
                                            (case
                                             "nonempty?[(XS!1)]({X: (XS!1) | f!1(X) = i!1})")
                                            (("1"
                                              (lemma
                                               "choose_member[(XS!1)]"
                                               ("a"
                                                "{X: (XS!1) | f!1(X) = i!1}"))
                                              (("1"
                                                (split -1)
                                                (("1"
                                                  (expand "member")
                                                  (("1"
                                                    (inst + "X!1")
                                                    (("1"
                                                      (expand
                                                       "injective?")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "choose[(XS!1)]({X: (XS!1) | f!1(X) = i!1})"
                                                         "X!1")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand "nonempty?")
                                                  (("2"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (expand "nonempty?")
                                                (("2"
                                                  (expand "empty?")
                                                  (("2"
                                                    (inst - "X!1")
                                                    (("2"
                                                      (expand "member")
                                                      (("2"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide -1)
                  (("2" (skosimp)
                    (("2" (expand "ZZ")
                      (("2"
                        (case-replace
                         "EXISTS (X: (XS!1)): f!1(X) = n!1")
                        (("1" (hide 1)
                          (("1" (skosimp)
                            (("1"
                              (lemma "choose_member[(XS!1)]"
                               ("a" "{X: (XS!1) | f!1(X) = n!1}"))
                              (("1"
                                (split -1)
                                (("1"
                                  (expand "member")
                                  (("1"
                                    (expand "injective?")
                                    (("1"
                                      (typepred "X!1")
                                      (("1"
                                        (inst
                                         -
                                         "choose[(XS!1)]({X: (XS!1) | f!1(X) = n!1})"
                                         "X!1")
                                        (("1" (assert) nil nil)
                                         ("2"
                                          (expand "nonempty?")
                                          (("2"
                                            (expand "empty?")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (inst - "X!1")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "empty?")
                                  (("2"
                                    (inst - "X!1")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (replace 1 *)
                          (("2" (rewrite "emptyset_is_empty?") nil
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp*)
              (("2" (expand "nonempty?")
                (("2" (expand "empty?")
                  (("2" (typepred "X!1")
                    (("2" (inst - "X!1")
                      (("2" (expand "member") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_countable const-decl "bool" countability nil)
    (injective? const-decl "bool" functions nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (number nonempty-type-decl nil numbers nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil countable_indexed_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (n!1 skolem-const-decl "nat" countable_indexed_sets nil)
    (a!1 skolem-const-decl "(XS!1)" countable_indexed_sets nil)
    (f!1 skolem-const-decl "(injective?[(XS!1), nat])"
     countable_indexed_sets nil)
    (XS!1 skolem-const-decl "setofsets[T]" countable_indexed_sets nil)
    (member const-decl "bool" sets nil)
    (choose_member formula-decl nil sets_lemmas nil)
    (empty? const-decl "bool" sets nil)
    (ZZ skolem-const-decl "[nat -> setof[T]]" countable_indexed_sets
     nil)
    (i!1 skolem-const-decl "nat" countable_indexed_sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (Union const-decl "set" sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil)
    (emptyset const-decl "set" sets nil))
   shostak))
 (Intersection_IIntersection 0
  (Intersection_IIntersection-1 nil 3423553206
   ("" (skosimp)
    (("" (lemma "Union_IUnion" ("XS" "Complement(XS!1)"))
      (("" (split -1)
        (("1" (skosimp)
          (("1" (rewrite "Demorgan2" - :dir rl)
            (("1" (inst + "IComplement(YS!1)")
              (("1" (rewrite "IDemorgan1" + :dir rl)
                (("1" (replace -1 1 rl)
                  (("1" (rewrite "complement_complement")
                    (("1" (skosimp)
                      (("1" (expand "Complement" -2)
                        (("1" (expand "IComplement")
                          (("1" (inst - "n!1")
                            (("1" (split -2)
                              (("1"
                                (hide-all-but (-1 1))
                                (("1"
                                  (rewrite "emptyset_is_empty?")
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (rewrite "complement_emptyset")
                                      (("1"
                                        (rewrite "fullset_is_full?")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (skosimp)
                                (("2"
                                  (typepred "b!1")
                                  (("2"
                                    (replace -2)
                                    (("2"
                                      (rewrite "complement_complement")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (expand "is_countable")
            (("2" (skosimp)
              (("2" (typepred "f!1")
                (("2"
                  (inst +
                   "lambda (x:(Complement(XS!1))): f!1(complement(x))")
                  (("1" (expand "injective?")
                    (("1" (skosimp)
                      (("1"
                        (inst - "complement[T](x1!1)"
                         "complement[T](x2!1)")
                        (("1" (rewrite "complement_equal")
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp)
                    (("2" (typepred "x!1")
                      (("2" (expand "Complement")
                        (("2" (skosimp)
                          (("2" (typepred "b!1")
                            (("2" (replace -2)
                              (("2"
                                (rewrite "complement_complement")
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Complement const-decl "setofsets[T]" sets_lemmas nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil countable_indexed_sets nil)
    (Union_IUnion formula-decl nil countable_indexed_sets nil)
    (complement const-decl "set" sets nil)
    (XS!1 skolem-const-decl "setofsets[T]" countable_indexed_sets nil)
    (f!1 skolem-const-decl "(injective?[(XS!1), nat])"
     countable_indexed_sets nil)
    (complement_equal formula-decl nil sets_lemmas nil)
    (injective? const-decl "bool" functions nil)
    (is_countable const-decl "bool" countability 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)
    (set type-eq-decl nil sets nil)
    (sequence type-eq-decl nil sequences nil)
    (IComplement const-decl "set[T]" indexed_sets_aux nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (complement_emptyset formula-decl nil sets_lemmas nil)
    (fullset_is_full? formula-decl nil sets_lemmas nil)
    (fullset const-decl "set" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (Intersection const-decl "set" sets nil)
    (IDemorgan1 formula-decl nil indexed_sets_aux nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (Demorgan2 formula-decl nil sets_lemmas nil))
   shostak)))


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