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: countability_aux.prf Sprache: Lisp

Original von: PVS^©

(countability_aux
(countable_emptyset 0
  (countable_emptyset-1 nil 3406351233
   ("" (expand "is_countable")
    (("" (inst + "lambda (x:(emptyset[T])): 0")
      (("" (expand "injective?")
        (("" (skosimp)
          (("" (typepred "x1!1")
            (("" (expand "emptyset") (("" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil countability_aux nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (emptyset const-decl "set" sets 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_countable const-decl "bool" countability nil))
   shostak))
(countable_singleton 0
  (countable_singleton-1 nil 3406351272
   ("" (skosimp)
    (("" (expand "is_countable")
      (("" (inst + "lambda (x:(singleton(t!1))):0")
        (("" (expand "injective?")
          (("" (skosimp)
            (("" (typepred "x1!1")
              (("" (typepred "x2!1")
                (("" (expand "singleton") (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_countable const-decl "bool" countability nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (t!1 skolem-const-decl "T" countability_aux 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)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (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 countability_aux nil))
   shostak))
(countable_add 0
  (countable_add-1 nil 3406352219
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "is_countable")
        (("" (skosimp)
          (("" (typepred "f!1")
            (("" (case "X!1(t!1)")
              (("1" (inst + "f!1")
                (("1" (split)
                  (("1" (skosimp)
                    (("1" (expand "add")
                      (("1" (expand "member")
                        (("1" (assert)
                          (("1" (hide -2) (("1" (grind) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "injective?")
                    (("2" (skosimp)
                      (("2" (typepred "x1!1")
                        (("2" (typepred "x2!1")
                          (("2" (expand "add")
                            (("2" (expand "member")
                              (("2"
                                (inst - "x1!1" "x2!1")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2"
                (inst +
                 "lambda (x:(add(t!1, X!1))): if x = t!1 then 0 else f!1(x)+1 endif")
                (("1" (expand "injective?")
                  (("1" (skosimp)
                    (("1" (case-replace "x1!1 = t!1")
                      (("1" (lift-if) (("1" (assert) nil nil)) nil)
                       ("2" (case-replace "x2!1 = t!1")
                        (("1" (lift-if) (("1" (assert) nil nil)) nil)
                         ("2" (assert)
                          (("2" (inst - "x1!1" "x2!1")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skosimp)
                  (("2" (typepred "x!1")
                    (("2" (expand "add")
                      (("2" (expand "member") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_countable const-decl "bool" countability nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countability_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (X!1 skolem-const-decl "(is_countable)" countability_aux nil)
    (t!1 skolem-const-decl "T" countability_aux nil)
    (f!1 skolem-const-decl "(injective?[(X!1), nat])" countability_aux
     nil)
    (add const-decl "(nonempty?)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers 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))
   shostak))
(countable_remove 0
  (countable_remove-1 nil 3406352813
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "is_countable")
        (("" (skosimp)
          (("" (typepred "f!1")
            (("" (case "X!1(t!1)")
              (("1" (inst + "lambda (x:(remove(t!1, X!1))): f!1(x)")
                (("1" (expand "injective?")
                  (("1" (skosimp)
                    (("1" (typepred "x1!1")
                      (("1" (typepred "x2!1")
                        (("1" (expand "remove")
                          (("1" (expand "member")
                            (("1" (flatten)
                              (("1"
                                (inst - "x1!1" "x2!1")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skosimp)
                  (("2" (typepred "x!1")
                    (("2" (expand "remove")
                      (("2" (expand "member") (("2" (flatten) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (inst + "lambda (x:(remove(t!1, X!1))): f!1(x)")
                (("1" (expand "injective?")
                  (("1" (skosimp)
                    (("1" (typepred "x1!1")
                      (("1" (typepred "x2!1")
                        (("1" (expand "remove")
                          (("1" (expand "member")
                            (("1" (flatten)
                              (("1"
                                (inst - "x1!1" "x2!1")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skosimp)
                  (("2" (typepred "x!1")
                    (("2" (expand "remove")
                      (("2" (expand "member") (("2" (flatten) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_countable const-decl "bool" countability nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countability_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (f!1 skolem-const-decl "(injective?[(X!1), nat])" countability_aux
     nil)
    (X!1 skolem-const-decl "(is_countable)" countability_aux nil)
    (t!1 skolem-const-decl "T" countability_aux nil)
    (remove const-decl "set" sets 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))
   shostak))
(countable_intersection1 0
  (countable_intersection1-1 nil 3406352737
   ("" (skosimp)
    ((""
      (lemma "countable_subset"
       ("S" "intersection(X!1, S!1)" "Count" "X!1"))
      (("" (rewrite "intersection_subset1") nil nil)) nil))
    nil)
   ((T formal-type-decl nil countability_aux nil)
    (countable_set nonempty-type-eq-decl nil countability nil)
    (is_countable const-decl "bool" countability nil)
    (intersection const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (countable_subset formula-decl nil countability nil)
    (intersection_subset1 formula-decl nil sets_lemmas nil))
   shostak))
(countable_intersection2 0
  (countable_intersection2-1 nil 3406352606
   ("" (skosimp)
    (("" (lemma "countable_intersection1" ("S" "S!1" "X" "X!1"))
      (("" (rewrite "intersection_commutative") nil nil)) nil))
    nil)
   ((is_countable const-decl "bool" countability nil)
    (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 countability_aux nil)
    (countable_intersection1 formula-decl nil countability_aux nil)
    (intersection_commutative formula-decl nil sets_lemmas nil)
    (countable_intersection2 application-judgement "countable_set[T]"
     countability_aux nil))
   shostak))
(countable_difference 0
  (countable_difference-1 nil 3406352658
   ("" (skosimp)
    (("" (lemma "difference_subset" ("a" "X!1" "b" "S!1"))
      ((""
        (lemma "countable_subset"
         ("S" "difference(X!1, S!1)" "A" "X!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((T formal-type-decl nil countability_aux nil)
    (is_countable const-decl "bool" countability nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (difference_subset formula-decl nil sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (countable_difference application-judgement "countable_set[T]"
     countability_aux nil))
   shostak)))

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