Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/sets_aux/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: countable_setofsets.prf Sprache: Lisp

Original von: PVS^©

(countable_setofsets
(countable_union1 0
  (countable_union1-1 nil 3317055771
   ("" (expand* "is_countable" "every")
    (("" (skosimp* t)
      (("" (lemma "countable_nat_tuple")
        ((""
          (case "EXISTS (f: [(Union(S!1)) -> [nat, nat]]): injective?(f)")
          (("1" (skosimp*)
            (("1" (expand "bijective?")
              (("1" (flatten)
                (("1"
                  (use "composition_injective[(Union(S!1)), [nat, nat], nat]")
                  (("1" (inst? +) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2"
            (case "EXISTS (f: [R: (S!1) -> (injective?[(R), nat])]): TRUE")
            (("1" (skosimp* t)
              (("1"
                (inst +
                 "LAMBDA (t: (Union(S!1))): (f!1(choose({R: (S!1) | R(t)})), f!2(choose({R: (S!1) | R(t)}))(t))")
                (("1" (expand "injective?")
                  (("1" (skosimp :preds? t)
                    (("1"
                      (inst - "choose({R: (S!1) | R(x1!1)})"
                       "choose({R: (S!1) | R(x2!1)})")
                      (("1" (assert)
                        (("1"
                          (typepred
                           "f!2(choose({R: (S!1) | R(x1!1)}))")
                          (("1" (expand "injective?")
                            (("1" (inst - "x1!1" "x2!1")
                              (("1" (assert) nil nil)) nil))
                            nil)
                           ("2"
                            (expand* "Union" "nonempty?" "empty?"
                             "member")
                            (("2" (skolem!) (("2" (inst?) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2"
                        (expand* "Union" "nonempty?" "empty?" "member")
                        (("2" (skosimp*) (("2" (inst?) nil nil)) nil))
                        nil)
                       ("3"
                        (expand* "Union" "nonempty?" "empty?" "member")
                        (("3" (skolem!) (("3" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skolem!) (("2" (assert) nil nil)) nil)
                 ("3" (skolem-typepred)
                  (("3" (expand* "Union" "nonempty?" "empty?" "member")
                    (("3" (skolem!) (("3" (inst?) nil nil)) nil)) nil))
                  nil))
                nil))
              nil)
             ("2"
              (inst +
               "LAMBDA (R: (S!1)): choose({f: [(R) -> nat] | injective?(f)})")
              (("2" (skolem!)
                (("2" (inst - "R!1")
                  (("2" (skosimp* t)
                    (("2" (expand* "nonempty?" "empty?" "member")
                      (("2" (inst - "f!3") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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_setofsets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (Union const-decl "set" sets nil)
    (bijective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (f!2 skolem-const-decl "[(Union(S!1)) -> [nat, nat]]"
     countable_setofsets nil)
    (S!1 skolem-const-decl "setofsets[T]" countable_setofsets nil)
    (f!3 skolem-const-decl "[[nat, nat] -> nat]" countable_setofsets
     nil)
    (O const-decl "T3" function_props nil)
    (x1!1 skolem-const-decl "(Union(S!1))" countable_setofsets nil)
    (x2!1 skolem-const-decl "(Union(S!1))" countable_setofsets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (TRUE const-decl "bool" booleans nil)
    (countable_nat_tuple formula-decl nil countable_set nil)
    (is_countable const-decl "bool" countability nil)
    (every const-decl "bool" sets nil))
   shostak))
(countable_union2 0
  (countable_union2-1 nil 3317056043
   ("" (expand* "is_countable" "every")
    (("" (skosimp* t)
      (("" (inst + "LAMBDA (t: (x!1)): f!1(t)")
        (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
      nil))
    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)
    (Union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil countable_setofsets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (f!1 skolem-const-decl "(injective?[(Union(S!1)), nat])"
     countable_setofsets nil)
    (x!1 skolem-const-decl "(S!1)" countable_setofsets nil)
    (S!1 skolem-const-decl "setofsets[T]" countable_setofsets nil)
    (is_countable const-decl "bool" countability nil)
    (every const-decl "bool" sets nil))
   shostak))
(countable_intersection 0
  (countable_intersection-1 nil 3317056085
   ("" (expand* "nonempty?" "empty?" "member" "every" "is_countable")
    (("" (skosimp*)
      (("" (inst - "x!1")
        (("" (skolem-typepred)
          (("" (inst + "LAMBDA (t: (Intersection(S!1))): f!1(t)")
            (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans 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)
    (injective? const-decl "bool" functions nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (f!1 skolem-const-decl "(injective?[(x!1), nat])"
     countable_setofsets nil)
    (set type-eq-decl nil sets nil)
    (Intersection const-decl "set" sets nil)
    (T formal-type-decl nil countable_setofsets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (S!1 skolem-const-decl "setofsets[T]" countable_setofsets nil)
    (x!1 skolem-const-decl "setof[T]" countable_setofsets nil)
    (nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (is_countable const-decl "bool" countability nil)
    (every const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil))
   shostak))
(countable_finite_subsets 0
  (countable_finite_subsets-1 nil 3317055726
   ("" (skolem-typepred)
    (("" (expand "is_countable")
      (("" (lemma "countable_family_nat")
        (("" (skosimp* t)
          ((""
            (inst +
             "LAMBDA (Q: (finite_subsets(S!1))): f!1(image(f!2, Q))")
            (("" (expand* "bijective?" "injective?" "surjective?")
              (("" (skosimp :preds? t)
                ((""
                  (inst -7
                   "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](x1!1))"
                   "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](x2!1))")
                  (("" (assert)
                    (("" (decompose-equality -7)
                      (("" (expand "image" -1)
                        (("" (apply-extensionality :hide? t)
                          ((""
                            (expand* "finite_subsets" "subset?"
                             "member")
                            (("" (iff)
                              ((""
                                (prop)
                                (("1"
                                  (inst -4 "x!1")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (inst - "f!2(x!1)")
                                      (("1"
                                        (iff)
                                        (("1"
                                          (prop)
                                          (("1"
                                            (skosimp* t)
                                            (("1"
                                              (expand "restrict")
                                              (("1"
                                                (inst - "x!1" "x!3")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (inst 2 "x!1")
                                            (("2"
                                              (expand "restrict")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (inst -6 "x!1")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (inst - "f!2(x!1)")
                                      (("2"
                                        (iff)
                                        (("2"
                                          (prop)
                                          (("1"
                                            (skosimp* t)
                                            (("1"
                                              (expand "restrict")
                                              (("1"
                                                (inst - "x!1" "x!2")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (inst + "x!1")
                                            (("2"
                                              (expand "restrict")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (x2!1 skolem-const-decl "(finite_subsets(S!1))" countable_setofsets
     nil)
    (x!1 skolem-const-decl "T" countable_setofsets nil)
    (x1!1 skolem-const-decl "(finite_subsets(S!1))" countable_setofsets
     nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (S!1 skolem-const-decl "countable_set[T]" countable_setofsets nil)
    (f!1 skolem-const-decl "[finite_set[nat] -> nat]"
     countable_setofsets nil)
    (f!2 skolem-const-decl "(injective?[(S!1), nat])"
     countable_setofsets nil)
    (restrict const-decl "R" restrict nil)
    (image const-decl "set[R]" function_image nil)
    (finite_subsets const-decl "set[finite_set[T]]" countable_setofsets
     nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_restrict application-judgement "finite_set[S]"
     restrict_set_props nil)
    (finite_image application-judgement "finite_set[R]"
     function_image_aux nil)
    (countable_family_nat formula-decl nil countable_set nil)
    (countable_set nonempty-type-eq-decl nil countability nil)
    (is_countable const-decl "bool" countability nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countable_setofsets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(countably_infinite_finite_subsets 0
  (countably_infinite_finite_subsets-1 nil 3317055726
   ("" (skolem-typepred)
    (("" (expand "is_countably_infinite")
      (("" (lemma "countable_family_nat")
        (("" (skosimp* t)
          ((""
            (inst +
             "LAMBDA (Q: (finite_subsets(S!1))): f!1(image(f!2, Q))")
            (("" (expand* "bijective?" "injective?" "surjective?")
              (("" (prop)
                (("1" (skosimp :preds? t)
                  (("1"
                    (inst -8
                     "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](x1!1))"
                     "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](x2!1))")
                    (("1" (assert)
                      (("1" (decompose-equality -8)
                        (("1" (expand "image" -1)
                          (("1" (apply-extensionality :hide? t)
                            (("1" (iff)
                              (("1"
                                (prop)
                                (("1"
                                  (expand*
                                   "finite_subsets"
                                   "subset?"
                                   "member")
                                  (("1"
                                    (inst -4 "x!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (inst - "f!2(x!1)")
                                        (("1"
                                          (iff)
                                          (("1"
                                            (prop)
                                            (("1"
                                              (skosimp* t)
                                              (("1"
                                                (expand "restrict")
                                                (("1"
                                                  (inst - "x!1" "x!3")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (inst 2 "x!1")
                                              (("2"
                                                (expand "restrict")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand*
                                   "finite_subsets"
                                   "subset?"
                                   "member")
                                  (("2"
                                    (inst -6 "x!1")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (inst - "f!2(x!1)")
                                        (("2"
                                          (iff)
                                          (("2"
                                            (prop)
                                            (("1"
                                              (skosimp* t)
                                              (("1"
                                                (expand "restrict")
                                                (("1"
                                                  (inst - "x!1" "x!2")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (inst + "x!1")
                                              (("2"
                                                (expand "restrict")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skolem!)
                  (("2" (inst -4 "y!1")
                    (("2" (skolem!)
                      (("2" (inst + "{t: (S!1) | x!1(f!2(t))}")
                        (("1"
                          (case "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](extend[T, (S!1), bool, FALSE]({t: (S!1) | x!1(f!2(t))}))) = x!1")
                          (("1" (assert) nil nil)
                           ("2" (delete 2)
                            (("2" (expand* "restrict" "extend" "image")
                              (("2"
                                (apply-extensionality :hide? t)
                                (("2"
                                  (iff)
                                  (("2"
                                    (smash)
                                    (("2"
                                      (inst - "x!2")
                                      (("2"
                                        (skolem!)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (inst + "x!3")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (split)
                          (("1" (typepred "x!1")
                            (("1" (expand "is_finite")
                              (("1"
                                (skolem!)
                                (("1"
                                  (inst
                                   +
                                   "N!1"
                                   "LAMBDA (w: (extend[T, (S!1), bool, FALSE]({t: (S!1) | x!1(f!2(t))}))): f!3(f!2(w))")
                                  (("1"
                                    (expand "injective?")
                                    (("1"
                                      (skosimp :preds? t)
                                      (("1"
                                        (expand "extend")
                                        (("1"
                                          (prop)
                                          (("1"
                                            (inst
                                             -
                                             "f!2(x1!1)"
                                             "f!2(x2!1)")
                                            (("1"
                                              (inst - "x1!1" "x2!1")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (skolem-typepred)
                                    (("2"
                                      (expand "extend")
                                      (("2" (prop) nil nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (skolem-typepred)
                                    (("3"
                                      (expand "extend")
                                      (("3" (prop) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (grind) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? 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)
    (injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (x!1 skolem-const-decl "finite_set[nat]" countable_setofsets nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (countable_finite_subsets application-judgement
     "countable_set[finite_set[T]]" countable_setofsets nil)
    (x2!1 skolem-const-decl "(finite_subsets(S!1))" countable_setofsets
     nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (x1!1 skolem-const-decl "(finite_subsets(S!1))" countable_setofsets
     nil)
    (x!1 skolem-const-decl "T" countable_setofsets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (S!1 skolem-const-decl "countably_infinite_set[T]"
     countable_setofsets nil)
    (f!1 skolem-const-decl "[finite_set[nat] -> nat]"
     countable_setofsets nil)
    (f!2 skolem-const-decl "(bijective?[(S!1), nat])"
     countable_setofsets nil)
    (restrict const-decl "R" restrict nil)
    (image const-decl "set[R]" function_image nil)
    (finite_subsets const-decl "set[finite_set[T]]" countable_setofsets
     nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_restrict application-judgement "finite_set[S]"
     restrict_set_props nil)
    (finite_image application-judgement "finite_set[R]"
     function_image_aux nil)
    (countable_family_nat formula-decl nil countable_set nil)
    (countably_infinite_set type-eq-decl nil countability nil)
    (is_countably_infinite const-decl "bool" countability nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countable_setofsets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)))