Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: countability.prf Sprache: Lisp

Original von: PVS^©

(countability
(countable_set_TCC1 0
  (countable_set_TCC1-1 nil 3316972170
   ("" (expand "is_countable")
    (("" (inst + "LAMBDA (t: (emptyset[T])): 0")
      (("" (subtype-tcc) nil nil)) nil))
    nil)
   ((T formal-type-decl nil countability 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)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (is_countable const-decl "bool" countability nil))
   nil))
(countably_infinite_countable 0
  (countably_infinite_countable-1 nil 3316972170
   ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil countability nil)
    (set type-eq-decl nil sets nil)
    (is_countably_infinite const-decl "bool" countability nil)
    (countably_infinite_set type-eq-decl nil 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)
    (bijective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (is_countable const-decl "bool" countability nil))
   nil))
(countably_infinite_subset 0
  (countably_infinite_subset-1 nil 3316972336
   ("" (skosimp :preds? t)
    (("" (case "FORALL (x: (Inf!1)): CountInf!1(x)")
      (("1" (expand "is_countably_infinite")
        (("1" (skolem-typepred)
          (("1" (lemma "bijective_image[(Inf!1), nat]")
            (("1" (inst - "restrict[(CountInf!1), (Inf!1), nat](f!1)")
              (("1"
                (case "enumerable?(image(restrict[(CountInf!1), (Inf!1), nat](f!1), fullset[(Inf!1)]))")
                (("1" (use "enum_bijective")
                  (("1"
                    (use "bijective_inverse_exists[nat, (image(restrict[(CountInf!1), (Inf!1), nat](f!1), fullset[(Inf!1)]))]")
                    (("1" (expand "exists1")
                      (("1" (skosimp*)
                        (("1"
                          (lemma
                           "bij_inv_is_bij_alt[nat, (image(restrict[(CountInf!1), (Inf!1), nat](f!1), fullset[(Inf!1)]))]")
                          (("1"
                            (inst -
                             "enum(image(restrict[(CountInf!1), (Inf!1), nat](f!1), fullset[(Inf!1)]))"
                             "x!1")
                            (("1"
                              (lemma
                               "composition_bijective[(Inf!1), (image(restrict[(CountInf!1), (Inf!1), nat](f!1), fullset[(Inf!1)])), nat]")
                              (("1"
                                (inst
                                 -
                                 "restrict[(CountInf!1), (Inf!1), nat](f!1)"
                                 "x!1")
                                (("1"
                                  (inst
                                   +
                                   "x!1 o restrict[(CountInf!1), (Inf!1), nat](f!1)")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2"
                  (expand* "image" "enumerable?" "bounded_below?"
                   "lower_bound?" "restrict")
                  (("2" (split)
                    (("1" (inst + "0")
                      (("1" (skolem!) (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (expand "is_finite")
                      (("2" (skolem!)
                        (("2"
                          (inst + "N!1"
                           "LAMBDA (i: (Inf!1)): f!2(f!1(i))")
                          (("1" (expand* "bijective?" "injective?")
                            (("1" (skosimp* t)
                              (("1"
                                (inst - "f!1(x1!1)" "f!1(x2!1)")
                                (("1"
                                  (inst - "x1!1" "x2!1")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skolem!)
                            (("2" (inst + "i!1")
                              (("2"
                                (expand "fullset")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand* "subset?" "member")
        (("2" (skolem-typepred)
          (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    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)
    (restrict_of_inj_is_inj application-judgement "(injective?[S, R])"
     restrict nil)
    (Inf!1 skolem-const-decl "infinite_set[T]" countability nil)
    (CountInf!1 skolem-const-decl "countably_infinite_set" countability
     nil)
    (injective? const-decl "bool" functions nil)
    (restrict const-decl "R" restrict nil)
    (lower_bound? const-decl "bool" bounded_orders "orders/")
    (bounded_below? const-decl "bool" bounded_orders "orders/")
    (= const-decl "[T, T -> boolean]" equalities 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)
    (i!1 skolem-const-decl "(Inf!1)" countability nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (enum_bijective formula-decl nil integer_enumerations "orders/")
    (f!1 skolem-const-decl "(bijective?[(CountInf!1), nat])"
     countability nil)
    (exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (O const-decl "T3" function_props nil)
    (x!1 skolem-const-decl
     "[(image(restrict[(CountInf!1), (Inf!1), nat](f!1), fullset[(Inf!1)])) ->
   nat]" countability nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (enum_member application-judgement "(S)" countability nil)
    (enum_strictly_monotone application-judgement
     "(strictly_monotone?)" countability nil)
    (enum def-decl "T" integer_enumerations "orders/")
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (fullset const-decl "set" sets nil)
    (image const-decl "set[R]" function_image nil)
    (enumerable? const-decl "bool" integer_enumerations "orders/")
    (bijective_image formula-decl nil function_image_aux nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil countability nil)
    (set type-eq-decl nil sets nil)
    (is_countably_infinite const-decl "bool" countability nil)
    (countably_infinite_set type-eq-decl nil countability nil)
    (is_finite const-decl "bool" finite_sets nil)
    (infinite_set type-eq-decl nil infinite_sets_def nil))
   shostak))
(countable_subset 0
  (countable_subset-1 nil 3316975555
   ("" (skosimp :preds? t)
    (("" (expand* "is_countable" "subset?" "member")
      (("" (skolem-typepred)
        (("" (inst + "LAMBDA (x: (S!1)): f!1(x)")
          (("1" (grind) nil nil) ("2" (reduce) nil nil)) nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (S!1 skolem-const-decl "set[T]" countability nil)
    (Count!1 skolem-const-decl "countable_set" countability nil)
    (f!1 skolem-const-decl "(injective?[(Count!1), nat])" 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)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil countability nil)
    (set type-eq-decl nil sets nil)
    (is_countable const-decl "bool" countability nil)
    (countable_set nonempty-type-eq-decl nil countability nil))
   shostak))
(countable_type_is_countably_infinite 0
  (countable_type_is_countably_infinite-1 nil 3318686144
   ("" (expand* "is_countably_infinite_type" "is_countable_type")
    (("" (skosimp* t)
      (("" (expand "bijective?")
        (("" (flatten) (("" (inst?) 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)
    (T formal-type-decl nil countability nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (is_countably_infinite_type const-decl "bool" countability nil)
    (is_countable_type const-decl "bool" countability nil))
   shostak))
(countable_full 0
  (countable_full-1 nil 3318686177 ("" (grind) nil nil)
   ((f!1 skolem-const-decl "(injective?[(fullset[T]), nat])"
     countability nil)
    (is_countable const-decl "bool" countability nil)
    (is_countable_type const-decl "bool" countability nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (f!1 skolem-const-decl "(injective?[T, nat])" countability nil)
    (set type-eq-decl nil sets 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)
    (T formal-type-decl nil countability nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (fullset const-decl "set" sets nil))
   shostak))
(countably_infinite_full 0
  (countably_infinite_full-1 nil 3318686258 ("" (grind) nil nil)
   ((f!1 skolem-const-decl "(bijective?[(fullset[T]), nat])"
     countability nil)
    (is_countably_infinite const-decl "bool" countability nil)
    (is_countably_infinite_type const-decl "bool" countability nil)
    (set type-eq-decl nil sets nil)
    (f!1 skolem-const-decl "(bijective?[T, nat])" countability nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (T formal-type-decl nil countability nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (fullset const-decl "set" sets nil))
   shostak))
(uncountable_full 0
  (uncountable_full-1 nil 3318686265
   ("" (lemma "countable_full") (("" (prop) nil nil)) nil)
   ((countable_full formula-decl nil countability nil)) shostak))
(countable_type_set 0
  (countable_type_set-1 nil 3318686284
   ("" (expand* "is_countable_type" "is_countable")
    (("" (skosimp* t)
      (("" (inst + "LAMBDA (t: (S!1)): f!1(t)") (("" (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)
    (T formal-type-decl nil countability nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (S!1 skolem-const-decl "set[T]" countability nil)
    (f!1 skolem-const-decl "(injective?[T, nat])" countability nil)
    (set type-eq-decl nil sets nil)
    (is_countable_type const-decl "bool" countability nil)
    (is_countable const-decl "bool" countability nil))
   shostak))
(countably_infinite_type_set 0
  (countably_infinite_type_set-1 nil 3318686340
   ("" (expand* "is_countably_infinite_type" "is_countable")
    (("" (skosimp* t)
      (("" (inst + "LAMBDA (t: (S!1)): f!1(t)") (("" (grind) 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)
    (T formal-type-decl nil countability nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil)
    (S!1 skolem-const-decl "set[T]" countability nil)
    (f!1 skolem-const-decl "(bijective?[T, nat])" countability nil)
    (set type-eq-decl nil sets nil)
    (injective? const-decl "bool" functions nil)
    (is_countably_infinite_type const-decl "bool" countability nil)
    (is_countable const-decl "bool" countability nil))
   shostak))
(uncountably_infinite_type_set 0
  (uncountably_infinite_type_set-1 nil 3318686379
   ("" (lemma "countable_type_set")
    (("" (prop) (("" (skolem!) (("" (inst?) nil nil)) nil)) nil)) 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 nil)
    (countable_type_set formula-decl nil countability nil))
   shostak))
(countable_complement 0
  (countable_complement-1 nil 3318686421
   ("" (skosimp*)
    (("" (forward-chain "countable_type_set") (("" (inst?) nil nil))
      nil))
    nil)
   ((countable_type_set formula-decl nil countability nil)
    (T formal-type-decl nil countability nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (complement const-decl "set" sets nil))
   shostak))
(countably_infinite_complement 0
  (countably_infinite_complement-1 nil 3318686452
   ("" (skosimp*)
    (("" (forward-chain "countably_infinite_type_set")
      (("" (inst?) nil nil)) nil))
    nil)
   ((countably_infinite_type_set formula-decl nil countability nil)
    (T formal-type-decl nil countability nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (complement const-decl "set" sets 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.