| products/Sources/formale Sprachen/PVS/sets_aux/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: countable_setofsets.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(countable_setofsets
(countable_union1 0 (countable_union1-1 nil 3317055771 ("" (expand* "is_countable" "every") (("" (skosimp* t) (("" (lemma "countable_nat_tuple") (("" (case "EXISTS (f: [(Union(S!1)) -> [nat, nat]]): injective?(f)") (("1" (skosimp*) (("1" (expand "bijective?") (("1" (flatten) (("1" (use "composition_injective[(Union(S!1)), [nat, nat], nat]") (("1" (inst? +) nil nil)) nil)) nil)) nil)) nil) ("2" (case "EXISTS (f: [R: (S!1) -> (injective?[(R), nat])]): TRUE") (("1" (skosimp* t) (("1" (inst + "LAMBDA (t: (Union(S!1))): (f!1(choose({R: (S!1) | R(t)})), f!2(choose({R: (S!1) (("1" (expand "injective?") (("1" (skosimp :preds? t) (("1" (inst - "choose({R: (S!1) | R(x1!1)})" "choose({R: (S!1) | R(x2!1)})") (("1" (assert) (("1" (typepred "f!2(choose({R: (S!1) | R(x1!1)}))") (("1" (expand "injective?") (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil) ("2" (expand* "Union" "nonempty?" "empty?" "member") (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (expand* "Union" "nonempty?" "empty?" "member") (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil) ("3" (expand* "Union" "nonempty?" "empty?" "member") (("3" (skolem!) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (assert) nil nil)) nil) ("3" (skolem-typepred) (("3" (expand* "Union" "nonempty?" "empty?" "member") (("3" (skolem!) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "LAMBDA (R: (S!1)): choose({f: [(R) -> nat] | injective?(f)})") (("2" (skolem!) (("2" (inst - "R!1") (("2" (skosimp* t) (("2" (expand* "nonempty?" "empty?" "member") (("2" (inst - "f!3") nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil countable_setofsets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (set type-eq-decl nil sets nil) (Union const-decl "set" sets nil) (bijective? const-decl "bool" functions nil) (composition_injective judgement-tcc nil function_props nil) (f!2 skolem-const-decl "[(Union(S!1)) -> [nat, nat]]" countable_setofsets nil) (S!1 skolem-const-decl "setofsets[T]" countable_setofsets nil) (f!3 skolem-const-decl "[[nat, nat] -> nat]" countable_setofsets nil) (O const-decl "T3" function_props nil) (x1!1 skolem-const-decl "(Union(S!1))" countable_setofsets nil) (x2!1 skolem-const-decl "(Union(S!1))" countable_setofsets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (countable_nat_tuple formula-decl nil countable_set nil) (is_countable const-decl "bool" countability nil) (every const-decl "bool" sets nil)) shostak)) (countable_union2 0 (countable_union2-1 nil 3317056043 ("" (expand* "is_countable" "every") (("" (skosimp* t) (("" (inst + "LAMBDA (t: (x!1)): f!1(t)") (("1" (grind) nil nil) ("2" (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) (Union const-decl "set" sets nil) (set type-eq-decl nil sets nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil countable_setofsets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (f!1 skolem-const-decl "(injective?[(Union(S!1)), nat])" countable_setofsets nil) (x!1 skolem-const-decl "(S!1)" countable_setofsets nil) (S!1 skolem-const-decl "setofsets[T]" countable_setofsets nil) (is_countable const-decl "bool" countability nil) (every const-decl "bool" sets nil)) shostak)) (countable_intersection 0 (countable_intersection-1 nil 3317056085 ("" (expand* "nonempty?" "empty?" "member" "every" "is_countable") (("" (skosimp*) (("" (inst - "x!1") (("" (skolem-typepred) (("" (inst + "LAMBDA (t: (Intersection(S!1))): f!1(t)") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans 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) (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (f!1 skolem-const-decl "(injective?[(x!1), nat])" countable_setofsets nil) (set type-eq-decl nil sets nil) (Intersection const-decl "set" sets nil) (T formal-type-decl nil countable_setofsets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (S!1 skolem-const-decl "setofsets[T]" countable_setofsets nil) (x!1 skolem-const-decl "setof[T]" countable_setofsets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (is_countable const-decl "bool" countability nil) (every const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) shostak)) (countable_finite_subsets 0 (countable_finite_subsets-1 nil 3317055726 ("" (skolem-typepred) (("" (expand "is_countable") (("" (lemma "countable_family_nat") (("" (skosimp* t) (("" (inst + "LAMBDA (Q: (finite_subsets(S!1))): f!1(image(f!2, Q))") (("" (expand* "bijective?" "injective?" "surjective?") (("" (skosimp :preds? t) (("" (inst -7 "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](x1!1))" "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](x2!1))") (("" (assert) (("" (decompose-equality -7) (("" (expand "image" -1) (("" (apply-extensionality :hide? t) (("" (expand* "finite_subsets" "subset?" "member") (("" (iff) (("" (prop) (("1" (inst -4 "x!1") (("1" (assert) (("1" (inst - "f!2(x!1)") (("1" (iff) (("1" (prop) (("1" (skosimp* t) (("1" (expand "restrict") (("1" (inst - "x!1" "x!3") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst 2 "x!1") (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -6 "x!1") (("2" (assert) (("2" (inst - "f!2(x!1)") (("2" (iff) (("2" (prop) (("1" (skosimp* t) (("1" (expand "restrict") (("1" (inst - "x!1" "x!2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "x!1") (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (= const-decl "[T, T -> boolean]" equalities nil) (x2!1 skolem-const-decl "(finite_subsets(S!1))" countable_setofsets nil) (x!1 skolem-const-decl "T" countable_setofsets nil) (x1!1 skolem-const-decl "(finite_subsets(S!1))" countable_setofsets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (S!1 skolem-const-decl "countable_set[T]" countable_setofsets nil) (f!1 skolem-const-decl "[finite_set[nat] -> nat]" countable_setofsets nil) (f!2 skolem-const-decl "(injective?[(S!1), nat])" countable_setofsets nil) (restrict const-decl "R" restrict nil) (image const-decl "set[R]" function_image nil) (finite_subsets const-decl "set[finite_set[T]]" countable_setofsets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (finite_image application-judgement "finite_set[R]" function_image_aux nil) (countable_family_nat formula-decl nil countable_set nil) (countable_set nonempty-type-eq-decl nil countability nil) (is_countable const-decl "bool" countability nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil countable_setofsets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (countably_infinite_finite_subsets 0 (countably_infinite_finite_subsets-1 nil 3317055726 ("" (skolem-typepred) (("" (expand "is_countably_infinite") (("" (lemma "countable_family_nat") (("" (skosimp* t) (("" (inst + "LAMBDA (Q: (finite_subsets(S!1))): f!1(image(f!2, Q))") (("" (expand* "bijective?" "injective?" "surjective?") (("" (prop) (("1" (skosimp :preds? t) (("1" (inst -8 "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](x1!1))" "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](x2!1))") (("1" (assert) (("1" (decompose-equality -8) (("1" (expand "image" -1) (("1" (apply-extensionality :hide? t) (("1" (iff) (("1" (prop) (("1" (expand* "finite_subsets" "subset?" "member") (("1" (inst -4 "x!1") (("1" (assert) (("1" (inst - "f!2(x!1)") (("1" (iff) (("1" (prop) (("1" (skosimp* t) (("1" (expand "restrict") (("1" (inst - "x!1" "x!3") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst 2 "x!1") (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "finite_subsets" "subset?" "member") (("2" (inst -6 "x!1") (("2" (assert) (("2" (inst - "f!2(x!1)") (("2" (iff) (("2" (prop) (("1" (skosimp* t) (("1" (expand "restrict") (("1" (inst - "x!1" "x!2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "x!1") (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (inst -4 "y!1") (("2" (skolem!) (("2" (inst + "{t: (S!1) | x!1(f!2(t))}") (("1" (case "image[(S!1), nat](f!2, restrict[T, (S!1), boolean](extend[T, (S!1), bool, (("1" (assert) nil nil) ("2" (delete 2) (("2" (expand* "restrict" "extend" "image") (("2" (apply-extensionality :hide? t) (("2" (iff) (("2" (smash) (("2" (inst - "x!2") (("2" (skolem!) (("2" (assert) (("2" (inst + "x!3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (typepred "x!1") (("1" (expand "is_finite") (("1" (skolem!) (("1" (inst + "N!1" "LAMBDA (w: (extend[T, (S!1), bool, FALSE]({t: (S!1) | x!1(f!2(t))}))): f!3(f!2( (("1" (expand "injective?") (("1" (skosimp :preds? t) (("1" (expand "extend") (("1" (prop) (("1" (inst - "f!2(x1!1)" "f!2(x2!1)") (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand "extend") (("2" (prop) nil nil)) nil)) nil) ("3" (skolem-typepred) (("3" (expand "extend") (("3" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions 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) (x!1 skolem-const-decl "finite_set[nat]" countable_setofsets nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (countable_finite_subsets application-judgement "countable_set[finite_set[T]]" countable_setofsets nil) (x2!1 skolem-const-decl "(finite_subsets(S!1))" countable_setofsets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (x1!1 skolem-const-decl "(finite_subsets(S!1))" countable_setofsets nil) (x!1 skolem-const-decl "T" countable_setofsets nil) (= const-decl "[T, T -> boolean]" equalities nil) (S!1 skolem-const-decl "countably_infinite_set[T]" countable_setofsets nil) (f!1 skolem-const-decl "[finite_set[nat] -> nat]" countable_setofsets nil) (f!2 skolem-const-decl "(bijective?[(S!1), nat])" countable_setofsets nil) (restrict const-decl "R" restrict nil) (image const-decl "set[R]" function_image nil) (finite_subsets const-decl "set[finite_set[T]]" countable_setofsets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (finite_image application-judgement "finite_set[R]" function_image_aux nil) (countable_family_nat formula-decl nil countable_set nil) (countably_infinite_set type-eq-decl nil countability nil) (is_countably_infinite const-decl "bool" countability nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil countable_setofsets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil))) ¤ Dauer der Verarbeitung: 0.23 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 |
