| products/sources/formale sprachen/PVS/metric_space/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: heine_borel_scaf.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(heine_borel_scaf
(heine_borel_aux 0 (heine_borel_aux-1 nil 3397472073 ("" (skosimp) (("" (name "S" "{z:real | a!1 <= z & z <= b!1 & EXISTS U: subset?(U, C!1) AND is_finite(U) & subset?({x | a!1 <= x AND x <= z}, Union(U))}") (("" (hide -1) (("" (case "S(a!1)") (("1" (typepred "sup(S)") (("1" (expand "least_upper_bound") (("1" (flatten) (("1" (name-replace "M" "sup(S)") (("1" (case "a!1<=M&M<=b!1") (("1" (flatten) (("1" (case "exists (a:set[real]): C!1(a) & a(M)") (("1" (skosimp) (("1" (copy -9) (("1" (expand "every" -1) (("1" (inst - "a!2") (("1" (expand "open?" -1) (("1" (expand "member") (("1" (expand "metric_induced_topology" -1) (("1" (expand "metric_open?") (("1" (inst - "M") (("1" (assert) (("1" (skosimp) (("1" (expand "ball") (("1" (expand "subset?" -1) (("1" (expand "member") (("1" (case "forall (r:posreal): r < r!1 => subset?({z:real| M-r<=z&z<=M+r},a!2)") (("1" (hide -2) (("1" (case "FORALL (r: posreal): r < r!1 => (EXISTS x: S(x) & M - r < x)") (("1" (case "FORALL (r: posreal): r < r!1 => EXISTS U: subset?(U, C!1) AND U(a!2) & is_finite(U) AND subset?({x | a!1 <= x AND x <= M+r}, Union(U))") (("1" (case "S(M)") (("1" (case "forall (r:posreal): r (("1" (expand "<=" -9) (("1" (split -9) (("1" (name "R" "min(b!1-M,r!1/2)") (("1" (inst - "R") (("1" (split -3) (("1" (inst - "R") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide-all-but (-3 1)) (("2" (expand "S") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "<=" -9) (("2" (split -9) (("1" (case "M+r!2<=b!1") (("1" (inst -5 "r!2") (("1" (assert) (("1" (skosimp) (("1" (expand "upper_bound" -14) (("1" (inst -14 "M+r!2") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "S" 1) (("2" (inst + "U!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "S" 1) (("2" (inst - "r!1/2") (("2" (assert) (("2" (skosimp) (("2" (inst + "U!1") (("2" (assert) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (inst -6 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "r!2") (("2" (inst - "r!2") (("2" (assert) (("2" (skosimp) (("2" (expand "S" -2) (("2" (assert) (("2" (flatten) (("2" (skosimp) (("2" (inst + "add(a!2,U!1)") (("2" (rewrite "finite_add[set[real]]") (("2" (split 1) (("1" (expand "add") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) (("1" (split -1) (("1" (assert) nil nil) ("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "add") (("2" (propax) nil nil)) nil) ("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp) (("3" (expand "add") (("3" (expand "member") (("3" (expand "Union") (("3" (case "M-r!2<=x!2") (("1" (inst -11 "x!2") (("1" (assert) (("1" (inst + "a!2") nil nil)) nil)) nil) ("2" (inst -8 "x!2") (("2" (assert) (("2" (skosimp) (("2" (inst + "a!3") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "r!2") (("2" (assert) (("2" (expand "subset?") (("2" (expand "member") (("2" (inst -8 "M-r!2") (("2" (assert) (("2" (expand "upper_bound" 2) (("2" (skosimp) (("2" (inst + "z!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -3 1)) (("2" (skosimp) (("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "open_cover?") (("2" (flatten) (("2" (expand "cover?") (("2" (expand "subset?") (("2" (expand "member") (("2" (inst -9 "M") (("2" (assert) (("2" (expand "Union") (("2" (skosimp) (("2" (inst + "a!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "upper_bound") (("1" (inst - "a!1") nil nil)) nil) ("2" (inst - "b!1") (("2" (split -2) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (expand "upper_bound") (("3" (skosimp) (("3" (typepred "z!1") (("3" (expand "S" -1) (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -4 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "above_bounded") (("2" (inst + "b!1") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (expand "S" -1) (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "S") (("2" (assert) (("2" (expand "open_cover?") (("2" (flatten) (("2" (expand "cover?") (("2" (expand "subset?" -4) (("2" (expand "member") (("2" (inst -4 "a!1") (("2" (assert) (("2" (expand "Union" -4) (("2" (skosimp) (("2" (inst + "singleton[set[real]](a!2)") (("2" (split) (("1" (expand "subset?") (("1" (expand "singleton") (("1" (expand "member") (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_singleton[set[real]]" ("x" "a!2")) (("2" (propax) nil nil)) nil) ("3" (expand "subset?") (("3" (expand "member") (("3" (expand "singleton") (("3" (expand "Union") (("3" (skosimp*) (("3" (inst + "a!2") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Union const-decl "set" sets nil) (is_finite const-decl "bool" finite_sets nil) (subset? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (empty? const-decl "bool" sets nil) (a!1 skolem-const-decl "real" heine_borel_scaf nil) (open_cover? const-decl "bool" topology_prelim "topology/") (cover? const-decl "bool" topology_prelim "topology/") (every const-decl "bool" sets nil) (open? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (real_plus_real_is_real application-judgement "real" reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (add const-decl "(nonempty?)" sets nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (finite_add formula-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (upper_bound const-decl "bool" bound_defs "reals/") (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (r!2 skolem-const-decl "posreal" heine_borel_scaf nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (R skolem-const-decl "{p: real | p <= b!1 - M AND p <= r!1 / 2}" heine_borel_scaf nil) (r!1 skolem-const-decl "posreal" heine_borel_scaf nil) (M skolem-const-decl "{x | least_upper_bound(<=)(x, S)}" heine_borel_scaf nil) (S skolem-const-decl "[real -> boolean]" heine_borel_scaf nil) (b!1 skolem-const-decl "real" heine_borel_scaf nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (ball const-decl "set[T]" metric_space_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (metric_space_is_hausdorff name-judgement "hausdorff" real_topology nil) (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology nil) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology nil) (metric_open? const-decl "bool" metric_space_def nil) (member const-decl "bool" sets nil) (a!2 skolem-const-decl "set[real]" heine_borel_scaf nil) (C!1 skolem-const-decl "setofsets[real]" heine_borel_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (nonempty? const-decl "bool" sets nil) (above_bounded const-decl "bool" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (finite_singleton judgement-tcc nil finite_sets nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil)) shostak))) ¤ Dauer der Verarbeitung: 0.28 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 |
