Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: infinite_sets.prf Sprache: Lisp

Original von: PVS^©

(infinite_sets
(infinite_add_card 0
  (infinite_add_card-1 nil 3317054230
   ("" (skolem!)
    (("" (rewrite "add_as_union")
      (("" (use "infinite_countable_union") nil nil)) nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite const-decl "bool" finite_sets nil)
    (infinite_set type-eq-decl nil infinite_sets_def nil)
    (T formal-type-decl nil infinite_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" infinite_sets nil)
    (infinite_union_left application-judgement "infinite_set[T]"
     infinite_sets nil)
    (infinite_countable_union formula-decl nil countable_props nil)
    (is_countable const-decl "bool" countability nil)
    (countable_set nonempty-type-eq-decl nil countability nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil))
   shostak))
(infinite_remove_card 0
  (infinite_remove_card-1 nil 3317054261
   ("" (skolem!)
    (("" (case "member(t!1, Inf!1)")
      (("1" (forward-chain "add_remove_member[T]")
        (("1" (use "infinite_add_card")
          (("1" (rewrite "card_eq_symmetric[T, T]")
            (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (forward-chain "member_remove[T]")
        (("2" (lemma "card_eq_is_reflexive")
          (("2" (expand "reflexive?")
            (("2" (inst - "Inf!1") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((infinite_set type-eq-decl nil infinite_sets_def nil)
    (is_finite const-decl "bool" finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member 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 infinite_sets nil)
    (infinite_add_card formula-decl nil infinite_sets nil)
    (remove const-decl "set" sets nil)
    (infinite_remove application-judgement "infinite_set[T]"
     infinite_sets nil)
    (card_eq_is_equivalence name-judgement "equivalence[set[T]]"
     infinite_sets nil)
    (infinite_add application-judgement "infinite_set[T]" infinite_sets
     nil)
    (card_eq_symmetric formula-decl nil card_comp_set_props nil)
    (nonempty? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (add_remove_member formula-decl nil sets_lemmas nil)
    (card_eq_is_reflexive judgement-tcc nil card_single nil)
    (reflexive? const-decl "bool" relations nil)
    (member_remove formula-decl nil sets_lemmas nil))
   shostak))
(finite_infinite_lt 0
  (finite_infinite_lt-1 nil 3317054357
   ("" (skolem!)
    (("" (prop)
      (("1" (inst?)
        (("1" (lemma "card_lt_is_irreflexive")
          (("1" (expand "irreflexive?") (("1" (inst?) nil nil)) nil))
          nil))
        nil)
       ("2" (skolem-typepred)
        (("2" (expand* "card_lt" "is_finite")
          (("2" (skosimp*)
            (("2"
              (use "composition_injective[(S!1), (Fin!1), below[N!1]]")
              (("2" (inst + "N!1" "f!1 o f!2") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((card_lt_is_irreflexive judgement-tcc nil card_single nil)
    (irreflexive? const-decl "bool" relations nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (T formal-type-decl nil infinite_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (S!1 skolem-const-decl "set[T]" infinite_sets nil)
    (card_lt const-decl "bool" card_comp_set nil)
    (composition_injective judgement-tcc nil function_props 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)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (f!2 skolem-const-decl "[(S!1) -> (Fin!1)]" infinite_sets nil)
    (injective? const-decl "bool" functions nil)
    (Fin!1 skolem-const-decl "finite_set[T]" infinite_sets nil)
    (f!1 skolem-const-decl "[(Fin!1) -> below[N!1]]" infinite_sets nil)
    (N!1 skolem-const-decl "nat" infinite_sets nil)
    (O const-decl "T3" function_props nil)
    (NOT const-decl "[bool -> bool]" booleans 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.