| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle card_power_set.prf Sprache: Lisp |
|||||||||
|
(card_power_set
(card_power 0 (card_power-1 nil 3316968399 ("" (skolem!) (("" (rewrite "card_lt_surj") (("" (split) (("1" (inst + "emptyset[T]") (("1" (grind) nil nil)) nil) ("2" (skolem!) (("2" (expand "surjective?") (("2" (inst - "{t: T | S!1(t) AND NOT f!1(t)(t)}") (("1" (skolem!) (("1" (decompose-equality) (("1" (inst - "x!1") (("1" (iff) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((card_lt_surj formula-decl nil card_comp_set_props nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (powerset const-decl "setofsets" sets nil) (T formal-type-decl nil card_power_set nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (f!1 skolem-const-decl "[(S!1) -> (powerset(S!1))]" card_power_set nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (surjective? const-decl "bool" functions nil) (nonempty_powerset application-judgement "(nonempty?[set[T]])" sets_lemmas nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (S!1 skolem-const-decl "set[T]" card_power_set nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil)) shostak))) ¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28