| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 139 kB |
|
Quelle real_metric_space.prfSprache: Lisp |
|||||||||||||||
|
(real_metric_space (real_metric_space 0 (real_metric_space-1 nil 3460456811 ("" (grind) nil nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans 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) (set type-eq-decl nil sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_dist const-decl "nnreal" real_metric_space nil) (space_zero? const-decl "bool" metric_spaces_def nil) (space_symmetric? const-decl "bool" metric_spaces_def nil) (space_triangle? const-decl "bool" metric_spaces_def nil) (metric_space? const-decl "bool" metric_spaces_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (IMP_compactness_TCC1 0 (IMP_compactness_TCC1-1 nil 3460718977 ("" (lemma "real_metric_space") (("" (inst - "fullset[real]") nil nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (real_metric_space formula-decl nil real_metric_space nil)) nil)) (compact_induction 0 (compact_induction-1 nil 3460795815 ("" (skosimp*) (("" (label "compact_first" -1) (("" (label "compact_second" -2) (("" (label "compact_final" 1) (("" (expand "compact?") (("" (skosimp*) (("" (label "tot_oc" -3) (("" (inst - "XS!1") (("" (inst - "XS!1") (("" (expand "open_cover?") (("" (prop) (("1" (label "sets_open" -4) (("1" (copy "compact_first") (("1" (hide "compact_first") (("1" (skosimp -1) (("1" (expand "finite_cover?") (("1" (prop) (("1" (label "first_ss" -1) (("1" (label "first_fin" -2) (("1" (expand "open_cover?" -3) (("1" (prop) (("1" (expand "subset?" -3) (("1" (expand "member") (("1" (label "first_is_cov" -3) (("1" (label "first_is_op" -4) (("1" (expand "Union" "first_is_cov") (("1" (copy "compact_second") (("1" (hide "compact_second") (("1" (skosimp -1) (("1" (expand "open_cover?" -3) (("1" (prop) (("1" (label "second_ss" -1) (("1" (label "second_fin" -2) (("1" (label "second_cov" -3) (("1" (label "second_op" -4) (("1" (expand "Union" "second_cov") (("1" (inst + "union[set[real]](YS!1,YS!2)") (("1" (expand "open_cover?") (("1" (expand "subset?") (("1" (expand "member") (("1" (prop) (("1" (skosimp*) (("1" (expand "union") (("1" (expand "member") (("1" (prop) (("1" (label "in_first" -1) (("1" (inst "first_ss" "x!1") (("1" (prop) nil nil)) nil)) nil) ("2" (label "in_second" -1) (("2" (inst "second_ss" "x!1") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "infinite_union[set[real]]") (("2" (label "inf_un" -1) (("2" (inst "inf_un" "YS!1" "YS!2") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (case "x!1 <= (c!1 + d!1)/2") (("1" (label "caseonx1" -1) (("1" (inst "first_is_cov" "x!1") (("1" (expand "Union") (("1" (assert) (("1" (skosimp "first_is_cov") (("1" (inst + "a!1") (("1" (expand "union") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst "second_cov" "x!1") (("2" (assert) (("2" (skosimp "second_cov") (("2" (expand "Union") (("2" (inst "compact_final" "a!1") (("2" (expand "union") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "union") (("4" (expand "member") (("4" (prop) (("1" (inst "first_ss" "C!1") (("1" (assert) (("1" (inst "sets_open" "C!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst "second_ss" "C!1") (("2" (inst "sets_open" "C!1") (("2" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst "tot_oc" "x!1") (("2" (expand "Union") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp*) (("3" (inst "tot_oc" "x!1") (("3" (expand "Union") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "subset?") (("4" (expand "member") (("4" (skosimp*) (("4" (inst "tot_oc" "x!1") (("4" (expand "Union") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (open_cover? const-decl "bool" compactness nil) (finite_cover? const-decl "bool" compactness nil) (subset? const-decl "bool" sets nil) (Union const-decl "set" sets nil) (a!1 skolem-const-decl "(YS!2)" real_metric_space nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (a!1 skolem-const-decl "(YS!1)" real_metric_space nil) (YS!2 skolem-const-decl "set[set[real]]" real_metric_space nil) (YS!1 skolem-const-decl "set[set[real]]" real_metric_space nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (infinite_union formula-decl nil infinite_sets_def nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (compact? const-decl "bool" compactness nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (seq_intv_scaf_TCC1 0 (seq_intv_scaf_TCC1-1 nil 3460814665 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans 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) (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space nil) (open_cover? const-decl "bool" compactness nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (open? const-decl "bool" metric_spaces nil) (Union const-decl "set" sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (seq_intv_scaf_TCC2 0 (seq_intv_scaf_TCC2-1 nil 3460814665 ("" (termination-tcc) nil nil) ((member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (seq_intv_scaf_TCC3 0 (seq_intv_scaf_TCC3-1 nil 3460814665 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (Union const-decl "set" sets nil) (real_dist const-decl "nnreal" real_metric_space nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (open? const-decl "bool" metric_spaces nil) (open_cover? const-decl "bool" compactness nil) (finite_cover? const-decl "bool" compactness nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (seq_intv_scaf_TCC4 0 (seq_intv_scaf_TCC4-1 nil 3460814665 ("" (termination-tcc) nil nil) ((member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (Union const-decl "set" sets nil) (real_dist const-decl "nnreal" real_metric_space nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (open? const-decl "bool" metric_spaces nil) (open_cover? const-decl "bool" compactness nil) (finite_cover? const-decl "bool" compactness nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (seq_intv_scaf_TCC5 0 (seq_intv_scaf_TCC5-1 nil 3460814665 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (int_minus_int_is_int application-judgement "int" integers nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (Union const-decl "set" sets nil) (real_dist const-decl "nnreal" real_metric_space nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (open? const-decl "bool" metric_spaces nil) (open_cover? const-decl "bool" compactness nil) (finite_cover? const-decl "bool" compactness nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (seq_intv_scaf_TCC6 0 (seq_intv_scaf_TCC6-1 nil 3460814665 ("" (termination-tcc) nil nil) ((member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (Union const-decl "set" sets nil) (real_dist const-decl "nnreal" real_metric_space nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (open? const-decl "bool" metric_spaces nil) (open_cover? const-decl "bool" compactness nil) (finite_cover? const-decl "bool" compactness nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (seq_inv_scaf_decreasing 0 (seq_inv_scaf_decreasing-1 nil 3460811042 ("" (skolem 1 ("c" "d" "YS")) (("" (skeep) (("" (split) (("1" (generalize "n" "m") (("1" (induct "m") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (expand "seq_intv_scaf" 1) (("2" (name "W" "seq_intv_scaf(c,d,YS)(j!1)") (("2" (replace -1) (("2" (hide -1) (("2" (name "P" "NOT (EXISTS (XS: set[set[real]]): subset?(XS, YS) AND open_cover?(XS, LAMBDA (x: real): W`1 <= x AND x <= (W`1 + W`2) / 2))") (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "seq_intv_scaf" -1) (("2" (name "W" "seq_intv_scaf(c,d,YS)(n)") (("2" (replace -1) (("2" (hide -1) (("2" (name "P" "NOT (EXISTS (XS: set[set[real]]): subset?(XS, YS) AND open_cover?(XS, LAMBDA (x: real): W`1 <= x AND x <= (W`1 + W`2) / 2))") (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (generalize "n" "m") (("3" (induct "m") (("1" (expand "seq_intv_scaf") (("1" (expand "^") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (name "W" "seq_intv_scaf(c,d,YS)(j!1)") (("2" (replace -1) (("2" (label "name_w" -1) (("2" (hide -1) (("2" (expand "seq_intv_scaf") (("2" (reveal "name_w") (("2" (replace "name_w") (("2" (hide "name_w") (("2" (name "P" "NOT (EXISTS (XS: set[set[real]]): subset?(XS, YS) AND finite_cover?(XS, LAMBDA (x: real): W`1 <= x AND x <= (W`1 + W`2) / 2))") (("2" (replace -1) (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_exp application-judgement "posint" exponentiation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (expt def-decl "real" exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space nil) (open_cover? const-decl "bool" compactness nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (seq_intv_scaf def-decl "[real, real]" real_metric_space nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_cover? const-decl "bool" compactness nil) (open? const-decl "bool" metric_spaces nil) (Union const-decl "set" sets nil) (is_finite const-decl "bool" finite_sets nil) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil)) shostak)) (compact_seq_induction 0 (compact_seq_induction-1 nil 3460812837 ("" (skolem 1 ("c" "d")) (("" (prop) (("" (expand "compact?") (("" (skosimp*) (("" (label "big_open_cov" -1) (("" (label "exists_fs" 1) (("" (label "smaller_sc" 2) (("" (inst "smaller_sc" "XS!1") (("" (assert) (("" (induct "n" "smaller_sc") (("1" (skosimp*) (("1" (expand "seq_intv_scaf") (("1" (inst "exists_fs" "XS!2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (name "W" "seq_intv_scaf(c,d,XS!1)(j!1)") (("2" (replace -1) (("2" (label "name_w" -1) (("2" (hide "name_w") (("2" (expand "seq_intv_scaf") (("2" (reveal "name_w") (("2" (replace "name_w") (("2" (hide "name_w") (("2" (case "(EXISTS (XS: set[set[real]]): subset?(XS, XS!1) AND finite_cover?(XS, LAMBDA (x: real): W`1 <= x AND x <= (W`1 + W`2) / 2))") (("1" (assert) (("1" (replace -1) (("1" (skosimp*) (("1" (inst + "union[set[real]](XS!2,XS!3)") (("1" (expand "subset?") (("1" (expand "member") (("1" (prop) (("1" (expand "union") (("1" (expand "member") (("1" (skolem 1 ("x")) (("1" (inst - "x") (("1" (inst - "x") (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "finite_cover?") (("2" (prop) (("1" (lemma "infinite_union[set[real]]") (("1" (inst - "XS!2" "XS!3") (("1" (prop) nil nil)) nil)) nil) ("2" (label "XS3_ss" -1) (("2" (label "XS2_ss" -6) (("2" (label "XS3_oc" -3) (("2" (label "XS2_oc" -5) (("2" (expand "open_cover?") (("2" (prop) (("1" (expand "Union") (("1" (expand "subset?") (("1" (expand "member") (("1" (assert) (("1" (skosimp*) (("1" (case "x!1 <= (W`1 + W`2)/2") (("1" (inst "XS3_oc" "x!1") (("1" (assert) (("1" (skosimp*) (("1" (inst "XS3_ss" "a!1") (("1" (inst + "a!1") (("1" (expand "union") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -9 "x!1") (("2" (assert) (("2" (skosimp*) (("2" (inst + "a!1") (("2" (expand "union") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "union") (("2" (expand "member") (("2" (inst -5 "C!1") (("2" (inst -9 "C!1") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace 1) (("2" (inst + "XS!2") (("2" (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) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets 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) (pred type-eq-decl nil defined_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space nil) (finite_cover? const-decl "bool" compactness nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (open_cover? const-decl "bool" compactness nil) (seq_intv_scaf def-decl "[real, real]" real_metric_space nil) (nat_induction formula-decl nil naturalnumbers nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union const-decl "set" sets nil) (a!1 skolem-const-decl "(XS!2)" real_metric_space nil) (XS!2 skolem-const-decl "set[set[real]]" real_metric_space nil) (XS!3 skolem-const-decl "set[set[real]]" real_metric_space nil) (a!1 skolem-const-decl "(XS!3)" real_metric_space nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (infinite_union formula-decl nil infinite_sets_def nil) (compact? const-decl "bool" compactness nil)) shostak)) (closed_intervals_compact 0 (closed_intervals_compact-1 nil 3460719116 ("" (skosimp*) (("" (lemma "compact_seq_induction") (("" (inst - "a!1" "b!1") (("" (assert) (("" (skosimp*) (("" (lemma "bolzano_weierstrass4") (("" (label "bzw" -1) (("" (label "open_cover" -2) (("" (label "induction_lem" -3) (("" (label "final_compact" 1) (("" (inst "bzw" "a!1" "b!1" "(LAMBDA (i:nat): seq_intv_scaf(a!1,b!1,YS!1)(i)`1)") (("" (prop) (("1" (skosimp*) (("1" (expand "accumulation") (("1" (expand "open_cover?") (("1" (prop) (("1" (label "subset_cover" -4) (("1" (expand "subset?") (("1" (expand "member") (("1" (inst "subset_cover" "c!1") (("1" (prop) (("1" (expand "Union") (("1" (skosimp*) (("1" (typepred "a!2") (("1" (label "tpa!2" -1) (("1" (inst "open_cover" "a!2") (("1" (assert) (("1" (expand "open?" "open_cover") (("1" (expand "interior") (("1" (replace "open_cover" "subset_cover" rl) (("1" (assert) (("1" (expand "interior_point?") (("1" (skosimp*) (("1" (lemma "axiom_of_archimedes") (("1" (inst -1 "max(10,2*(b!1-a!1)/r!1)") (("1" (skosimp*) (("1" (label "ipred" -1) (("1" (inst "bzw" "r!1/2" "i!1") (("1" (skosimp*) (("1" (inst "induction_lem" "i!2") (("1" (inst "induction_lem" "{V: set[real] | V = a!2}") (("1" (prop) (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (expand "finite_cover?") (("2" (prop) (("1" (expand "is_finite") (("1" (inst "induction_lem" "2" "(LAMBDA (K: ({V: set[real] | V = a!2})): 1)") (("1" (expand "injective?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "open_cover?") (("2" (prop) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (expand "Union") (("1" (inst "induction_lem" "a!2") (("1" (lemma "seq_inv_scaf_decreasing") (("1" (inst?) (("1" (prop) (("1" (hide -1) (("1" (hide -1) (("1" (label "size_diff" -1) (("1" (inst "subset_cover" "x!1") (("1" (prop) (("1" (expand "ball") (("1" (expand "real_dist") (("1" (name "ZA" "seq_intv_scaf(a!1, b!1, YS!1)(i!2)`1") (("1" (name "ZB" "seq_intv_scaf(a!1, b!1, YS!1)(i!2)`2") (("1" (replace -1) (("1" (replace -2) (("1" (hide -1) (("1" (hide -1) (("1" (hide ("open_cover" 2 "final_compact")) (("1" (field "size_diff") (("1" (case " i!1<2^i!2") (("1" (replace "size_diff" "ipred" rl) (("1" (expand "max") (("1" (mult-by -1 "ZB-ZA") (("1" (assert) (("1" (mult-by -1 "2/r!1") (("1" (assert) (("1" (case "10 < (2 * ((2 ^ i!2) * ZB) - 2 * ((2 ^ i!2) * ZA)) / r!1") (("1" (assert) (("1" (sub-formulas -2 "ipred") (("1" (field -1) (("1" (cancel-by -2 "i!1") (("1" (hide -4 -5) (("1" (grind :exclude ("ZA" "ZB")) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (sub-formulas -1 1) (("2" (field -1) (("2" (mult-by ipred "2*(ZB-ZA)") (("2" (hide -3) (("2" (grind :exclude ("ZA" "ZB")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "i!1 >= 10") (("1" (hide-all-but (-1 "bzw" 1)) (("1" (copy -4) (("1" (copy -2) (("1" (add-formulas -1 -2) (("1" (both-sides "-" "i!1" -1) (("1" (assert) (("1" (hide -2) (("1" (hide -2) (("1" (hide -2) (("1" (hide -3) (("1" (add-formulas -2 1) (("1" (both-sides "-" "i!1" -1) (("1" (assert) (("1" (generalize-skolem-constants) (("1" (induct "i_1") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but ("ipred" 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)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "open_cover") (("2" (skosimp*) (("2" (inst "open_cover" "a!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (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)) nil)) nil) ("2" (case "FORALL (j:nat): subset?(closed_intv(seq_intv_scaf(a!1,b!1,YS!1)(j)`1,seq_int (("1" (skosimp*) (("1" (hide-all-but (-1 1)) (("1" (inst - "i!1") (("1" (expand "subset?") (("1" (expand "member") (("1" (inst - "seq_intv_scaf(a!1,b!1,YS!1)(i!1)`1") (("1" (assert) (("1" (lemma "seq_inv_scaf_decreasing") (("1" (inst?) (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (reveal "open_cover") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (reveal "open_cover") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "j") (("1" (expand "seq_intv_scaf") (("1" (assert) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "seq_inv_scaf_decreasing") (("2" (inst?) (("1" (prop) (("1" (name "Aj1" "LAMBDA (x: real): seq_intv_scaf(a!1, b!1, YS!1)(j!1 + 1)`1 <= x AND x <= seq_intv_scaf(a!1, b!1, YS!1)(j!1 + 1)`2") (("1" (replace -1) (("1" (name "Djmin1" "LAMBDA (x: real): seq_intv_scaf(a!1, b!1, YS!1)(j!1)`1 <= x AND x <= seq_intv_scaf(a!1, b!1, YS!1)(j!1)`2") (("1" (replace -1) (("1" (name "closedint" "LAMBDA (x: real): a!1 <= x AND x <= b!1") (("1" (replace -1) (("1" (hide -1 -2 -3) (("1" (hide -1 -3) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "open_cover") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (reveal "open_cover") (("3" (propax) nil nil)) nil)) nil) ("4" (reveal "open_cover") (("4" (propax) nil nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil) ("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((compact_seq_induction formula-decl nil real_metric_space nil) (bolzano_weierstrass4 formula-decl nil convergence_sequences nil) (real_minus_real_is_real application-judgement "real" reals nil) (accumulation const-decl "bool" convergence_sequences nil) (subset? const-decl "bool" sets nil) (Union const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (open? const-decl "bool" metric_spaces nil) (interior_point? const-decl "bool" metric_spaces nil) (axiom_of_archimedes formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (i!1 skolem-const-decl "int" real_metric_space nil) (below type-eq-decl nil nat_types nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (seq_inv_scaf_decreasing formula-decl nil real_metric_space nil) (ball const-decl "set[T]" metric_spaces nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (zero_div formula-decl nil extra_tegies nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (zero_times1 formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (pos_div_gt formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (CBD_3 skolem-const-decl "int" real_metric_space nil) (- const-decl "[numfield -> numfield]" number_fields nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (minus_real_is_real application-judgement "real" reals nil) (minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_neg formula-decl nil extra_tegies nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ZB skolem-const-decl "real" real_metric_space nil) (ZA skolem-const-decl "real" real_metric_space nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (both_sides_plus_ge2 formula-decl nil real_props nil) (both_sides_minus_ge1 formula-decl nil real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (finite_cover? const-decl "bool" compactness nil) (= const-decl "[T, T -> boolean]" equalities nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (interior const-decl "set[T]" metric_spaces nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (seq_intv_scaf def-decl "[real, real]" real_metric_space nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (set type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space nil) (open_cover? const-decl "bool" compactness nil) (YS!1 skolem-const-decl "set[set[real]]" real_metric_space nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (a!1 skolem-const-decl "real" real_metric_space nil) (b!1 skolem-const-decl "{x: real | a!1 < x}" real_metric_space nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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)) shostak)))
¤ Dauer der Verarbeitung: 0.77 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26