| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/metric_space/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 837 kB |
|
Quelle metric_space.prfSprache: Lisp |
|||||||||||||||
|
(metric_space (metric_zero 0 (metric_zero-1 nil 3359138177 ("" (skosimp) (("" (typepred "d") (("" (expand "metric?") (("" (expand "metric_zero?") (("" (flatten) (("" (inst - "x!1" "y!1") nil nil)) nil)) nil)) nil)) nil)) nil) ((d formal-const-decl "metric" metric_space nil) (metric nonempty-type-eq-decl nil metric_def nil) (metric? const-decl "bool" metric_def nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (T formal-type-decl nil metric_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (metric_zero? const-decl "bool" metric_def nil)) shostak)) (metric_symmetric 0 (metric_symmetric-1 nil 3359138210 ("" (typepred "d") (("" (expand "metric?") (("" (expand "metric_symmetric?") (("" (flatten) nil nil)) nil)) nil)) nil) ((metric_symmetric? const-decl "bool" metric_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil metric_space 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) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil)) shostak)) (metric_triangle 0 (metric_triangle-1 nil 3359138244 ("" (typepred "d") (("" (expand "metric?") (("" (expand "metric_triangle?") (("" (flatten) nil nil)) nil)) nil)) nil) ((metric_triangle? const-decl "bool" metric_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil metric_space 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) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil)) shostak)) (metric_is_0 0 (metric_is_0-1 nil 3359138288 ("" (skosimp) (("" (rewrite "metric_zero") nil nil)) nil) ((metric_zero formula-decl nil metric_space nil) (T formal-type-decl nil metric_space nil)) shostak)) (ball_centre 0 (ball_centre-1 nil 3359138314 ("" (skosimp) (("" (expand "member") (("" (expand "ball") (("" (rewrite "metric_is_0") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (metric_is_0 formula-decl nil metric_space nil) (T formal-type-decl nil metric_space nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_space_def nil)) shostak)) (metric_open_ball 0 (metric_open_ball-1 nil 3359138339 ("" (skosimp) (("" (expand "metric_open?") (("" (skosimp) (("" (split) (("1" (flatten) (("1" (case-replace "x!2=x!1") (("1" (inst + "r!1") (("1" (rewrite "subset_reflexive") nil nil)) nil) ("2" (case "r!1 - d(x!1, x!2) > 0") (("1" (inst + "r!1-d(x!1,x!2)") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) (("1" (expand "ball") (("1" (lemma "metric_triangle" ("x" "x!1" "y" "x!2" "z" "x!3")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide 3) (("2" (expand "ball") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (inst - "x!2") (("2" (rewrite "ball_centre") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((metric_open? const-decl "bool" metric_space_def nil) (T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (subset_reflexive formula-decl nil sets_lemmas nil) (set type-eq-decl nil sets nil) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (ball const-decl "set[T]" metric_space_def nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-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) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (r!1 skolem-const-decl "posreal" metric_space nil) (x!1 skolem-const-decl "T" metric_space nil) (x!2 skolem-const-decl "T" metric_space nil) (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (metric_triangle formula-decl nil metric_space nil) (subset? const-decl "bool" sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (ball_centre formula-decl nil metric_space nil)) shostak)) (metric_open_TCC1 0 (metric_open_TCC1-1 nil 3359138684 ("" (expand "metric_open_set") (("" (expand "emptyset") (("" (expand "metric_open?") (("" (skosimp) (("" (skosimp) (("" (expand "subset?") (("" (inst - "x!1") (("" (rewrite "ball_centre") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (ball_centre formula-decl nil metric_space 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) (>= 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) (member const-decl "bool" sets nil) (T formal-type-decl nil metric_space nil) (metric_open? const-decl "bool" metric_space_def nil) (metric_open_set const-decl "set[T]" metric_space nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (metric_closed_TCC1 0 (metric_closed_TCC1-1 nil 3359138684 ("" (expand "metric_closed_set") (("" (expand "metric_closed?") (("" (rewrite "complement_complement") (("" (rewrite "metric_open_TCC1") nil nil)) nil)) nil)) nil) ((metric_closed? const-decl "bool" metric_space_def nil) (metric_open_TCC1 subtype-tcc nil metric_space nil) (T formal-type-decl nil metric_space nil) (metric_open_set const-decl "set[T]" metric_space nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (complement_complement formula-decl nil sets_lemmas nil) (metric_closed_set const-decl "set[T]" metric_space nil)) shostak)) (ball_is_metric_open 0 (ball_is_metric_open-1 nil 3359138684 ("" (skosimp) (("" (expand "metric_open?") (("" (skosimp) (("" (split) (("1" (flatten) (("1" (case-replace "x!2=x!1") (("1" (inst + "r!1") (("1" (rewrite "subset_reflexive") nil nil)) nil) ("2" (lemma "metric_zero" ("x" "x!1" "y" "x!2")) (("2" (assert) (("2" (case "r!1-d(x!1,x!2)>0") (("1" (inst + "r!1 - d(x!1, x!2)") (("1" (expand "subset?") (("1" (skosimp) (("1" (expand "member") (("1" (expand "ball") (("1" (lemma "metric_triangle" ("x" "x!1" "y" "x!2" "z" "x!3")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (expand "ball") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (inst - "x!2") (("2" (rewrite "ball_centre") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((metric_open? const-decl "bool" metric_space_def nil) (T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (subset_reflexive formula-decl nil sets_lemmas nil) (set type-eq-decl nil sets nil) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (ball const-decl "set[T]" metric_space_def nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-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) (number nonempty-type-decl nil numbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (r!1 skolem-const-decl "posreal" metric_space nil) (x!1 skolem-const-decl "T" metric_space nil) (x!2 skolem-const-decl "T" metric_space nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (metric_triangle formula-decl nil metric_space nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (metric_zero formula-decl nil metric_space nil) (ball_centre formula-decl nil metric_space nil)) shostak)) (metric_space_is_topology? 0 (metric_space_is_topology?-1 nil 3382769693 ("" (expand "metric_induced_topology") (("" (expand "topology?") (("" (split) (("1" (expand "topology_empty?") (("1" (expand "member") (("1" (expand "metric_open?") (("1" (skosimp) (("1" (expand "emptyset") (("1" (skosimp) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (expand "ball") (("1" (rewrite "metric_is_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "topology_full?") (("2" (expand "fullset") (("2" (expand "member") (("2" (expand "metric_open?") (("2" (skosimp) (("2" (expand "subset?") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "topology_Union?") (("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp) (("3" (expand "metric_open?") (("3" (skosimp) (("3" (split 1) (("1" (flatten) (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (inst - "a!1") (("1" (assert) (("1" (inst - "x!1") (("1" (assert) (("1" (skosimp) (("1" (inst + "r!1") (("1" (expand "subset?") (("1" (skosimp) (("1" (inst - "x!2") (("1" (expand "member") (("1" (inst + "a!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (expand "Union") (("2" (expand "member") (("2" (inst - "x!1") (("2" (lemma "ball_centre" ("x" "x!1" "r" "r!1")) (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "topology_intersection?") (("4" (skosimp) (("4" (typepred "A!1") (("4" (typepred "B!1") (("4" (expand "intersection") (("4" (expand "metric_open?") (("4" (expand "member") (("4" (skosimp) (("4" (inst - "x!1") (("4" (inst - "x!1") (("4" (split 1) (("1" (flatten) (("1" (assert) (("1" (skosimp*) (("1" (inst + "min(r!1,r!2)") (("1" (hide -4 -6) (("1" (expand "subset?") (("1" (skosimp) (("1" (inst - "x!2") (("1" (inst - "x!2") (("1" (expand "member") (("1" (expand "ball") (("1" (expand "min") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp) (("2" (assert) (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (rewrite "ball_centre") (("2" (expand "member") (("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) ((topology? const-decl "bool" topology_prelim "topology/") (topology_intersection? const-decl "bool" topology_prelim "topology/") (d formal-const-decl "metric" metric_space nil) (metric nonempty-type-eq-decl nil metric_def nil) (metric? const-decl "bool" metric_def nil) (nnreal type-eq-decl nil real_types nil) (set type-eq-decl nil sets nil) (intersection const-decl "set" sets nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_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) (topology_Union? const-decl "bool" topology_prelim "topology/") (Union const-decl "set" sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (ball_is_metric_open application-judgement "metric_open" metric_space nil) (ball_centre formula-decl nil metric_space nil) (topology_full? const-decl "bool" topology_prelim "topology/") (fullset const-decl "set" sets nil) (topology_empty? const-decl "bool" topology_prelim "topology/") (metric_open? const-decl "bool" metric_space_def nil) (emptyset const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (metric_is_0 formula-decl nil metric_space nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_space_def nil) (T formal-type-decl nil metric_space nil) (member const-decl "bool" sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil)) nil)) (metric_space_is_hausdorff? 0 (metric_space_is_hausdorff?-1 nil 3359138686 ("" (expand "hausdorff?") (("" (expand "is_T2?") (("" (skosimp) (("" (lemma "metric_zero" ("x" "x!1" "y" "y!1")) (("" (assert) (("" (name "R" "d(x!1,y!1)/2") (("" (inst + "ball(x!1,R)" "ball(y!1,R)") (("1" (split 3) (("1" (expand "disjoint?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp) (("1" (expand "ball") (("1" (lemma "metric_triangle" ("x" "x!1" "y" "x!2" "z" "y!1")) (("1" (lemma "metric_symmetric" ("x" "y!1" "y" "x!2")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "ball_centre" ("x" "x!1" "r" "R")) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "ball_centre" ("x" "y!1" "r" "R")) (("3" (expand "member") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "metric_induced_topology") (("2" (propax) nil nil)) nil) ("3" (expand "metric_induced_topology") (("3" (propax) nil nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_T2? const-decl "bool" topology_prelim "topology/") (metric_zero formula-decl nil metric_space nil) (T formal-type-decl nil metric_space nil) (d formal-const-decl "metric" metric_space nil) (metric nonempty-type-eq-decl nil metric_def nil) (metric? const-decl "bool" metric_def 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (intersection const-decl "set" sets nil) (metric_symmetric formula-decl nil metric_space nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_triangle formula-decl nil metric_space nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (ball_centre formula-decl nil metric_space nil) (y!1 skolem-const-decl "T" metric_space nil) (x!1 skolem-const-decl "T" metric_space nil) (ball const-decl "set[T]" metric_space_def nil) (set type-eq-decl nil sets nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (R skolem-const-decl "nnreal" metric_space nil) (> const-decl "bool" reals nil) (ball_is_metric_open application-judgement "metric_open" metric_space nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (hausdorff? const-decl "bool" topology_prelim "topology/") (metric_space_is_topology? name-judgement "(topology?)" metric_space nil)) shostak)) (metric_space_is_hausdorff 0 (metric_space_is_hausdorff-1 nil 3384417346 ("" (judgement-tcc) nil nil) ((T formal-type-decl nil metric_space nil) (hausdorff_space? const-decl "bool" topology_prelim "topology/") (metric_space_is_topology? name-judgement "(topology?)" metric_space nil) (metric_space_is_hausdorff? name-judgement "(hausdorff?)" metric_space nil)) nil)) (metric_open_def 0 (metric_open_def-1 nil 3359138576 ("" (skosimp) (("" (expand "open?") (("" (expand "member") (("" (expand "metric_induced_topology") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((open? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (member const-decl "bool" sets nil)) shostak)) (metric_closed_def 0 (metric_closed_def-1 nil 3359138599 ("" (skosimp) (("" (expand "metric_closed?") (("" (expand "closed?") (("" (expand "metric_induced_topology") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((metric_closed? const-decl "bool" metric_space_def nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (member const-decl "bool" sets nil) (closed? const-decl "bool" topology "topology/")) shostak)) (metric_open_is_open 0 (metric_open_is_open-1 nil 3359138623 ("" (skosimp) (("" (rewrite "metric_open_def" 1 :dir rl) nil nil)) nil) ((metric_open_def formula-decl nil metric_space nil) (T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets 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) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (metric_open? const-decl "bool" metric_space_def nil) (metric_open nonempty-type-eq-decl nil metric_space nil)) shostak)) (open_is_metric_open 0 (open_is_metric_open-1 nil 3359138648 ("" (skosimp) (("" (rewrite "metric_open_def") nil nil)) nil) ((metric_open_def formula-decl nil metric_space nil) (T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets 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) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (open? const-decl "bool" topology "topology/") (open nonempty-type-eq-decl nil topology "topology/")) shostak)) (metric_closed_is_closed 0 (metric_closed_is_closed-1 nil 3359138658 ("" (skosimp) (("" (rewrite "metric_closed_def" 1 :dir rl) nil nil)) nil) ((metric_closed_def formula-decl nil metric_space nil) (T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets 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) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (metric_closed? const-decl "bool" metric_space_def nil) (metric_closed nonempty-type-eq-decl nil metric_space nil)) shostak)) (closed_is_metric_closed 0 (closed_is_metric_closed-1 nil 3359138674 ("" (skosimp) (("" (rewrite "metric_closed_def") nil nil)) nil) ((metric_closed_def formula-decl nil metric_space nil) (T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets 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) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/")) shostak)) (metric_adherent_iff_adherent 0 (metric_adherent_iff_adherent-1 nil 3406977548 ("" (skosimp) (("" (expand "metric_adherent?") (("" (expand "adherent_point?") (("" (split) (("1" (flatten) (("1" (skosimp*) (("1" (expand "neighbourhood?") (("1" (expand "interior_point?") (("1" (skosimp) (("1" (expand "member") (("1" (typepred "U!2") (("1" (typepred "U!1") (("1" (rewrite "metric_open_def" -1 :dir rl) (("1" (expand "metric_open?") (("1" (expand "nonempty?") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "subset?") (("1" (expand "member") (("1" (inst -4 "x!1") (("1" (assert) (("1" (inst - "x!1") (("1" (assert) (("1" (skosimp) (("1" (inst -3 "r!1") (("1" (skosimp) (("1" (inst - "x!2") (("1" (assert) (("1" (inst - "x!2") (("1" (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" (skosimp*) (("2" (expand "intersection") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "ball(x!1, r!1)") (("2" (split -1) (("1" (skosimp) (("1" (inst - "x!2") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "neighbourhood?") (("2" (expand "interior_point?") (("2" (inst + "ball(x!1, r!1)") (("2" (expand "subset?") (("2" (expand "member") (("2" (split) (("1" (skosimp) nil nil) ("2" (lemma "ball_centre" ("x" "x!1" "r" "r!1")) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((metric_adherent? const-decl "bool" metric_space_def nil) (interior_point? const-decl "bool" topology "topology/") (member const-decl "bool" sets nil) (metric_open? const-decl "bool" metric_space_def nil) (intersection const-decl "set" sets nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (ball_is_metric_open application-judgement "metric_open" metric_space nil) (subset? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (metric_open_def formula-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil metric_space nil) (set type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets 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) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (open? const-decl "bool" topology "topology/") (open nonempty-type-eq-decl nil topology "topology/") (neighbourhood? const-decl "bool" topology "topology/") (ball const-decl "set[T]" metric_space_def nil) (ball_centre formula-decl nil metric_space nil) (adherent_point? const-decl "bool" topology "topology/")) shostak)) (metric_closure_is_Cl 0 (metric_closure_is_Cl-1 nil 3406977926 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (expand "metric_closure") (("" (expand "Cl") (("" (rewrite "metric_adherent_iff_adherent") nil nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (Cl const-decl "set[T]" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (metric_closure const-decl "set[T]" metric_space_def nil) (d formal-const-decl "metric" metric_space nil) (metric nonempty-type-eq-decl nil metric_def nil) (metric? const-decl "bool" metric_def nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (metric_space_is_hausdorff name-judgement "hausdorff" metric_space nil) (metric_space_is_hausdorff? name-judgement "(hausdorff?)" metric_space nil) (Cl_is_closed application-judgement "closed[T, (metric_induced_topology)]" metric_space nil) (metric_adherent_iff_adherent formula-decl nil metric_space nil)) shostak)) (metric_convergence_def 0 (metric_convergence_def-1 nil 3390467646 ("" (expand "metric_converges_to") (("" (expand "convergence?") (("" (skosimp) (("" (split) (("1" (skosimp*) (("1" (inst - "ball(x!1, r!1)") (("1" (lemma "ball_centre" ("x" "x!1" "r" "r!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "U!1") (("2" (expand "open?") (("2" (expand "member") (("2" (expand "metric_induced_topology") (("2" (expand "metric_open?") (("2" (inst - "x!1") (("2" (assert) (("2" (skosimp) (("2" (inst - "r!1") (("2" (skosimp) (("2" (inst + "n!1") (("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) (("2" (expand "subset?") (("2" (inst - "u!1(i!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) ((convergence? const-decl "bool" topological_convergence "topology/") (ball_is_metric_open application-judgement "metric_open" metric_space nil) (T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets 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) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (open? const-decl "bool" topology "topology/") (open nonempty-type-eq-decl nil topology "topology/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (ball const-decl "set[T]" metric_space_def nil) (member const-decl "bool" sets nil) (ball_centre formula-decl nil metric_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (metric_open? const-decl "bool" metric_space_def 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) (subset? const-decl "bool" sets nil) (sequence type-eq-decl nil sequences nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (metric_converges_to const-decl "bool" metric_space_def nil)) shostak)) (compact_is_weierstrass_bolzano 0 (compact_is_weierstrass_bolzano-1 nil 3406536163 ("" (flatten) (("" (lemma "compact_def[T,(metric_induced_topology)]") (("" (flatten) (("" (hide -2) (("" (split) (("1" (expand "weierstrass_bolzano?") (("1" (skosimp) (("1" (name "AA" "lambda (n:nat): metric_closure({x | exists (m:nat): m>n & x = u!1(m)})") (("1" (case "forall (n,m:nat): n > m => subset?(AA(n),AA(m))") (("1" (inst -3 "image(AA,fullset[nat])") (("1" (hide -4) (("1" (split -3) (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "Intersection") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp*) (("1" (case "forall (n:nat): AA(n)(x!1)") (("1" (hide -2) (("1" (replace -3 -1 rl) (("1" (assert) (("1" (expand "metric_closure" -1) (("1" (expand "metric_adherent?") (("1" (expand "intersection") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "ball") (("1" (name "NEXT" "lambda (i:nat,k:posnat): (choose({j:nat | j>i & d(x!1,u!1(j)) <1/k}),k+1)") (("1" (name "SEQ" "lambda (n:nat): u!1((iterate[[nat, posnat]](NEXT, n)(0, 1))`1)") (("1" (inst + "SEQ") (("1" (split) (("1" (expand "subseq?") (("1" (expand "SEQ") (("1" (inst + "lambda (i:nat): (iterate[[nat, posnat]](NEXT, i)(0, 1))`1") (("1" (skosimp) nil nil) ("2" (expand "strict_increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (assert) (("2" (flatten) (("2" (lemma "iterate_add_applied[[nat, posnat]]" ("f" "NEXT" "x" "(0, 1)" "n" "i!1" "m" "j!1-i!1")) (("1" (assert) (("1" (replace -1 1 rl) (("1" (name-replace "DRL1" "(iterate[[nat, posnat]](NEXT, i!1)(0, 1))") (("1" (hide-all-but (1 -4 -2)) (("1" (case "forall (pn:posnat,x:[[nat, posnat]]): x`1 < (iterate(NEXT, pn)(x))`1") (("1" (inst - "j!1-i!1" "DRL1") nil nil) ("2" (hide 2) (("2" (induct "pn") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (case-replace "j!2=0") (("1" (hide -2 -1 -3 -4) (("1" (expand "iterate") (("1" (expand "iterate") (("1" (expand "NEXT") (("1" (lemma "choose_member" ("a" "{j: nat | j > x!2`1 & d(x!1, u!1(j)) < 1 / x!2`2}")) (("1" (case-replace "empty?({j: nat | j > x!2`1 & d(x!1, u!1(j)) < 1 / x!2`2})") (("1" (hide 1) (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -2 "x!2`1") (("1" (inst -2 "1/x!2`2") (("1" (skosimp) (("1" (skosimp) (("1" (inst - "m!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (name-replace "DRL4" "choose({j: nat | j > x!2`1 & d(x!1, u!1(j)) < 1 / x!2`2})") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "j!2>=1") (("1" (assert) (("1" (hide 1) (("1" (expand "iterate" 1) (("1" (inst - "x!2") (("1" (name-replace "DRL5" "iterate(NEXT, j!2)(x!2)") (("1" (expand "NEXT" 1) (("1" (lemma "choose_member" ("a" "{j: nat | j > DRL5`1 & d(x!1, u!1(j)) < 1 / DRL5`2}")) (("1" (case-replace "empty?({j: nat | j > DRL5`1 & d(x!1, u!1(j)) < 1 / DRL5`2})") (("1" (hide-all-but (-1 -6)) (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -2 "DRL5`1") (("1" (inst -2 "1/DRL5`2") (("1" (skosimp) (("1" (skosimp) (("1" (inst - "m!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (name-replace "DRL6" "choose({j: nat | j > DRL5`1 & d(x!1, u!1(j)) < 1 / DRL5`2})") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (expand "NEXT") (("4" (typepred "x1!1`2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "NEXT") (("3" (skosimp) (("3" (typepred "x1!1`2") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "metric_convergent?") (("2" (inst + "x!1") (("2" (case "forall (n:nat): (iterate[[nat, posnat]](NEXT, n)(0, 1))`2 = 1+n") (("1" (case "FORALL (n: nat): d(x!1, SEQ(n + 1)) < 1 / (1 + n)") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (lemma "archimedean" ("px" "r!1")) (("1" (skosimp) (("1" (inst + "1+n!1") (("1" (skosimp) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "i!1-1") (("1" (assert) (("1" (lemma "both_sides_div_pos_lt2" ("pz" "1" "py" "n!1" "px" "i!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -4 1)) (("2" (skosimp) (("2" (expand "SEQ") (("2" (expand "iterate" 1) (("2" (expand "NEXT" 1 1) (("2" (lemma "choose_member" ("a" "{j: nat | j > iterate(NEXT, n!1)(0, 1)`1 & d(x!1, u!1(j)) < 1 / iterate(NEXT, n!1)(0, 1)`2}")) (("1" (case-replace "empty?({j: nat | j > iterate(NEXT, n!1)(0, 1)`1 & d(x!1, u!1(j)) < 1 / iterate(NEXT, n!1)(0, 1)`2})") (("1" (hide -2 1) (("1" (inst - "iterate(NEXT, n!1)(0, 1)`1") (("1" (inst - "1/iterate(NEXT, n!1)(0, 1)`2") (("1" (skosimp) (("1" (skosimp) (("1" (expand "empty?") (("1" (inst - "m!1") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "NEXT") (("2" (typepred "x1!1`2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "x1!1`2") (("2" (expand "NEXT") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (name-replace "DRL11" "choose({j: nat | j > iterate(NEXT, n!1)(0, 1)`1 & d(x!1, u!1(j)) < 1 / iterate(NEXT, n!1)(0, 1)`2})") (("1" (expand "member") (("1" (flatten) (("1" (inst - "n!1") (("1" (replace -3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (expand "NEXT") (("2" (typepred "x1!1`2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "n") (("1" (expand "iterate") (("1" (propax) nil nil)) nil) ("2" (skosimp) (("2" (expand "iterate" 1) (("2" (expand "NEXT" 1 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "NEXT") (("3" (skosimp) (("3" (typepred "x1!1`2") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "NEXT") (("2" (skosimp) (("2" (typepred "x1!1`2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -2 "i!1") (("2" (inst -2 "1/k!1") (("2" (skosimp) (("2" (skosimp) (("2" (inst - "m!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) ("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (inst - "AA(n!1)") (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "every") (("2" (skosimp) (("2" (typepred "x!1") (("2" (skosimp) (("2" (replace -1) (("2" (hide -1) (("2" (expand "AA") (("2" (rewrite "metric_closure_is_Cl") (("2" (lemma "Cl_closed" ("A" "{x | EXISTS (m: nat): m > x!2 & x = u!1(m)}")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -2 2) (("3" (skosimp) (("3" (case "FORALL (Y: setofsets[T], pn: posnat): is_finite(Y) & card(Y) = pn & subset?(Y, image(AA, fullset[nat])) => exists (n:nat): Intersection(Y) = AA(n)") (("1" (case "card(Y1!1)>0") (("1" (inst - "Y1!1" "card(Y1!1)") (("1" (assert) (("1" (skosimp) (("1" (replace -2) (("1" (hide-all-but 1) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "AA") (("1" (inst - "u!1(n!1+1)") (("1" (expand "metric_closure") (("1" (expand "metric_adherent?") (("1" (skosimp) (("1" (expand "intersection") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "u!1(1 + n!1)") (("1" (split) (("1" (inst + "1+n!1") (("1" (assert) nil nil)) nil) ("2" (lemma "ball_centre" ("r" "r!1" "x" "u!1(1 + n!1)")) (("2" (expand "member") (("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) ("2" (case "card(Y1!1)=0") (("1" (lemma "card_is_0[set[T]]" ("S" "Y1!1")) (("1" (assert) (("1" (replace -2 -1) (("1" (replace -1) (("1" (hide-all-but 2) (("1" (expand "Intersection") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "u!1(0)") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "emptyset") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("3" (propax) nil nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (induct "pn") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (assert) (("3" (case-replace "j!1=0") (("1" (hide -1 -2 -3) (("1" (assert) (("1" (lemma "card_one[set[T]]" ("S" "Y!1")) (("1" (assert) (("1" (skosimp) (("1" (expand "subset?" -4) (("1" (expand "member") (("1" (inst - "x!1") (("1" (assert) (("1" (replace -1 -4) (("1" (expand "singleton" -4) (("1" (expand "fullset") (("1" (expand "image") (("1" (skolem - ("n!1")) (("1" (inst + "n!1") (("1" (replace -4) (("1" (replace -1) (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "j!1>=1") (("1" (hide 1) (("1" (inst - "rest(Y!1)") (("1" (lemma "choose_rest" ("a" "Y!1")) (("1" (lemma "rest_subset" ("a" "Y!1")) (("1" (lemma "subset_transitive" ("a" "rest(Y!1)" "b" "Y!1" "c" "image(AA, fullset[nat])")) (("1" (assert) (("1" (lemma "finite_rest[set[T]]" ("A" "Y!1")) (("1" (assert) (("1" (lemma "nonempty_card[set[T]]" ("S" "Y!1")) (("1" (assert) (("1" (expand "nonempty?" -1) (("1" (lemma "card_rest[set[T]]" ("S" "Y!1")) (("1" (assert) (("1" (skosimp) (("1" (lemma "choose_member" ("a" "Y!1")) (("1" (replace 1) (("1" (expand "member") (("1" (expand "subset?" -12) (("1" (expand "member") (("1" (inst -12 "choose(Y!1)") (("1" (assert) (("1" (expand "fullset") (("1" (expand "image") (("1" (skolem - ("n!2")) (("1" (inst + "max(n!1,n!2)") (("1" (rewrite "Intersection_intersection_rew" 2) (("1" (replace -8) (("1" (replace -12) (("1" (hide-all-but (-13 2)) (("1" (apply-extensionality :hide? t) (("1" (expand "intersection") (("1" (expand "member") (("1" (expand "max") (("1" (case-replace "n!1 < n!2") (("1" (inst - "n!2" "n!1") (("1" (assert) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (assert) (("1" (case-replace "AA(n!2)(x!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "n!2=n!1") (("1" (assert) (("1" (case-replace "AA(n!1)(x!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "n!1" "n!2") (("2" (assert) (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (expand "member") (("2" (case-replace "AA(n!1)(x!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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "subset?") (("2" (expand "AA") (("2" (expand "member") (("2" (expand "metric_closure") (("2" (expand "metric_adherent?") (("2" (expand "intersection") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst -2 "r!1") (("2" (skosimp) (("2" (skosimp) (("2" (inst - "x!2") (("2" (assert) (("2" (inst + "m!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) ("2" (hide 2) (("2" (expand "compact_space?") (("2" (expand "compact?") (("2" (case-replace "Union((metric_induced_topology)) = fullset[T]") (("1" (expand "fullset") (("1" (expand "Union") (("1" (replace -2) (("1" (typepred "metric_induced_topology") (("1" (expand "hausdorff_space?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "fullset") (("2" (expand "Union") (("2" (inst + "ball(x!1,1)") (("1" (expand "ball") (("1" (assert) (("1" (typepred "d") (("1" (expand "metric?") (("1" (flatten) (("1" (expand "metric_zero?") (("1" (inst - "x!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "metric_induced_topology") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (d formal-const-decl "metric" metric_space nil) (metric nonempty-type-eq-decl nil metric_def nil) (metric? const-decl "bool" metric_def nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil metric_space nil) (compact_def formula-decl nil topology "topology/") (compact? const-decl "bool" topology "topology/") (x!1 skolem-const-decl "T" metric_space nil) (metric_zero? const-decl "bool" metric_def nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (hausdorff? const-decl "bool" topology_prelim "topology/") (hausdorff_space? const-decl "bool" topology_prelim "topology/") (fullset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" metric_space nil) (Union const-decl "set" sets nil) (compact_space? const-decl "bool" topology_prelim "topology/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" metric_space nil) (metric_space_is_hausdorff name-judgement "hausdorff" metric_space nil) (weierstrass_bolzano? const-decl "bool" metric_space nil) (sequence type-eq-decl nil sequences nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (metric_closure const-decl "set[T]" metric_space_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (ball_is_metric_open application-judgement "metric_open" metric_space nil) (fullset const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (ball const-decl "set[T]" metric_space_def nil) (iterate def-decl "T" function_iterate nil) (SEQ skolem-const-decl "[nat -> T]" metric_space nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (iterate_add_applied formula-decl nil function_iterate nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (choose_member formula-decl nil sets_lemmas nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (NEXT skolem-const-decl "[d1: [nat, posnat] -> [({j: nat | j > d1`1 & d(x!1, u!1(j)) < 1 / d1`2}), numfield]]" metric_space nil) (u!1 skolem-const-decl "sequence[T]" metric_space nil) (x!1 skolem-const-decl "T" metric_space nil) (subseq? const-decl "bool" subseq "topology/") (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (both_sides_div_pos_lt2 formula-decl nil real_props nil) (i!1 skolem-const-decl "nat" metric_space nil) (archimedean formula-decl nil real_props nil) (metric_converges_to const-decl "bool" metric_space_def nil) (metric_convergent? const-decl "bool" metric_space_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (choose const-decl "(p)" sets 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) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (metric_adherent? const-decl "bool" metric_space_def nil) (n!1 skolem-const-decl "nat" metric_space nil) (AA skolem-const-decl "[nat -> set[T]]" metric_space nil) (TRUE const-decl "bool" booleans nil) (empty? const-decl "bool" sets nil) (Intersection const-decl "set" sets nil) (every const-decl "bool" sets nil) (Cl_closed formula-decl nil topology "topology/") (Cl_is_closed application-judgement "closed[T, (metric_induced_topology)]" metric_space nil) (metric_closure_is_Cl formula-decl nil metric_space nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_setofsets "sets_aux/") (card_one formula-decl nil finite_sets nil) (rest const-decl "set" sets nil) (rest_subset formula-decl nil sets_lemmas nil) (card_rest formula-decl nil finite_sets nil) (Intersection_intersection_rew formula-decl nil sets_lemmas nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nonempty_card formula-decl nil finite_sets nil) (finite_rest judgement-tcc nil finite_sets nil) (subset_transitive formula-decl nil sets_lemmas nil) (choose_rest formula-decl nil sets_lemmas nil) (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (ball_centre formula-decl nil metric_space nil) (Y1!1 skolem-const-decl "setofsets[T]" metric_space nil) (card_is_0 formula-decl nil finite_sets nil) (emptyset const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[finite_set[T]]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[set[T]]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (subset? const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) shostak)) (cauchy_subseq_is_totally_bounded 0 (cauchy_subseq_is_totally_bounded-1 nil 3397740732 ("" (skosimp*) (("" (expand "fullset") (("" (expand "totally_bounded?") (("" (skosimp) (("" (case "is_finite(fullset[T])") (("1" (inst + "fullset[T]") (("1" (expand "epsilon_net?") (("1" (assert) (("1" (expand "fullset") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) (("1" (expand "image") (("1" (expand "Union") (("1" (inst + "ball(x!1,r!1)") (("1" (lemma "ball_centre" ("x" "x!1" "r" "r!1")) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "forall (X:set[T]): is_finite(X) & nonempty?(X) => exists (y:T): NOT X(y) & for (("1" (case "nonempty?(fullset[T])") (("1" (expand "nonempty?" -1) (("1" (expand "fullset" 1) (("1" (expand "empty?" 1) (("1" (skosimp) (("1" (expand "member") (("1" (name "NEXT" "lambda (X: non_empty_finite_set[T]):choose[T] ({y: T | NOT X(y) & (FORALL x: X(x) => d(x, y) >= r!1)})") (("1" (name "ADD" "LAMBDA (X: non_empty_finite_set[T]): add[T](NEXT(X),X)") (("1" (name "XX" "lambda (n:nat): iterate(ADD,n)(singleton[T](x!1))") (("1" (name "UU" "lambda (n:nat): NEXT(XX(n))") (("1" (inst -6 "UU") (("1" (skosimp) (("1" (expand "subseq?") (("1" (skosimp) (("1" (replace -1 -7 rl) (("1" (assert) (("1" (hide 1 2) (("1" (expand "cauchy?") (("1" (inst -6 "r!1") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (case "forall (i,j:nat): i<j => d(v!1(j), v!1(i)) >= r!1") (("1" (inst - "n!1" "n!1+1") (("1" (inst -7 "n!1" "n!1+1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide -6) (("2" (hide -1) (("2" (skosimp) (("2" (inst-cp -6 "i!1") (("2" (inst -6 "j!1") (("2" (replace -6) (("2" (replace -7) (("2" (hide -6 -7) (("2" (typepred "f!1") (("2" (expand "strict_increasing?") (("2" (inst - "i!1" "j!1") (("2" (replace -2 -1) (("2" (hide -2) (("2" (name-replace "m" "f!1(i!1)") (("2" (name-replace "n" "f!1(j!1)") (("2" (expand "NEXT" 1) (("2" (lemma "choose_member[T]" ("a" "{y: T | NOT XX(n)(y) & (FORALL x: XX(n)(x) => d(x, y) >= r!1)}")) (("2" (inst-cp -6 "XX(n)") (("2" (typepred "XX(n)") (("2" (expand "nonempty?" -8) (("2" (replace 1) (("2" (split -2) (("1" (name-replace "Xn" "choose[T] ({y: T | NOT XX(n)(y) & (FORALL x: XX(n)(x) => d(x, y) >= r!1)})") (("1" (expand "member") (("1" (flatten) (("1" (lemma "choose_member[T]" ("a" "{y_1: T | NOT XX(m)(y_1) & (FORALL (x_1: T): XX(m)(x_1) => d(x_1, y_1) >= r!1)}")) (("1" (name-replace "Xm" "choose[T] ({y_1: T | NOT XX(m)(y_1) & (FORALL (x_1: T): XX(m)(x_1) => d(x_1, y_1) >= r!1)})") (("1" (split -1) (("1" (expand "member") (("1" (flatten) (("1" (inst -2 "Xm") (("1" (split -2) (("1" (hide-all-but (-1 4)) (("1" (rewrite "metric_symmetric") nil nil)) nil) ("2" (hide -1 5) (("2" (case "forall (i:nat): XX(i+1+m)(Xm)") (("1" (inst - "n-m-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide -7 2 4 5 -1 -2) (("2" (skosimp) (("2" (case "XX(m+1)(Xm)") (("1" (case "forall (i,j:nat): subset?(XX(i),XX(i+j))") (("1" (inst - "m+1" "i!2") (("1" (expand "subset?") (("1" (inst - "Xm") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 3 -1) (("2" (induct "j") (("1" (skosimp) (("1" (simplify 1) (("1" (expand "subset?") (("1" (skosimp) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "i!3+1") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "x!2") (("2" (split -) (("1" (propax) nil nil) ("2" (hide-all-but (-1 1)) (("2" (expand "XX") (("2" (expand "iterate" 1) (("2" (expand "ADD" 1 1) (("2" (expand "add" 1) (("2" (flatten) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (expand "Xm" 1) (("2" (expand "XX" 1 1) (("2" (expand "iterate" 1) (("2" (assert) (("2" (typepred "m") (("2" (split 1) (("1" (flatten) (("1" (hide-all-but (-1 -2)) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (expand "ADD" 1 1) (("2" (expand "add" 1) (("2" (flatten) (("2" (hide 2) (("2" (expand "NEXT" 1) (("2" (expand "XX" 1) (("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)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (hide 2) (("2" (hide -7 -9 2) (("2" (inst -7 "XX(m)") (("2" (assert) (("2" (typepred "XX(m)") (("2" (expand "nonempty?") (("2" (skosimp) (("2" (inst - "y!1") (("2" (replace -7) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?" 1) (("2" (assert) (("2" (hide-all-but (-1 -9)) (("2" (inst - "XX(m)") (("2" (typepred "XX(m)") (("2" (expand "nonempty?") (("2" (assert) (("2" (skosimp) (("2" (expand "empty?" -2) (("2" (expand "member") (("2" (inst - "y!1") (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (skosimp) (("2" (inst - "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (skosimp) (("2" (inst - "y!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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (typepred "X!1") (("2" (inst - "X!1") (("2" (expand "nonempty?") (("2" (assert) (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (skosimp) (("2" (inst - "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (rewrite "emptyset_is_empty?") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "epsilon_net?") (("2" (inst 3 "X!1") (("2" (assert) (("2" (expand "image") (("2" (expand "Union") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (inst 1 "x!1") (("2" (assert) (("2" (case-replace "X!1(x!1)") (("1" (inst + "ball(x!1,r!1)") (("1" (lemma "ball_centre" ("x" "x!1" "r" "r!1")) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (inst + "x!1") nil nil)) nil) ("2" (replace 1) (("2" (skosimp) (("2" (inst + "ball(x!2,r!1)") (("1" (expand "ball") (("1" (assert) nil nil)) nil) ("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" metric_space nil) (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" metric_space nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (empty? const-decl "bool" sets nil) (nonempty_add_finite application-judgement "non_empty_finite_set[T]" countable_setofsets "sets_aux/") (add const-decl "(nonempty?)" sets nil) (cauchy? const-decl "bool" metric_space_def nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (choose_member formula-decl nil sets_lemmas nil) (XX skolem-const-decl "[nat -> non_empty_finite_set[T]]" metric_space nil) (ADD skolem-const-decl "[non_empty_finite_set[T] -> non_empty_finite_set[T]]" metric_space nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (Xm skolem-const-decl "({y_1: T | NOT XX(m)(y_1) & (FORALL (x_1: T): XX(m)(x_1) => d(x_1, y_1) >= r!1)})" metric_space nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (m skolem-const-decl "nat" metric_space nil) (n skolem-const-decl "nat" metric_space nil) (int_plus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (metric_symmetric formula-decl nil metric_space nil) (NEXT skolem-const-decl "[X: non_empty_finite_set[T] -> ({y: T | NOT X(y) & (FORALL x: X(x) => d(x, y) >= r!1)})]" metric_space nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (< const-decl "bool" reals nil) (subseq? const-decl "bool" subseq "topology/") (sequence type-eq-decl nil sequences nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (iterate def-decl "T" function_iterate 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) (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" metric_space nil) (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" metric_space nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_setofsets "sets_aux/") (finite_set type-eq-decl nil finite_sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (choose const-decl "(p)" sets nil) (x!1 skolem-const-decl "T" metric_space nil) (X!1 skolem-const-decl "set[T]" metric_space nil) (x!2 skolem-const-decl "T" metric_space nil) (subset? const-decl "bool" sets nil) (Union const-decl "set" sets nil) (ball_centre formula-decl nil metric_space nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (metric? const-decl "bool" metric_def nil) (metric nonempty-type-eq-decl nil metric_def nil) (d formal-const-decl "metric" metric_space nil) (ball const-decl "set[T]" metric_space_def nil) (x!1 skolem-const-decl "T" metric_space nil) (r!1 skolem-const-decl "posreal" metric_space nil) (ball_is_metric_open application-judgement "metric_open" metric_space nil) (image const-decl "set[R]" function_image nil) (member const-decl "bool" sets nil) (epsilon_net? const-decl "bool" metric_space_def nil) (fullset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" metric_space nil) (T formal-type-decl nil metric_space nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (totally_bounded? const-decl "bool" metric_space_def nil)) shostak)) (totally_bounded_is_separable 0 (totally_bounded_is_separable-1 nil 3398103975 ("" (flatten) (("" (expand "fullset") (("" (expand "totally_bounded?") (("" (name "F" "lambda (n:nat): choose({X:set[T] | epsilon_net?({x: T | TRUE},X,1/(n+1))})") (("1" (name "A" "IUnion(F)") (("1" (case "is_countable(A)") (("1" (expand "separable?") (("1" (inst + "A") (("1" (replace -1) (("1" (expand "subset?") (("1" (expand "member") (("1" (expand "dense_in?") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) (("1" (expand "metric_closure") (("1" (expand "metric_adherent?") (("1" (skosimp) (("1" (lemma "archimedean" ("px" "r!1")) (("1" (skosimp) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (hide -4 -5) (("1" (typepred "F(n!1-1)") (("1" (expand "epsilon_net?") (("1" (flatten) (("1" (hide -1 -2) (("1" (expand "image") (("1" (expand "Union") (("1" (expand "subset?") (("1" (expand "member") (("1" (inst - "x!1") (("1" (skosimp) (("1" (typepred "a!1") (("1" (skosimp) (("1" (typepred "x!2") (("1" (replace -2) (("1" (hide -2) (("1" (inst - "x!2") (("1" (expand "intersection") (("1" (expand "member") (("1" (split) (("1" (replace -5 * rl) (("1" (hide -5 -4) (("1" (expand "IUnion") (("1" (inst + "n!1-1") nil nil)) nil)) nil)) nil) ("2" (expand "ball") (("2" (rewrite "metric_symmetric") (("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)) nil)) nil) ("2" (hide 2) (("2" (lemma "countable_union1[T]") (("2" (inst - "image[nat,set[T]](F,fullset[nat])") (("2" (expand "fullset") (("2" (case-replace "Union(image[nat, set[T]](F, {x: nat | TRUE}))=A") (("1" (split) (("1" (propax) nil nil) ("2" (hide 2) (("2" (lemma "countable_image[nat, set[T]]" ("f" "F" "S" "{x_1: nat | TRUE}")) (("2" (split -1) (("1" (expand "image" -1) (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "is_countable") (("2" (inst + "lambda (n:nat): n") (("2" (expand "injective?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "every") (("3" (skosimp) (("3" (typepred "x!1") (("3" (expand "image") (("3" (skosimp) (("3" (hide -2 -3 -4) (("3" (typepred "F(x!2)") (("3" (expand "epsilon_net?") (("3" (flatten) (("3" (replace -4 * rl) (("3" (hide-all-but (-1 1)) (("3" (lemma "finite_countable" ("x" "x!1")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (replace -2 1 rl) (("2" (hide-all-but 1) (("2" (expand "IUnion") (("2" (case-replace "EXISTS (i: nat): F(i)(x!1)") (("1" (skosimp) (("1" (expand "image") (("1" (expand "Union") (("1" (inst + "F(i!1)") (("1" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (inst + "x!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) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "1/(n!1+1)") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "X!1") (("2" (expand "epsilon_net?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset const-decl "set" sets nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities 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) (TRUE const-decl "bool" booleans nil) (epsilon_net? const-decl "bool" metric_space_def nil) (d formal-const-decl "metric" metric_space nil) (metric nonempty-type-eq-decl nil metric_def nil) (metric? const-decl "bool" metric_def nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil metric_space nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_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) (is_countable const-decl "bool" countability "sets_aux/") (subset? const-decl "bool" sets nil) (dense_in? const-decl "bool" metric_space_def nil) (metric_closure const-decl "set[T]" metric_space_def nil) (empty? const-decl "bool" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (image const-decl "set[R]" function_image nil) (ball const-decl "set[T]" metric_space_def nil) (intersection const-decl "set" sets nil) (metric_symmetric formula-decl nil metric_space nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Union const-decl "set" sets nil) (archimedean formula-decl nil real_props nil) (metric_adherent? const-decl "bool" metric_space_def nil) (member const-decl "bool" sets nil) (separable? const-decl "bool" metric_space_def nil) (countable_union1 formula-decl nil countable_setofsets "sets_aux/") (i!1 skolem-const-decl "nat" metric_space nil) (F skolem-const-decl "[n: nat -> ({X: set[T] | epsilon_net?({x: T | TRUE}, X, 1 / (n + 1))})]" metric_space nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (countable_image formula-decl nil countable_image "sets_aux/") (injective? const-decl "bool" functions nil) (image const-decl "set[R]" function_image nil) (every const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_countable judgement-tcc nil countable_props "sets_aux/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (totally_bounded? const-decl "bool" metric_space_def nil)) shostak)) (separable_has_countable_basis 0 (separable_has_countable_basis-1 nil 3398131538 ("" (flatten) (("" (expand "has_countable_basis?") (("" (expand "fullset") (("" (expand "separable?") (("" (skosimp) (("" (expand "dense_in?") (("" (flatten) (("" (expand "subset?") (("" (expand "member") (("" (hide -1 -3) (("" (copy -1) (("" (expand "is_countable" -1) (("" (skosimp) (("" (name "BALLS" "{B:set[T] | exists (x:(X!1), n:nat): B = ball(x,1/(n+1))}") (("" (case "is_countable(BALLS)") (("1" (inst + "BALLS") (("1" (assert) (("1" (hide -1 -3) (("1" (split) (("1" (expand "synthetic_base?") (("1" (split) (("1" (inst + "BALLS") (("1" (expand "subset?") (("1" (expand "member") (("1" (split) (("1" (skosimp) nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "fullset") (("2" (inst - "x!1") (("2" (expand "metric_closure") (("2" (expand "metric_adherent?") (("2" (expand "Union") (("2" (expand "intersection") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "1") (("2" (skosimp) (("2" (inst + "ball(x!2,1)") (("1" (expand "ball") (("1" (rewrite "metric_symmetric") nil nil)) nil) ("2" (expand "BALLS") (("2" (inst + "x!2" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "B2!1") (("2" (typepred "B1!1") (("2" (hide -3) (("2" (inst + "{B:set[T] | BALLS(B) & subset?(B,B1!1) & subset?(B,B2!1)}") (("2" (split) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) nil nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "Union") (("2" (case-replace "B1!1(x!1) AND B2!1(x!1)") (("1" (flatten) (("1" (expand "BALLS") (("1" (skosimp*) (("1" (expand "ball") (("1" (replace -3) (("1" (replace -4) (("1" (assert) (("1" (expand "metric_closure") (("1" (expand "metric_adherent?") (("1" (inst - "x!1") (("1" (lemma "archimedean" ("px" "min(1 / (1 + n!1) - d(x!2, x!1), 1 / (1 + n!2) - d(x!3, x!1))")) (("1" (skosimp) (("1" (inst - "1/(2*n!3)") (("1" (expand "intersection") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp) (("1" (expand "member") (("1" (flatten) (("1" (expand "ball") (("1" (inst + "ball(x!4,1 / (2 * n!3))") (("1" (expand "ball") (("1" (rewrite "metric_symmetric" 1) nil nil)) nil) ("2" (split) (("1" (expand "BALLS") (("1" (inst + "x!4" "2*n!3-1") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (replace -5) (("2" (assert) (("2" (expand "ball") (("2" (lemma "metric_triangle" ("x" "x!2" "y" "x!1" "z" "x!5")) (("2" (lemma "metric_triangle" ("x" "x!1" "y" "x!4" "z" "x!5")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp) (("3" (expand "ball") (("3" (replace -6) (("3" (assert) (("3" (lemma "metric_triangle" ("x" "x!3" "y" "x!1" "z" "x!5")) (("3" (lemma "metric_triangle" ("x" "x!1" "y" "x!4" "z" "x!5")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "member") (("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" (expand "metric_induced_topology") (("2" (expand "synthetic_generated_topology_set") (("2" (apply-extensionality :hide? t) (("2" (case-replace "metric_open?(x!1)") (("1" (inst + "{A:set[T] | BALLS(A) & subset?(A,x!1)}") (("1" (split) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) nil nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (case-replace "x!1(x!2)") (("1" (expand "Union") (("1" (inst - "x!2") (("1" (expand "metric_closure") (("1" (expand "metric_adherent?") (("1" (expand "metric_open?") (("1" (inst - "x!2") (("1" (assert) (("1" (skosimp) (("1" (expand "subset?") (("1" (expand "member") (("1" (hide -3) (("1" (expand "intersection") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "archimedean" ("px" "r!1")) (("1" (skosimp) (("1" (inst -4 "1/(2*n!1)") (("1" (skosimp) (("1" (expand "ball") (("1" (inst + "ball(x!3,1/(2*n!1))") (("1" (expand "ball") (("1" (rewrite "metric_symmetric") nil nil)) nil) ("2" (split) (("1" (expand "BALLS") (("1" (inst + "x!3" "2*n!1-1") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "ball") (("2" (lemma "metric_triangle" ("x" "x!2" "y" "x!3" "z" "x!4")) (("2" (inst - "x!4") (("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) ("2" (assert) (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "subset?") (("2" (inst - "x!2") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (lemma "open_Union" ("Y" "V!1")) (("2" (rewrite "metric_open_def") (("2" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but (-1 1)) (("2" (expand "every") (("2" (skosimp) (("2" (typepred "x!2") (("2" (expand "subset?") (("2" (inst - "x!2") (("2" (expand "member") (("2" (assert) (("2" (expand "BALLS") (("2" (skosimp) (("2" (lemma "metric_open_ball" ("x" "x!3" "r" "1/(1+n!1)")) (("2" (rewrite "metric_open_def") (("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" (hide-all-but (-2 1)) (("2" (lemma "is_countable_cross[T,nat]") (("2" (inst - "X!1" "fullset[nat]") (("2" (assert) (("2" (split -1) (("1" (hide -2) (("1" (expand "cross_product") (("1" (lemma "countable_image[[T, nat],set[T]]") (("1" (inst - "{x: [T, nat] | X!1(x`1) AND fullset[nat](x`2)}" "_") (("1" (replace -2) (("1" (inst - "lambda (xr:[T, nat]): ball(xr`1,1/(1+xr`2))") (("1" (expand "image") (("1" (expand "fullset") (("1" (hide -2) (("1" (case-replace "(image(LAMBDA (xr: [T, nat]): ball(xr`1, 1 / (1 + xr`2)), {x: [T, nat] | X!1(x`1)}))=BALLS") (("1" (hide -1 2) (("1" (apply-extensionality :hide? t) (("1" (expand "image") (("1" (case-replace "BALLS(x!1)") (("1" (expand "BALLS") (("1" (skosimp) (("1" (inst + "(x!2,n!1)") nil nil)) nil)) nil) ("2" (assert) (("2" (expand "BALLS") (("2" (skosimp) (("2" (inst + "x!2`1" "x!2`2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "fullset") (("2" (expand "is_countable") (("2" (inst + "lambda (n:nat): n") (("2" (expand "injective?") (("2" (skosimp) 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) ((has_countable_basis? const-decl "bool" topology_def "topology/") (separable? const-decl "bool" metric_space_def nil) (dense_in? const-decl "bool" metric_space_def nil) (subset? const-decl "bool" sets nil) (is_countable const-decl "bool" countability "sets_aux/") (+ 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) (ball const-decl "set[T]" metric_space_def nil) (d formal-const-decl "metric" metric_space nil) (metric nonempty-type-eq-decl nil metric_def nil) (metric? const-decl "bool" metric_def nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil metric_space nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (ball_is_metric_open application-judgement "metric_open" metric_space nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (cross_product const-decl "set[[T1, T2]]" cross_product "topology/") (image const-decl "set[R]" function_image nil) (image const-decl "set[R]" function_image nil) (countable_image formula-decl nil countable_image "sets_aux/") (injective? const-decl "bool" functions nil) (TRUE const-decl "bool" booleans nil) (is_countable_cross formula-decl nil countable_cross nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (metric_open? const-decl "bool" metric_space_def nil) (metric_open_def formula-decl nil metric_space nil) (metric_open_ball formula-decl nil metric_space nil) (every const-decl "bool" sets nil) (open_Union formula-decl nil topology "topology/") (x!3 skolem-const-decl "T" metric_space nil) (n!1 skolem-const-decl "posnat" metric_space nil) (x!1 skolem-const-decl "[T -> boolean]" metric_space nil) (synthetic_generated_topology_set const-decl "setofsets[T]" basis "topology/") (synthetic_base? const-decl "bool" basis "topology/") (AND const-decl "[bool, bool -> bool]" booleans nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (metric_triangle formula-decl nil metric_space nil) (B2!1 skolem-const-decl "(BALLS)" metric_space nil) (B1!1 skolem-const-decl "(BALLS)" metric_space nil) (n!3 skolem-const-decl "posnat" metric_space nil) (x!4 skolem-const-decl "T" metric_space nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (archimedean formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (Union const-decl "set" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (fullset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" metric_space nil) (metric_adherent? const-decl "bool" metric_space_def nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (BALLS skolem-const-decl "[set[T] -> boolean]" metric_space nil) (x!2 skolem-const-decl "T" metric_space nil) (metric_symmetric formula-decl nil metric_space nil) (X!1 skolem-const-decl "set[T]" metric_space nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nonempty? const-decl "bool" sets nil) (metric_closure const-decl "set[T]" metric_space_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" sets nil) (fullset const-decl "set" sets nil)) shostak)) (compact_iff_convergent_subseq 0 (compact_iff_convergent_subseq-1 nil 3398127236 ("" (split) (("1" (flatten) (("1" (lemma "compact_is_weierstrass_bolzano") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "weierstrass_bolzano?") (("2" (lemma "cauchy_subseq_is_totally_bounded") (("2" (split -1) (("1" (lemma "totally_bounded_is_separable") (("1" (assert) (("1" (lemma "lindelof[T,metric_induced_topology]") (("1" (expand "compact?") (("1" (expand "compact_subset?") (("1" (skosimp) (("1" (inst - "U!1") (("1" (assert) (("1" (skosimp) (("1" (expand "subcover?") (("1" (flatten) (("1" (lemma "Union_IUnion") (("1" (lemma "Union_IUnion" ("XS" "V!1")) (("1" (assert) (("1" (skosimp) (("1" (name "WW" "lambda (n:nat): IUnion[T](n,YS!1)") (("1" (case "forall (n:nat): nonempty?[T](difference(fullset[T],WW(n)))") (("1" (name "XX" "lambda (n:nat): choose[T]({x:T | difference(fullset[T], WW(n))(x)})") (("1" (inst -13 "XX") (("1" (skosimp) (("1" (expand "metric_convergent?") (("1" (skosimp) (("1" (expand "open_cover?") (("1" (hide -1 1 -12 -11 -8 -6) (("1" (case "forall (n:nat): difference(fullset[T], WW(n))(XX(n))") (("1" (expand "cover?") (("1" (expand "subset?" -7) (("1" (inst -7 "x!1") (("1" (expand "member") (("1" (expand "fullset" -7) (("1" (expand "subset?" -11) (("1" (expand "member") (("1" (expand "metric_induced_topology") (("1" (replace -4 -7) (("1" (expand "IUnion" -7) (("1" (skosimp) (("1" (case "forall (n:nat): metric_open?(WW(n))") (("1" (case "forall (i,j:nat): i<=j=>subset?(WW(i),WW(j))") (("1" (expand "subseq?") (("1" (skosimp) (("1" (typepred "f!1") (("1" (case "FORALL (n: nat): n >= i!1 => WW(f!1(n))(x!1)") (("1" (inst - "i!1") (("1" (assert) (("1" (inst -4 "f!1(i!1)") (("1" (name "II" "f!1(i!1)") (("1" (replace -1) (("1" (expand "metric_open?" -5) (("1" (inst -5 "x!1") (("1" (assert) (("1" (skosimp) (("1" (expand "metric_converges_to") (("1" (expand "member") (("1" (inst -15 "r!1") (("1" (skosimp) (("1" (inst -15 "i!1+n!1+1") (("1" (inst -14 "i!1+n!1+1") (("1" (assert) (("1" (expand "strict_increasing?") (("1" (inst -3 "i!1" "1 + i!1 + n!1") (("1" (assert) (("1" (replace -1) (("1" (name "JJ" "f!1(1 + i!1 + n!1)") (("1" (replace -1) (("1" (replace -15) (("1" (hide-all-but (-3 -4 -6 -5 -7 -16)) (("1" (inst - "II" "JJ") (("1" (assert) (("1" (inst - "JJ") (("1" (expand "difference") (("1" (expand "member") (("1" (flatten) (("1" (hide -5) (("1" (expand "subset?") (("1" (inst -4 "XX(JJ)") (("1" (expand "member") (("1" (inst - "XX(JJ)") (("1" (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) ("2" (skosimp) (("2" (lemma "subseq_index" ("f" "f!1" "i" "n!1")) (("2" (inst -4 "i!1" "f!1(n!1)") (("2" (assert) (("2" (expand "subset?" -4) (("2" (inst - "x!1") (("2" (assert) (("2" (hide 1) (("2" (replace -7 1 rl) (("2" (assert) (("2" (expand "IUnion" 1) (("2" (expand "image") (("2" (expand "Union") (("2" (inst + "YS!1(i!1)") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "WW") (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (skosimp) (("2" (inst + "a!1") (("2" (typepred "a!1") (("2" (skosimp) (("2" (inst + "x!3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "n") (("1" (expand "WW") (("1" (rewrite "IUnion_0_def") (("1" (inst -4 "0") (("1" (split) (("1" (rewrite "emptyset_is_empty?") (("1" (replace -1) (("1" (assert) (("1" (expand "metric_open?") (("1" (expand "emptyset") (("1" (skosimp) (("1" (skosimp) (("1" (expand "subset?") (("1" (expand "member") (("1" (inst -2 "x!2") (("1" (hide-all-but 1) (("1" (lemma "ball_centre" ("x" "x!2" "r" "r!1")) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (inst -7 "YS!1(0)") (("2" (inst -10 "YS!1(0)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "WW") (("2" (rewrite "IUnion_n_def" 1) (("2" (assert) (("2" (inst -5 "1 + j!1") (("2" (hide-all-but (-1 -5 1 -8 -11)) (("2" (rewrite "metric_open_def") (("2" (rewrite "metric_open_def") (("2" (split) (("1" (rewrite "emptyset_is_empty?") (("1" (replace -1) (("1" (rewrite "union_empty") nil nil)) nil)) nil) ("2" (expand "subset?") (("2" (inst - "YS!1(1 + j!1)") (("2" (inst - "YS!1(1 + j!1)") (("2" (assert) (("2" (rewrite "metric_open_def") (("2" (rewrite "union_is_open") 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" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (expand "XX") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "n!1") (("2" (hide-all-but (-1 1)) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "nonempty?") (("2" (hide -5) (("2" (name "VV" "{X:set[T] | V!1(X) & exists (n:nat): n <= n!1 & YS!1(n) = X}") (("2" (inst + "VV") (("2" (split) (("1" (expand "subset?") (("1" (skosimp) (("1" (inst -10 "x!1") (("1" (assert) (("1" (replace -2 -1 rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "finite_cover?" 1) (("2" (split) (("1" (expand "VV") (("1" (hide -1) (("1" (lemma "finite_subset[set[T]]" ("A" "image(YS!1,{n:nat| n <= n!1})" "s" "{X: set[T] | V!1(X) & (EXISTS (n: nat): n <= n!1 & YS!1(n) = X)}")) (("1" (assert) (("1" (hide 2) (("1" (expand "subset?" 1) (("1" (expand "member") (("1" (skosimp) (("1" (skosimp) (("1" (expand "image") (("1" (inst + "n!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_image[nat,set[T]]" ("f" "YS!1" "S" "{n: nat | n <= n!1}")) (("1" (propax) nil nil) ("2" (hide-all-but 1) (("2" (expand "is_finite") (("2" (inst + "n!1+1" "lambda (x:{n: nat | n <= n!1}): x") (("2" (expand "injective?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "cover?" 1) (("2" (expand "subset?" 1) (("2" (skosimp) (("2" (expand "member") (("2" (expand "VV") (("2" (expand "Union") (("2" (expand "fullset") (("2" (expand "empty?") (("2" (inst - "x!1") (("2" (expand "difference") (("2" (expand "member") (("2" (replace -2 -1 rl) (("2" (assert) (("2" (expand "IUnion" -1) (("2" (expand "image" -1) (("2" (expand "Union" -1) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (inst + "a!1") (("2" (assert) (("2" (typepred "x!2") (("2" (inst -6 "x!2") (("2" (split -6) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst + "x!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)) 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 -3 -2) (("2" (expand "second_countable?") (("2" (expand "has_countable_basis?") (("2" (lemma "separable_has_countable_basis") (("2" (assert) (("2" (hide -2) (("2" (expand "has_countable_basis?") (("2" (split 1) (("1" (typepred "metric_induced_topology[T,d]") (("1" (expand "hausdorff_space?") (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "u!1") (("2" (skosimp) (("2" (inst + "v!1") (("2" (assert) (("2" (hide -1) (("2" (expand "metric_convergent?") (("2" (expand "cauchy?") (("2" (skosimp) (("2" (skosimp) (("2" (expand "metric_converges_to") (("2" (expand "ball") (("2" (expand "member") (("2" (inst - "r!1/2") (("2" (skosimp) (("2" (inst + "n!1") (("2" (skosimp) (("2" (inst-cp - "i!1") (("2" (inst - "j!1") (("2" (assert) (("2" (lemma "metric_triangle" ("x" "v!1(j!1)" "y" "x!1" "z" "v!1(i!1)")) (("2" (rewrite "metric_symmetric" -4) (("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) ((cauchy_subseq_is_totally_bounded formula-decl nil metric_space nil) (cauchy? const-decl "bool" metric_space_def nil) (ball const-decl "set[T]" metric_space_def nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (metric_symmetric formula-decl nil metric_space nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (metric_triangle formula-decl nil metric_space nil) (totally_bounded_is_separable formula-decl nil metric_space nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (d formal-const-decl "metric" metric_space nil) (metric nonempty-type-eq-decl nil metric_def nil) (metric? const-decl "bool" metric_def nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil metric_space nil) (lindelof formula-decl nil lindelof "topology/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" metric_space nil) (metric_space_is_hausdorff name-judgement "hausdorff" metric_space nil) (second_countable? const-decl "bool" topology_def "topology/") (compact_subset? const-decl "bool" topology_prelim "topology/") (nonempty? const-decl "bool" sets nil) (difference const-decl "set" sets nil) (fullset const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (metric_convergent? const-decl "bool" metric_space_def nil) (open_cover? const-decl "bool" topology_prelim "topology/") (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (metric_open? const-decl "bool" metric_space_def nil) (j!1 skolem-const-decl "nat" metric_space nil) (i!2 skolem-const-decl "nat" metric_space nil) (a!1 skolem-const-decl "({y: set[T] | EXISTS (x: ({i | i <= i!2})): y = YS!1(x)})" metric_space nil) (x!3 skolem-const-decl "({i | i <= i!2})" metric_space nil) (WW skolem-const-decl "[nat -> set[T]]" metric_space nil) (subseq? const-decl "bool" subseq "topology/") (NOT const-decl "[bool -> bool]" booleans nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (Union const-decl "set" sets nil) (YS!1 skolem-const-decl "sequence[set[T]]" metric_space nil) (i!1 skolem-const-decl "nat" metric_space nil) (image const-decl "set[R]" function_image nil) (subseq_index formula-decl nil subseq "topology/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (ball_is_metric_open application-judgement "metric_open" metric_space nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (metric_converges_to const-decl "bool" metric_space_def 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) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/") (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (metric_open_def formula-decl nil metric_space nil) (union_empty formula-decl nil sets_lemmas nil) (open nonempty-type-eq-decl nil topology "topology/") (open? const-decl "bool" topology "topology/") (union_is_open judgement-tcc nil topology "topology/") (union const-decl "set" sets nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" metric_space nil) (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" metric_space nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (ball_centre formula-decl nil metric_space nil) (IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/") (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (cover? const-decl "bool" topology_prelim "topology/") (XX skolem-const-decl "[n: nat -> ({x: T | difference(fullset[T], WW(n))(x)})]" metric_space nil) (choose const-decl "(p)" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (injective? const-decl "bool" functions nil) (finite_image judgement-tcc nil function_image_aux nil) (n!1 skolem-const-decl "nat" metric_space nil) (n!2 skolem-const-decl "nat" metric_space nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_subset formula-decl nil finite_sets nil) (VV skolem-const-decl "[set[T] -> boolean]" metric_space nil) (a!1 skolem-const-decl "({y: set[T] | EXISTS (x: ({i | i <= n!1})): y = YS!1(x)})" metric_space nil) (V!1 skolem-const-decl "setofsets[T]" metric_space nil) (finite_cover? const-decl "bool" topology_prelim "topology/") (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/") (sequence type-eq-decl nil sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (Union_IUnion formula-decl nil countable_indexed_sets "sets_aux/") (subcover? const-decl "bool" topology_prelim "topology/") (compact? const-decl "bool" topology "topology/") (separable_has_countable_basis formula-decl nil metric_space nil) (hausdorff? const-decl "bool" topology_prelim "topology/") (hausdorff_space? const-decl "bool" topology_prelim "topology/") (has_countable_basis? const-decl "bool" topology_def "topology/") (weierstrass_bolzano? const-decl "bool" metric_space nil) (fullset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" metric_space nil) (compact_is_weierstrass_bolzano formula-decl nil metric_space nil)) shostak)) (totally_bounded_iff_cauchy_subseq 0 (totally_bounded_iff_cauchy_subseq-1 nil 3406536093 ("" (split) (("1" (flatten) (("1" (skosimp) (("1" (lemma "totally_bounded_is_separable") (("1" (assert) (("1" (expand "fullset") (("1" (expand "totally_bounded?") (("1" (expand "separable?") (("1" (skosimp) (("1" (hide -1) (("1" (case "FORALL (r:posreal,S): EXISTS (X: set[T]): epsilon_net?(S, X, r)") (("1" (hide -4) (("1" (name "seq_in" "lambda u,S: forall (n:nat): S(u(n))") (("1" (case "forall (SS:setofsets[T],u): is_finite(SS) & seq_in(u,Union(SS)) => exists v,S: (("1" (name "CENTRES" "LAMBDA (n: nat, S): choose[set[T]]({X: set[T] | epsilon_net?(S, X, 1 / (n + 2))})") (("1" (case "FORALL (n: nat, S): is_finite(CENTRES(n, S)) & subset?(CENTRES(n, S), S)") (("1" (name "BALLS" "LAMBDA (n: nat, S): image[T,set[T]](lambda (x:T): ball(x,1/(2+n)),CENTRES(n,S))") (("1" (hide -3) (("1" (case "FORALL (n: nat, S): is_finite(BALLS(n, S)) & subset?(S,Union(BALLS(n, S)))") (("1" (hide -2) (("1" (name "SELECT_BALL_SUBSEQ" "lambda (n:nat,S:set[T],u:(lambda u: seq_in(u,S))): choose[[sequence[T],set[T]]]({vx (("1" (case "forall (n: nat, S,u): seq_in(u, S)=>BALLS(n, S)(SELECT_BALL_SUBSEQ(n,S,u)`2)&subseq?(SELECT_BALL_SUBSEQ(n,S,u)`1, u)&&nbs (("1" (name "GG" "lambda (n:nat,S:set[T],u:(LAMBDA u: seq_in(u, S))): let (v,b)= SELECT_BALL_SUBSEQ(n,S, (("1" (name "F" "lambda (n:nat): iterate(GG,n)(0,fullset[T],u!1)") (("1" (case "FORALL (n: nat, S, u): seq_in(u, S) => GG(n, S, u)`1 = n + 1 & BALLS(n, S)(GG(n, S, u)`2) & seq_in(GG(n, S, u)`3, GG(n, S, u)`2) & subseq?(GG(n, S, u)`3, u)") (("1" (name "AA" "lambda (n:nat): F(n)`2") (("1" (name "US" "lambda (n:nat): F(n)`3") (("1" (case "forall (n:nat): F(n+1) = GG(F(n))") (("1" (case "forall (n:nat): F(n)`1=n") (("1" (case "AA(0) = fullset[T] & US(0) = u!1 & seq_in(US(0), AA(0))") (("1" (case "FORALL (n: nat): BALLS(n, AA(n))(AA(n + 1)) & seq_in(US(n + 1), AA(n + 1)) & subseq?(US(n + 1), US(n))") (("1" (case "forall (n,i:nat): seq_in(US(n+i),AA(n))") (("1" (hide -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19) (("1" (name "EXTRACT" "lambda (u:sequence[T],v:(LAMBDA v: subseq?(v,u))): choose[[nat->nat]]({f:[nat->nat] | s (("1" (case "forall (n:nat): strict_increasing?(EXTRACT(US(n),US(n+1)))") (("1" (case "forall (n,i:nat): US(n + 1)(i) = US(n)(EXTRACT(US(n), US(n + 1))(i))") (("1" (name "EE" "LAMBDA (n:nat,f:{f:[nat->nat] | strict_increasing?(f)}): (n + 1, f o EXTRACT(US(n), US(n + 1 (("1" (name "E" "lambda (n:nat): iterate(EE,n)(0,lambda (n:nat):n)") (("1" (case "forall (n:nat): E(n)`1=n") (("1" (case "forall (n:nat): E(n+1)`2=E(n)`2 o EXTRACT(US(n), US(n + 1))") (("1" (name "H" "lambda (n:nat): E(n)`2") (("1" (case "H(0)=lambda (n:nat):n") (("1" (case "forall (n:nat): H(n+1)=H(n) o EXTRACT(US(n), US(n + 1))") (("1" (case "forall (n:nat): US(n) = u!1 o H(n)") (("1" (case "forall (n:nat): strict_increasing?(H(n))") (("1" (name "FF" "lambda (n:nat): H(n)(n)") (("1" (case "strict_increasing?(FF)") (("1" (name "U" "lambda (n:nat): US(n)(n)") (("1" (case "forall (n:nat): U(n) = u!1(FF(n))") (("1" (case "subseq?(U,u!1)") (("1" (case "cauchy?(U)") (("1" (inst + "U") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "cauchy?") (("2" (skosimp) (("2" (expand "member") (("2" (lemma "archimedean" ("px" "r!1/2")) (("2" (skosimp) (("2" (inst + "n!1+2") (("2" (skosimp) (("2" (inst -22 "n!1") (("2" (flatten) (("2" (inst-cp -21 "n!1+1" "i!1-(n!1+1)") (("1" (inst -21 "n!1+1" "j!1-(n!1+1)") (("1" (assert) (("1" (hide-all-but (-1 -2 -3 -21 -22 -23 1)) (("1" (expand "BALLS") (("1" (expand "image") (("1" (skosimp) (("1" (replace -6) (("1" (hide -6) (("1" (expand "seq_in") (("1" (expand "U") (("1" (inst -4 "j!1") (("1" (inst -5 "i!1") (("1" (expand "ball") (("1" (typepred "d") (("1" (expand "metric?") (("1" (flatten) (("1" (expand "metric_symmetric?") (("1" (inst - "x!1" "US(j!1)(j!1)") (("1" (expand "metric_triangle?") (("1" (inst - "US(j!1)(j!1)" "x!1" "US(i!1)(i!1)") (("1" (assert) (("1" (replace -2) (("1" (case "1 / (2 + n!1)+1 / (2 + n!1)<r!1") (("1" (assert) nil nil) ("2" (hide-all-but (-4 1)) (("2" (assert) (("2" (rewrite "div_mult_pos_lt1" -1) (("2" (lemma "div_mult_pos_lt1" ("py" "2+n!1" "z" "2" "x" "r!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)) --> -------------------- --> maximum size reached --> --------------------
¤ 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.0.688Bemerkung: (vorverarbeitet am 2026-04-26) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26