| products/sources/formale sprachen/PVS/sets_aux/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: countable_image.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(countable_image
(countable_image 0 (countable_image-2 nil 3322415765 ("" (skosimp) (("" (expand "is_countable") (("" (skolem-typepred) (("" (case "surjective?[(S!1), (image(f!1)(S!1))](f!1)") (("1" (assert) (("1" (lemma "surjective_inverse_exists[(S!1), (image(f!1)(S!1))]" ("f" "restrict[D, ((S!1)), R](f!1)")) (("1" (skolem!) (("1" (inst + "f!2 o g!1") (("1" (assert) (("1" (lemma "inj_inv_alt[(S!1), (image(f!1)(S!1))]" ("f" "restrict[D, ((S!1)), R](f!1)" "g" "g!1")) (("1" (expand* "injective?" "o") (("1" (skosimp) (("1" (inst - "x1!1" "x2!1") (("1" (inst - "g!1(x1!1)" "g!1(x2!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "restrict" "image" "image") (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (expand* "restrict" "surjective?") (("2" (skolem-typepred) (("2" (expand* "image" "image") (("2" (skolem!) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand* "image" "image") (("3" (skolem!) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_countable const-decl "bool" countability nil) (R formal-type-decl nil countable_image nil) (image const-decl "set[R]" function_image nil) (surjective? const-decl "bool" functions nil) (restrict const-decl "R" restrict nil) (surjective_inverse_exists formula-decl nil function_inverse_def nil) (O const-decl "T3" function_props nil) (g!1 skolem-const-decl "[(image(f!1)(S!1)) -> (S!1)]" countable_image nil) (f!2 skolem-const-decl "(injective?[(S!1), nat])" countable_image nil) (S!1 skolem-const-decl "set[D]" countable_image nil) (f!1 skolem-const-decl "[D -> R]" countable_image nil) (inj_inv_alt formula-decl nil function_inverse_def nil) (inverse? const-decl "bool" function_inverse_def nil) (image const-decl "set[R]" function_image 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) (set type-eq-decl nil sets nil) (D formal-type-decl nil countable_image nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil) (countable_image-1 nil 3313909571 ("" (skosimp*) (("" (case "is_finite(S!1)") (("1" (lemma "image_finite" ("X" "S!1" "f" "f!1")) (("1" (assert) (("1" (hide -2 -3) (("1" (expand "is_finite") (("1" (skosimp) (("1" (expand "is_countable") (("1" (inst + "f!2") (("1" (expand "injective?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "countable_card" -1) (("2" (split) (("1" (propax) nil nil) ("2" (expand "is_countably_infinite") (("2" (skosimp) (("2" (typepred "f!2") (("2" (expand "is_countable") (("2" (case "surjective?[(S!1),(image(f!1)(S!1))](f!1)") (("1" (hide 1) (("1" (lemma "surjective_inverse_exists[(S!1), (image(f!1)(S!1))]" ("f" "restrict[D, ((S!1)), R](f!1)")) (("1" (skosimp*) (("1" (inst + "f!2 o g!1") (("1" (lemma "inj_inv_alt[(S!1), (image(f!1)(S!1))]" ("f" "restrict[D, ((S!1)), R](f!1)" "g" "g!1")) (("1" (expand "bijective?") (("1" (flatten) (("1" (hide-all-but (-1 -4 1)) (("1" (expand "o") (("1" (expand "injective?") (("1" (skosimp*) (("1" (inst -3 "g!1(x1!1)" "g!1(x2!1)") (("1" (assert) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (expand "restrict") (("2" (expand "image") (("2" (expand "image") (("2" (inst + "x1!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "restrict") (("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (expand "image") (("2" (expand "image") (("2" (skosimp*) (("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "image") (("3" (expand "image") (("3" (skosimp) (("3" (inst + "x1!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (is_countable const-decl "bool" countability nil) (is_countably_infinite const-decl "bool" countability nil)) shostak))) ¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
