| 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 262 kB |
|
Quelle real_topology.prfSprache: Lisp |
|||||||||||||||
|
(real_topology (IMP_metric_space_TCC1 0 (IMP_metric_space_TCC1-1 nil 3387600277 ("" (expand "metric?") (("" (expand "metric_zero?") (("" (expand "metric_symmetric?") (("" (expand "metric_triangle?") (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (metric_zero? const-decl "bool" metric_def nil) (metric_triangle? const-decl "bool" metric_def nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (metric_symmetric? const-decl "bool" metric_def nil) (metric? const-decl "bool" metric_def nil)) nil)) (interval_TCC1 0 (interval_TCC1-1 nil 3454134699 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (set type-eq-decl nil sets nil) (interval? const-decl "bool" real_topology 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[T]" countable_setofsets "sets_aux/") (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" real_topology nil) (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology nil)) nil)) (bounded_interval_TCC1 0 (bounded_interval_TCC1-1 nil 3454134699 ("" (subtype-tcc) nil nil) ((set type-eq-decl nil sets 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (emptyset const-decl "set" sets nil) (interval? const-decl "bool" real_topology nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (upper_bound const-decl "bool" bound_defs "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (bounded? const-decl "bool" real_topology nil) (bounded_interval? const-decl "bool" real_topology 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_compact name-judgement "compact[T, (metric_induced_topology)]" real_topology nil) (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology nil)) nil)) (unbounded_interval_TCC1 0 (unbounded_interval_TCC1-1 nil 3454134699 ("" (expand "fullset") (("" (expand "unbounded_interval?") (("" (split) (("1" (grind) nil nil) ("2" (expand "unbounded?") (("2" (expand "bounded?") (("2" (expand "nonempty?") (("2" (split) (("1" (expand "empty?") (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (expand "above_bounded") (("2" (skosimp) (("2" (expand "upper_bound") (("2" (inst - "n!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((unbounded_interval? const-decl "bool" real_topology nil) (unbounded? const-decl "bool" real_topology nil) (nonempty? const-decl "bool" sets nil) (above_bounded const-decl "bool" bounded_reals "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (TRUE const-decl "bool" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets 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) (bounded? const-decl "bool" real_topology nil) (interval? const-decl "bool" real_topology nil) (fullset const-decl "set" sets nil)) nil)) (bounded_open_interval_TCC1 0 (bounded_open_interval_TCC1-1 nil 3454134699 ("" (expand "bounded_open_interval?") (("" (split) (("1" (grind) nil nil) ("2" (lemma "open_emptyset") (("2" (rewrite "metric_open_def") nil nil)) nil)) nil)) nil) ((set type-eq-decl nil sets 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (emptyset const-decl "set" sets nil) (interval? const-decl "bool" real_topology nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (upper_bound const-decl "bool" bound_defs "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (bounded? const-decl "bool" real_topology nil) (bounded_interval? const-decl "bool" real_topology nil) (real_minus_real_is_real application-judgement "real" reals nil) (metric_open_def formula-decl nil metric_space nil) (open_emptyset formula-decl nil topology "topology/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (bounded_open_interval? const-decl "bool" real_topology nil) (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology nil) (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" real_topology 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)) nil)) (open_interval_TCC1 0 (open_interval_TCC1-1 nil 3387600277 ("" (inst + "ball(0,1)") (("" (inst + "0" "1") nil nil)) nil) ((ball const-decl "set[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (open_interval_is_bounded_open_interval 0 (open_interval_is_bounded_open_interval-1 nil 3454134699 ("" (skolem + "X!1") (("" (typepred "X!1") (("" (skosimp) (("" (replace -1) (("" (hide -1) (("" (expand "bounded_open_interval?") (("" (expand "bounded_interval?") (("" (split) (("1" (grind) nil nil) ("2" (expand "bounded?") (("2" (flatten) (("2" (hide 1) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "above_bounded") (("2" (inst + "x!1+r!1") (("2" (grind) nil nil)) nil)) nil) ("3" (expand "below_bounded") (("3" (inst + "x!1-r!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "metric_open_ball") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((open_interval nonempty-type-eq-decl nil real_topology nil) (ball const-decl "set[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (set 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (bounded_open_interval? const-decl "bool" real_topology nil) (minus_real_is_real application-judgement "real" reals 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) (interval? const-decl "bool" real_topology nil) (real_minus_real_is_real application-judgement "real" reals nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (upper_bound const-decl "bool" bound_defs "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (bounded? const-decl "bool" real_topology nil) (metric_open_ball formula-decl nil metric_space nil) (bounded_interval? const-decl "bool" real_topology nil)) nil)) (open_basis 0 (open_basis-1 nil 3389861684 ("" (expand "base?") (("" (split) (("1" (expand "subset?") (("1" (skosimp*) (("1" (expand "fullset") (("1" (expand "metric_induced_topology") (("1" (expand "extend") (("1" (expand "member") (("1" (prop) (("1" (skosimp) (("1" (replace -1) (("1" (expand "metric_open?") (("1" (skosimp) (("1" (case-replace "ball(x!2, r!1)(x!3)") (("1" (assert) (("1" (expand "ball") (("1" (hide -2) (("1" (inst + "r!1-abs(x!2-x!3)") (("1" (expand "subset?") (("1" (skosimp) (("1" (expand "member") (("1" (lemma "triangle") (("1" (inst - "x!2-x!3" "x!3-x!4") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (hide -1) (("2" (skosimp) (("2" (expand "subset?") (("2" (expand "member") (("2" (inst - "x!3") (("2" (lemma "ball_centre" ("x" "x!3" "r" "r!2")) (("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" (skosimp) (("2" (typepred "A!1") (("2" (expand "extend") (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "fullset") (("2" (expand "metric_induced_topology") (("2" (expand "metric_open?") (("2" (name "VV" "{X:set[real]| EXISTS (x:real,r:posreal): X=ball(x,r) & subset?[real](X,A!1)}") (("2" (inst + "VV") (("2" (split) (("1" (skosimp) (("1" (hide -2) (("1" (prop) (("1" (expand "VV") (("1" (skosimp) (("1" (inst + "x!2" "r!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide -1) (("2" (expand "Union") (("2" (inst - "x!1") (("2" (case-replace "A!1(x!1)") (("1" (assert) (("1" (skosimp) (("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" (expand "VV") (("2" (replace -2) (("2" (inst + "x!1" "r!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "VV") (("2" (skosimp) (("2" (expand "subset?") (("2" (inst - "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) ((metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (member const-decl "bool" sets nil) (metric_open? const-decl "bool" metric_space_def nil) (real_minus_real_is_real application-judgement "real" reals 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) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (ball const-decl "set[T]" metric_space_def 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) (r!1 skolem-const-decl "posreal" real_topology nil) (x!2 skolem-const-decl "real" real_topology nil) (x!3 skolem-const-decl "real" real_topology nil) (triangle formula-decl nil real_props 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_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ball_centre formula-decl nil metric_space nil) (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (r!1 skolem-const-decl "posreal" real_topology nil) (x!1 skolem-const-decl "real" real_topology nil) (VV skolem-const-decl "[set[real] -> boolean]" real_topology nil) (= const-decl "[T, T -> boolean]" equalities nil) (base? const-decl "bool" basis "topology/")) shostak)) (rational_open_interval_TCC1 0 (rational_open_interval_TCC1-1 nil 3387600277 ("" (inst + "ball(0,1)") (("" (inst + "0" "1") nil nil)) nil) ((ball const-decl "set[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (posrat nonempty-type-eq-decl nil rationals nil) (> const-decl "bool" reals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (>= const-decl "bool" reals nil) (rational nonempty-type-from-decl nil rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (rational_basis 0 (rational_basis-1 nil 3387602054 ("" (lemma "open_basis") (("" (expand "extend") (("" (expand "base?") (("" (flatten) (("" (split) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) (("1" (prop) (("1" (skosimp) (("1" (inst -3 "x!1") (("1" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (inst + "q!1" "pq!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "A!1") (("2" (skosimp) (("2" (inst + "{X:set[real] | EXISTS q, pq: X = ball(q, pq) & subset?[real](X,A!1)}") (("2" (split) (("1" (expand "subset?") (("1" (skosimp) (("1" (expand "member") (("1" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "q!1" "pq!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "Union") (("2" (case-replace "A!1(x!1)") (("1" (replace -4 -1 rl) (("1" (assert) (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "subset?" -4) (("1" (expand "member") (("1" (inst -4 "a!1") (("1" (assert) (("1" (prop) (("1" (skosimp) (("1" (hide -5) (("1" (replace -1 -4) (("1" (expand "ball" -4) (("1" (name "AA" "ball(x!1,r!1-abs(x!2-x!1))") (("1" (case "subset?[real](AA,a!1)") (("1" (name-replace "R" "r!1 - abs(x!2 - x!1)") (("1" (case "R>0") (("1" (lemma "density" ("x" "x!1-R/8" "y" "x!1+R/8")) (("1" (assert) (("1" (skolem - ("q!1")) (("1" (flatten) (("1" (lemma "density" ("x" "R/4" "y" "R/2")) (("1" (assert) (("1" (skosimp) (("1" (case "ball(q!1,r!2)(x!1)") (("1" (case "subset?[real](ball(q!1, r!2),AA)") (("1" (inst + "ball(q!1, r!2)") (("1" (inst + "q!1" "r!2") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp) (("1" (replace -15 1 rl) (("1" (assert) (("1" (hide -15) (("1" (inst - "x!3") (("1" (assert) (("1" (inst - "x!3") (("1" (inst + "a!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide -13 2) (("2" (expand "AA") (("2" (expand "R") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (grind) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "R") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "AA") (("2" (expand "ball") (("2" (replace -3) (("2" (assert) (("2" (lemma "triangle") (("2" (inst - "x!2-x!1" "x!1-x!3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (expand "subset?") (("2" (inst - "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) ((extend const-decl "R" extend nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (R skolem-const-decl "real" real_topology nil) (minus_real_is_real application-judgement "real" reals nil) (AA skolem-const-decl "set[real]" real_topology nil) (r!2 skolem-const-decl "rat" real_topology nil) (q!1 skolem-const-decl "rat" real_topology nil) (A!1 skolem-const-decl "(metric_induced_topology)" real_topology 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) (density formula-decl nil rational_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (triangle formula-decl nil 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) (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) (NOT const-decl "[bool -> bool]" booleans nil) (metric_space_is_hausdorff name-judgement "hausdorff" real_topology nil) (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union const-decl "set" sets nil) (ball const-decl "set[T]" metric_space_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (setofsets type-eq-decl nil sets nil) (subset? const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (posrat nonempty-type-eq-decl nil rationals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (rational nonempty-type-from-decl nil rationals 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) (rat nonempty-type-eq-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (member const-decl "bool" sets nil) (base? const-decl "bool" basis "topology/") (open_basis formula-decl nil real_topology nil)) shostak)) (countable_rational_open_interval 0 (countable_rational_open_interval-1 nil 3389931575 ("" (lemma "is_countable_cross" ("X" "fullset[rat]" "Y" "fullset[posrat]")) (("" (lemma "nat_posrat") (("" (lemma "nat_rational") (("" (split) (("1" (hide -2 -3) (("1" (expand "fullset") (("1" (expand "cross_product") (("1" (expand "is_countable") (("1" (skosimp) (("1" (typepred "f!1") (("1" (name "F" "lambda (r:rat,pq:posrat): ball(r,pq)") (("1" (case "bijective?[[rat, posrat],rational_open_interval](F)") (("1" (lemma "bij_inv_is_bij[[rat, posrat], rational_open_interval]" ("f" "F")) (("1" (split) (("1" (assert) (("1" (inst + "f!1 o inverse[[rat, posrat], rational_open_interval](F)") (("1" (expand "bijective?") (("1" (flatten) (("1" (hide-all-but (-1 -6 1)) (("1" (expand "o") (("1" (expand "injective?") (("1" (skosimp) (("1" (inst -3 "inverse[[rat, posrat], rational_open_interval](F)(x1!1)" "inverse[[rat, posrat], rational_open_interval](F)(x2!1)") (("1" (assert) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "bijective?") (("2" (split) (("1" (expand "injective?") (("1" (skosimp*) (("1" (expand "F") (("1" (rewrite "extensionality_postulate" -1 :dir rl) (("1" (lemma "trich_lt" ("x" "x1!1`1" "y" "x2!1`1")) (("1" (split) (("1" (lemma "trich_lt" ("x" "x1!1`2" "y" "x2!1`2")) (("1" (split) (("1" (inst - "max(x1!1`1+x1!1`2,x2!1`1)") (("1" (expand "ball") (("1" (grind) nil nil)) nil)) nil) ("2" (inst - "max(x1!1`1+x1!1`2,x2!1`1)") (("2" (expand "ball") (("2" (grind) nil nil)) nil)) nil) ("3" (expand "ball") (("3" (inst - "min(x1!1`1-x2!1`2,x1!1`1)") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "trich_lt" ("x" "x1!1`2" "y" "x2!1`2")) (("2" (split) (("1" (inst - "x1!1`1+x1!1`2") (("1" (expand "ball") (("1" (grind) nil nil)) nil)) nil) ("2" (decompose-equality) nil nil) ("3" (inst - "x1!1`1+x2!1`2") (("3" (expand "ball") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "trich_lt" ("x" "x1!1`2" "y" "x2!1`2")) (("3" (split) (("1" (inst - "min(x2!1`1-x1!1`2,x2!1`1)") (("1" (expand "ball") (("1" (grind) nil nil)) nil)) nil) ("2" (inst - "min(x1!1`1-x1!1`2,x2!1`1)") (("2" (expand "ball") (("2" (grind) nil nil)) nil)) nil) ("3" (inst - "max(x1!1`1+x2!1`2,x1!1`1)") (("3" (expand "ball") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp) (("2" (typepred "y!1") (("2" (skosimp) (("2" (inst + "(q!1, pq!1)") (("2" (expand "F") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst + "x1!1`1" "x1!1`2") (("3" (expand "F") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (expand "fullset") (("2" (expand "is_countable") (("2" (expand "is_countably_infinite_type") (("2" (skosimp) (("2" (inst + "f!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (expand "fullset") (("3" (expand "is_countably_infinite_type") (("3" (expand "is_countable") (("3" (skosimp) (("3" (inst + "f!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat_posrat formula-decl nil countable_types "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (NOT const-decl "[bool -> bool]" booleans nil) (TRUE const-decl "bool" booleans nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (injective? const-decl "bool" functions nil) (rational_open_interval nonempty-type-eq-decl nil real_topology nil) (bijective? const-decl "bool" functions nil) (inverse const-decl "D" function_inverse nil) (O const-decl "T3" function_props nil) (f!1 skolem-const-decl "(injective?[({z | TRUE}), nat])" real_topology nil) (F skolem-const-decl "[[rat, posrat] -> set[real]]" real_topology nil) (bij_inv_is_bij formula-decl nil function_inverse nil) (surjective? const-decl "bool" functions nil) (trich_lt formula-decl nil real_props nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (rat_min application-judgement "{s: rat | s <= q AND s <= r}" real_defs nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_abs_is_nonneg application-judgement "{r: nonneg_rat | r >= q}" real_defs nil) (minus_rat_is_rat application-judgement "rat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (extensionality_postulate formula-decl nil functions nil) (ball const-decl "set[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (cross_product const-decl "set[[T1, T2]]" cross_product "topology/") (is_countably_infinite_type const-decl "bool" countability "sets_aux/") (nat_rational formula-decl nil countable_types "sets_aux/") (is_countable_cross formula-decl nil countable_cross nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (rational nonempty-type-from-decl nil rationals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (> const-decl "bool" reals nil) (posrat nonempty-type-eq-decl nil rationals nil)) shostak)) (metric_induced_topology_is_second_countable 0 (metric_induced_topology_is_second_countable-1 nil 3387600277 ("" (expand "second_countable?") (("" (typepred "metric_induced_topology [real, (LAMBDA (x, y: real): abs(x - y))]") (("" (expand "hausdorff_space?") (("" (assert) (("" (expand "has_countable_basis?") (("" (lemma "rational_basis") (("" (lemma "base_is_synthetic_base" ("t" "metric_induced_topology" "U" "fullset[rational_open_interval]")) (("" (assert) (("" (inst + "fullset[rational_open_interval]") (("" (replace -1) (("" (hide -1 -2 -3) (("" (split) (("1" (case "is_countable(fullset[rat])") (("1" (lemma "countable_subset[rat]" ("S" "fullset[posrat]" "Count" "fullset[rat]")) (("1" (split) (("1" (lemma "is_countable_cross[rat,posrat]" ("X" "fullset[rat]" "Y" "fullset[posrat]")) (("1" (assert) (("1" (split) (("1" (hide -2 -3 -4) (("1" (name "F" "lambda (q:rat,pq:posrat): ball(q,pq)") (("1" (case "bijective?[(cross_product(fullset[rat], fullset[posrat])),rational_open_interval (("1" (case "bijective?[[rat, posrat],rational_open_interval](F)") (("1" (hide -2) (("1" (lemma "bijective_inverse_is_bijective[[rat, posrat], rational_open_interval]" ("f" "F")) (("1" (expand "is_countable") (("1" (skosimp) (("1" (inst + "lambda (x:rational_open_interval): f!1(inverse[[rat,posrat],rational_open_interva (("1" (typepred "f!1") (("1" (expand "bijective?") (("1" (flatten) (("1" (hide -3 -4 -5 -6) (("1" (expand "injective?") (("1" (skosimp) (("1" (inst - "inverse[[rat, posrat], rational_open_interval](F)(x1!1)" "inverse[[rat, posrat], rational_open_interval](F)(x2!1)") (("1" (assert) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (prop) (("1" (expand "fullset") (("1" (expand "extend") (("1" (prop) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (expand "extend") (("2" (prop) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "fullset") (("3" (expand "cross_product") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "restrict") (("2" (expand "bijective?") (("2" (flatten) (("2" (split) (("1" (hide -2) (("1" (expand "injective?") (("1" (skosimp) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil) ("2" (expand "fullset") (("2" (expand "cross_product") (("2" (propax) nil nil)) nil)) nil) ("3" (expand "fullset") (("3" (expand "cross_product") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "surjective?") (("2" (skosimp) (("2" (inst - "y!1") (("2" (skosimp) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -2 1 rl) (("3" (skosimp) (("3" (inst + "x1!1`1" "x1!1`2") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (expand "bijective?") (("2" (expand "restrict") (("2" (split) (("1" (expand "injective?") (("1" (skosimp) (("1" (expand "F") (("1" (rewrite "extensionality_postulate" -1 :dir rl) (("1" (case-replace "x2!1`1=x1!1`1") (("1" (case-replace "x2!1`2=x1!1`2") (("1" (decompose-equality) nil nil) ("2" (case "x2!1`2 > x1!1`2") (("1" (inst - "x1!1`1-x1!1`2") (("1" (expand "ball") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (inst - "x1!1`1-x2!1`2") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (case-replace "x2!1`2=x1!1`2") (("1" (case "x2!1`1>x1!1`1") (("1" (inst - "max(x1!1`1+x1!1`2,x2!1`1)") (("1" (grind) nil nil)) nil) ("2" (inst - "max(x2!1`1+x1!1`2,x1!1`1)") (("2" (grind) nil nil)) nil)) nil) ("2" (case "x2!1`2>x1!1`2") (("1" (case "x2!1`1>x1!1`1") (("1" (inst - "max(x1!1`1+x2!1`2,x2!1`1)") (("1" (grind) nil nil)) nil) ("2" (inst - "x2!1`1-x1!1`2") (("2" (grind) nil nil)) nil)) nil) ("2" (case "x2!1`1>x1!1`1") (("1" (inst - "x1!1`1-x2!1`2") (("1" (grind) nil nil)) nil) ("2" (inst - "x1!1`1+x2!1`2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "F") (("2" (expand "surjective?") (("2" (skosimp) (("2" (typepred "y!1") (("2" (skosimp) (("2" (inst + "(q!1,pq!1)") (("1" (assert) nil nil) ("2" (expand "cross_product") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst + "x1!1`1" "x1!1`2") (("3" (expand "F") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2 -3) (("2" (expand "fullset") (("2" (expand "extend") (("2" (expand "is_countable") (("2" (skosimp) (("2" (inst + "f!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "nat_rational") (("2" (expand "is_countably_infinite_type") (("2" (expand "fullset") (("2" (expand "is_countable") (("2" (skosimp) (("2" (inst + "f!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "metric_induced_topology") (("2" (case-replace "metric_open?(x!1)") (("1" (expand "fullset") (("1" (expand "extend") (("1" (expand "synthetic_generated_topology_set") (("1" (lemma "rational_basis") (("1" (expand "base?") (("1" (flatten) (("1" (inst - "x!1") (("1" (skosimp) (("1" (inst + "V!1") (("1" (expand "fullset") (("1" (expand "extend") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "metric_induced_topology") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (expand "extend") (("2" (expand "synthetic_generated_topology_set") (("2" (assert) (("2" (skosimp) (("2" (replace -2 * rl) (("2" (rewrite "metric_open_def") (("2" (lemma "open_Union" ("Y" "V!1")) (("2" (assert) (("2" (expand "every") (("2" (skosimp) (("2" (typepred "x!2") (("2" (expand "subset?") (("2" (expand "member") (("2" (inst - "x!2") (("2" (assert) (("2" (prop) (("2" (skosimp) (("2" (replace -1) (("2" (rewrite "metric_open_def" 1 :dir rl) (("2" (rewrite "metric_open_ball") 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) ((hausdorff_space? const-decl "bool" topology_prelim "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (hausdorff? const-decl "bool" topology_prelim "topology/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (rational_basis formula-decl nil real_topology nil) (is_countably_infinite_type const-decl "bool" countability "sets_aux/") (nat_rational formula-decl nil countable_types "sets_aux/") (countable_subset formula-decl nil countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (is_countable_cross formula-decl nil countable_cross nil) (extensionality_postulate formula-decl nil functions nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (minus_rat_is_rat application-judgement "rat" rationals nil) (rat_abs_is_nonneg application-judgement "{r: nonneg_rat | r >= q}" real_defs nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (q!1 skolem-const-decl "rat" real_topology nil) (pq!1 skolem-const-decl "posrat" real_topology nil) (bijective_inverse_is_bijective judgement-tcc nil function_inverse nil) (f!1 skolem-const-decl "(injective?[(cross_product(fullset[rat], fullset[posrat])), nat])" real_topology nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (F skolem-const-decl "[[rat, posrat] -> set[real]]" real_topology nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (injective? const-decl "bool" functions nil) (inverse const-decl "D" function_inverse nil) (surjective? const-decl "bool" functions nil) (x2!1 skolem-const-decl "[rat, posrat]" real_topology nil) (x1!1 skolem-const-decl "[rat, posrat]" real_topology nil) (restrict const-decl "R" restrict nil) (bijective? const-decl "bool" functions nil) (cross_product const-decl "set[[T1, T2]]" cross_product "topology/") (restrict_of_inj_is_inj application-judgement "(injective?[S, R])" restrict nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (TRUE const-decl "bool" booleans nil) (is_countable const-decl "bool" countability "sets_aux/") (Union const-decl "set" sets 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/") (base? const-decl "bool" basis "topology/") (x!1 skolem-const-decl "[real -> boolean]" real_topology nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (metric_open? const-decl "bool" metric_space_def nil) (synthetic_generated_topology_set const-decl "setofsets[T]" basis "topology/") (synthetic_base type-eq-decl nil basis "topology/") (synthetic_base? const-decl "bool" basis "topology/") (base_is_synthetic_base formula-decl nil basis "topology/") (set type-eq-decl nil sets nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (rational nonempty-type-from-decl nil rationals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (> const-decl "bool" reals nil) (posrat nonempty-type-eq-decl nil rationals nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal nonempty-type-eq-decl nil real_types nil) (ball const-decl "set[T]" metric_space_def nil) (rational_open_interval nonempty-type-eq-decl nil real_topology nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (topology? const-decl "bool" topology_prelim "topology/") (topology nonempty-type-eq-decl nil topology_prelim "topology/") (has_countable_basis? const-decl "bool" topology_def "topology/") (second_countable? const-decl "bool" topology_def "topology/") (metric_space_is_hausdorff name-judgement "hausdorff" real_topology nil) (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology nil)) nil)) (real_is_complete 0 (real_is_complete-1 nil 3397565960 ("" (expand "complete_metric_space?") (("" (split) (("1" (grind) nil nil) ("2" (expand "fullset") (("2" (expand "metric_complete?") (("2" (skosimp) (("2" (case "forall (u:sequence[real]): (exists (a:real): forall (i:nat): u(i) <= a) & (forall (("1" (case "forall (X:set[real]): is_finite(X) & nonempty?(X) => exists (a:(X)): forall (x:( (("1" (copy -3) (("1" (expand "cauchy?" -1) (("1" (inst - "1") (("1" (expand "ball") (("1" (expand "member") (("1" (skosimp) (("1" (case "forall (n:nat): nonempty?(image(u!1,{m:nat | m>=n}))") (("1" (case "forall (n:nat):bounded_real_defs. bounded?(image(u!1,{m:nat | m>=n}))") (("1" (name "V" "LAMBDA (n: nat): bounded_real_defs.lub(image(u!1, {m: nat | m >= n}))") (("1" (case "FORALL (i, j: nat): i <= j => V(i) >= V(j)") (("1" (case "metric_convergent?({x: real | TRUE}, V)") (("1" (hide -8 -7) (("1" (expand "metric_convergent?") (("1" (skosimp) (("1" (inst + "x!1") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst - "r!1/3") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (hide -6) (("1" (expand "cauchy?") (("1" (inst -6 "r!1/3") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (case "FORALL (i: nat): i >= max(n!2, n!3) => abs(V(i)-u!1(i)) < 2 * r!1 / 3") (("1" (inst + "max(n!2, n!3)") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst - "i!1") (("1" (assert) (("1" (lemma "triangle" ("x" "x!1 - V(i!1)" "y" "V(i!1) - u!1(i!1)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "V" 1) (("2" (hide -4) (("2" (inst -4 "i!1") (("2" (inst -5 "i!1") (("2" (expand "bounded?") (("2" (flatten) (("2" (typepred "bounded_real_defs.lub(image(u!1, {m: nat | m >= i!1}))") (("2" (name-replace "LUB" "bounded_real_defs.lub(image(u!1, {m: nat | m >= i!1}))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?") (("2" (inst - "u!1(i!1)") (("1" (expand "abs" 1) (("1" (assert) (("1" (inst - "u!1(i!1)+r!1/3") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "image" -1) (("1" (skolem - ("M")) (("1" (typepred "M") (("1" (inst -10 "i!1" "M") (("1" (assert) (("1" (expand "abs" -10) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "image") (("2" (inst + "i!1") 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 -8 2) (("2" (inst -7 "lambda (i:nat): -V(i)") (("2" (hide -2) (("2" (split -6) (("1" (hide-all-but (-1 1)) (("1" (expand "metric_convergent?") (("1" (skosimp) (("1" (inst + "-x!1") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst - "r!1") (("1" (skosimp) (("1" (inst + "n!2") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (expand "ball") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst-cp -2 "0") (("2" (expand "bounded?" -3) (("2" (flatten) (("2" (expand "bounded_below?") (("2" (skosimp) (("2" (inst + "-x!1") (("2" (skosimp) (("2" (hide -3) (("2" (expand "lower_bound?") (("2" (expand "V" 1) (("2" (inst -2 "i!1") (("2" (inst -4 "i!1") (("2" (expand "bounded?") (("2" (flatten) (("2" (typepred "bounded_real_defs.lub(image(u!1, {m: nat | m >= i!1}))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?") (("2" (inst - "u!1(i!1)") (("1" (inst -6 "u!1(i!1)") (("1" (assert) nil nil) ("2" (expand "image") (("2" (inst + "i!1") nil nil)) nil)) nil) ("2" (expand "image") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst - "i!1" "j!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -6 2 -5) (("2" (skosimp) (("2" (hide -2) (("2" (inst-cp - "i!1") (("2" (inst - "j!1") (("2" (inst-cp - "i!1") (("2" (inst - "j!1") (("2" (expand "bounded?") (("2" (flatten) (("2" (expand "V") (("2" (typepred "bounded_real_defs.lub(image(u!1, {m: nat | m >= i!1}))") (("2" (typepred "bounded_real_defs.lub(image(u!1, {m: nat | m >= j!1}))") (("2" (name-replace "LUB_I" "bounded_real_defs.lub(image(u!1, {m: nat | m >= i!1}))") (("2" (name-replace "LUB_J" "bounded_real_defs.lub(image(u!1, {m: nat | m >= j!1}))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?") (("2" (hide-all-but (-2 -3 -5 1)) (("2" (inst - "LUB_I") (("2" (split -1) (("1" (assert) nil nil) ("2" (skosimp) (("2" (typepred "s!1") (("2" (expand "image") (("2" (skolem - "M") (("2" (typepred "M") (("2" (inst - "u!1(M)") (("1" (assert) nil nil) ("2" (expand "image") (("2" (inst + "M") (("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) ("2" (skosimp) (("2" (inst - "n!2") (("2" (inst - "n!2") (("2" (expand "bounded?") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -5 -4) (("2" (skosimp) (("2" (expand "bounded?") (("2" (split) (("1" (expand "bounded_above?") (("1" (inst -3 "image(u!1, {m: nat | m < n!1})") (("1" (case-replace "n!1=0") (("1" (inst + "u!1(0)+1") (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "image") (("1" (skosimp) (("1" (replace -1) (("1" (inst -4 "0" "x!1") (("1" (assert) (("1" (hide-all-but (-4 1)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!1>=1") (("1" (hide 1) (("1" (lemma "finite_image[nat,real]" ("f" "u!1" "S" "{m: nat | m < n!1}")) (("1" (replace -1) (("1" (split -5) (("1" (skosimp) (("1" (typepred "a!1") (("1" (inst + "max(a!1,u!1(n!1)+1)") (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "image" -1) (("1" (skolem - "j!1") (("1" (replace -1) (("1" (case "j!1<n!1") (("1" (inst -4 "u!1(j!1)") (("1" (expand "max") (("1" (case-replace "a!1 < 1 + u!1(n!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "image") (("2" (inst + "j!1") nil nil)) nil)) nil) ("2" (case "j!1>=n!1") (("1" (hide 1) (("1" (inst -8 "n!1" "j!1") (("1" (assert) (("1" (hide-all-but (-8 1)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "image") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "u!1(0)") (("2" (expand "member") (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "is_finite") (("2" (inst + "n!1" "lambda (x:{m: nat | m < n!1}): x") (("2" (expand "injective?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "bounded_below?") (("2" (case-replace "n!1=0") (("1" (hide -3) (("1" (inst + "-(1+abs(u!1(0)))") (("1" (expand "lower_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "image") (("1" (skolem - ("M")) (("1" (replace -1) (("1" (typepred "M") (("1" (inst - "M" "0") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n!1>=1") (("1" (hide 1) (("1" (inst -3 "image[nat,real](lambda (i:nat): -u!1(i),{m: nat | m < n!1})") (("1" (lemma "finite_image[nat,real]" ("f" "LAMBDA (i: nat): -u!1(i)" "S" "{m: nat | m < n!1}")) (("1" (replace -1) (("1" (split -4) (("1" (skosimp) (("1" (inst + "-max(a!1,abs(u!1(n!1))+1)") (("1" (expand "lower_bound?") (("1" (skosimp) (("1" (typepred "s!1") (("1" (expand "image") (("1" (hide -3) (("1" (skolem - ("M")) (("1" (replace -1) (("1" (typepred "M") (("1" (hide -2) (("1" (case "M>=n!1") (("1" (inst -5 "M" "n!1") (("1" (assert) (("1" (hide-all-but (-5 1)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (case "M<n!1") (("1" (hide 1) (("1" (inst - "-u!1(M)") (("1" (hide -5) (("1" (grind) nil nil)) nil) ("2" (expand "image") (("2" (inst + "M") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "image") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "-u!1(0)") (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "is_finite") (("2" (inst + "n!1" "lambda (x: {m: nat | m < n!1}): x") (("2" (expand "injective?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "image") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "u!1(n!2)") (("2" (expand "member") (("2" (inst + "n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "FORALL (n:posnat,X: set[real]): is_finite[real](X) & card[real](X)=n & nonempty?[real](X) => (EXISTS (a: (X)): FORALL (x: (X)): x <= a)") (("1" (skosimp) (("1" (inst - "card[real](X!1)" "X!1") (("1" (assert) nil nil) ("2" (rewrite "nonempty_card") nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (case-replace "j!1=0") (("1" (hide -1 -2 -3) (("1" (lemma "card_one[real]" ("S" "X!1")) (("1" (assert) (("1" (skosimp) (("1" (inst + "x!1") (("1" (skosimp) (("1" (typepred "x!2") (("1" (replace -2 -1) (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1 *) (("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1>=1") (("1" (assert) (("1" (hide 1) (("1" (lemma "card_rest[real]" ("S" "X!1")) (("1" (split -1) (("1" (replace -6) (("1" (assert) (("1" (inst - "rest[real](X!1)") (("1" (assert) (("1" (lemma "nonempty_card[real]" ("S" "rest[real](X!1)")) (("1" (assert) (("1" (rewrite "finite_rest[real]") (("1" (lemma "choose_rest[real]" ("a" "X!1")) (("1" (split) (("1" (skosimp) (("1" (inst + "max(choose[real](X!1),a!1)") (("1" (skosimp) (("1" (typepred "x!1") (("1" (replace -2 -1 rl) (("1" (hide -2) (("1" (expand "add" -1) (("1" (split -1) (("1" (expand "max") (("1" (replace -1) (("1" (lift-if 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (inst - "x!1") (("2" (expand "max") (("2" (lift-if 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "a!1") (("2" (lemma "choose_member[real]" ("a" "X!1")) (("2" (split -1) (("1" (expand "member") (("1" (expand "max") (("1" (replace -1) (("1" (expand "rest" -2) (("1" (expand "nonempty?") (("1" (assert) (("1" (expand "remove") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (skosimp) (("2" (lemma "lub_exists" ("SA" "image(u!2,fullset[nat])")) (("1" (skosimp) (("1" (expand "metric_convergent?") (("1" (inst + "x!1") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (case "EXISTS (n:nat): FORALL (i:nat): i >= n => x!1 - u!2(i) < r!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst - "u!2(i!1)") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst -2 "x!1-r!1") (("2" (assert) (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (replace -1) (("2" (inst + "x!2") (("2" (skosimp) (("2" (inst -5 "x!2" "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)) nil)) nil) ("2" (split 1) (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "u!2(0)") (("1" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (expand "image") (("2" (expand "bounded_above?") (("2" (inst + "a!1") (("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (inst - "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) ((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) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (metric_zero? const-decl "bool" metric_space_def nil) (metric_symmetric? const-decl "bool" metric_space_def nil) (metric_triangle? const-decl "bool" metric_space_def nil) (metric_space? const-decl "bool" metric_space_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (metric_complete? const-decl "bool" metric_space_def nil) (TRUE const-decl "bool" booleans nil) (metric_convergent? const-decl "bool" metric_space_def nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (choose_rest formula-decl nil sets_lemmas nil) (remove const-decl "set" sets nil) (choose_member formula-decl nil sets_lemmas nil) (add const-decl "(nonempty?)" sets nil) (x!1 skolem-const-decl "(X!1)" real_topology nil) (a!1 skolem-const-decl "(rest[real](X!1))" real_topology nil) (choose const-decl "(p)" sets nil) (finite_rest judgement-tcc nil finite_sets nil) (rest const-decl "set" sets nil) (card_rest formula-decl nil finite_sets nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (X!1 skolem-const-decl "set[real]" real_topology nil) (x!1 skolem-const-decl "real" real_topology nil) (singleton const-decl "(singleton?)" sets nil) (card_one formula-decl nil finite_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (nonempty_card formula-decl nil finite_sets nil) (X!1 skolem-const-decl "set[real]" real_topology nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (member const-decl "bool" sets nil) (image const-decl "set[R]" function_image nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (M skolem-const-decl "({m: nat | m >= n!2})" real_topology nil) (below type-eq-decl nil nat_types nil) (injective? const-decl "bool" functions nil) (empty? const-decl "bool" sets nil) (n!1 skolem-const-decl "nat" real_topology nil) (n!2 skolem-const-decl "nat" real_topology nil) (j!1 skolem-const-decl "({m: nat | m >= n!2})" real_topology nil) (finite_set type-eq-decl nil finite_sets nil) (finite_image judgement-tcc nil function_image_aux nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (M skolem-const-decl "({m: nat | m >= j!1})" real_topology nil) (j!1 skolem-const-decl "nat" real_topology nil) (i!1 skolem-const-decl "nat" real_topology nil) (V skolem-const-decl "[n: nat -> {x | least_upper_bound?(x, image(u!1, {m: nat | m >= n}))}]" real_topology nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "nat" real_topology nil) (u!1 skolem-const-decl "sequence[({x | TRUE})]" real_topology nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (triangle formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (metric_converges_to const-decl "bool" metric_space_def nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (i!1 skolem-const-decl "nat" real_topology nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (bounded? const-decl "bool" bounded_real_defs nil) (ball const-decl "set[T]" metric_space_def nil) (cauchy? const-decl "bool" metric_space_def nil) (nonempty? const-decl "bool" sets nil) (is_finite const-decl "bool" finite_sets nil) (lub_exists formula-decl nil bounded_real_defs nil) (u!2 skolem-const-decl "sequence[real]" real_topology nil) (i!1 skolem-const-decl "nat" real_topology nil) (complete_metric_space? const-decl "bool" metric_space_def nil) (fullset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology nil)) nil)) (closed_ball_TCC1 0 (closed_ball_TCC1-1 nil 3425709557 ("" (skosimp) (("" (case "open?({y| x!1+r!1<y})") (("1" (case "open?({y| y < x!1-r!1})") (("1" (lemma "open_union" ("U1" "{y | x!1 + r!1 < y}" "U2" "{y | y < x!1 - r!1}")) (("1" (rewrite "open_complement" 1 :dir rl) (("1" (case-replace "union({y | x!1 + r!1 < y}, {y | y < x!1 - r!1})=complement({y | abs(x!1 - y) <= r!1})") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "open?") (("2" (expand "member") (("2" (expand "metric_induced_topology") (("2" (expand "metric_open?") (("2" (skosimp) (("2" (split) (("1" (flatten) (("1" (inst + "x!1-(r!1+x!2)") (("1" (expand "ball") (("1" (grind) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "ball") (("2" (inst - "x!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "open?") (("2" (expand "member") (("2" (expand "metric_induced_topology") (("2" (expand "metric_open?") (("2" (skosimp) (("2" (split) (("1" (flatten) (("1" (inst + "x!2-(r!1+x!1)") (("1" (expand "subset?") (("1" (expand "ball") (("1" (expand "member") (("1" (skosimp) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "ball") (("2" (inst - "x!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "metric_induced_topology [real, (LAMBDA (x, y: real): abs(x - y))]") (("3" (expand "hausdorff_space?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (open? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (metric_space_is_hausdorff name-judgement "hausdorff" real_topology nil) (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology nil) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology nil) (real_plus_real_is_real application-judgement "real" reals nil) (metric_open? const-decl "bool" metric_space_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (r!1 skolem-const-decl "nnreal" real_topology nil) (x!2 skolem-const-decl "real" real_topology nil) (x!1 skolem-const-decl "real" real_topology nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (ball const-decl "set[T]" metric_space_def nil) (open_union formula-decl nil topology "topology/") (open nonempty-type-eq-decl nil topology "topology/") (complement const-decl "set" sets nil) (union const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_le_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) (member const-decl "bool" sets nil) (minus_real_is_real application-judgement "real" reals nil) (open_complement formula-decl nil topology "topology/") (<= const-decl "bool" reals nil) (x!2 skolem-const-decl "real" real_topology nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (closed_interval_TCC1 0 (closed_interval_TCC1-1 nil 3425709557 ("" (inst + "closed_ball(0,0)") (("" (inst + "0" "0") nil nil)) nil) ((closed_ball const-decl "closed" real_topology nil) (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (open_TCC1 0 (open_TCC1-1 nil 3425709557 ("" (skosimp) (("" (typepred "b!1") (("" (assert) nil nil)) nil)) 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_lt_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) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (open_TCC2 0 (open_TCC2-1 nil 3425709557 ("" (skosimp*) (("" (typepred "b!1") (("" (inst + "(a!1 + b!1) / 2" "(b!1 - a!1) / 2") nil nil)) nil)) 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (+ 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (closed_TCC1 0 (closed_TCC1-1 nil 3425709557 ("" (skosimp) (("" (typepred "b!1") (("" (assert) nil nil)) nil)) 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (closed_TCC2 0 (closed_TCC2-1 nil 3425709557 ("" (skosimp) (("" (typepred "b!1") (("" (inst + "(a!1 + b!1) / 2" "(b!1 - a!1) / 2") nil nil)) nil)) 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (open_inf_TCC1 0 (open_inf_TCC1-1 nil 3454134699 ("" (skosimp) (("" (rewrite "metric_open_def" + :dir rl) (("" (expand "metric_open?") (("" (skosimp) (("" (split) (("1" (flatten) (("1" (inst + "x!1-a!1") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (expand "member") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((metric_open_def formula-decl nil metric_space nil) (set type-eq-decl nil sets nil) (< const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_space_def nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (a!1 skolem-const-decl "real" real_topology nil) (x!1 skolem-const-decl "real" real_topology nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_open? const-decl "bool" metric_space_def nil)) nil)) (inf_open_TCC1 0 (inf_open_TCC1-1 nil 3454134699 ("" (skosimp) (("" (rewrite "metric_open_def" + :dir rl) (("" (expand "metric_open?") (("" (skosimp) (("" (split) (("1" (flatten) (("1" (inst + "a!1-x!1") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((metric_open_def formula-decl nil metric_space nil) (set type-eq-decl nil sets nil) (< const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_space_def nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (x!1 skolem-const-decl "real" real_topology nil) (a!1 skolem-const-decl "real" real_topology nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_open? const-decl "bool" metric_space_def nil)) nil)) (closed_inf_TCC1 0 (closed_inf_TCC1-1 nil 3454134699 ("" (skosimp) (("" (rewrite "open_complement" 1 :dir rl) (("" (lemma "inf_open_TCC1" ("a" "a!1")) (("" (case-replace "complement({x | a!1 <= x})={x | x < a!1}") (("" (hide-all-but 1) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((open_complement formula-decl nil topology "topology/") (set type-eq-decl nil sets nil) (<= const-decl "bool" reals 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) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (< const-decl "bool" reals nil) (complement const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (inf_open_TCC1 subtype-tcc nil real_topology nil)) nil)) (inf_closed_TCC1 0 (inf_closed_TCC1-1 nil 3454134699 ("" (skosimp) (("" (rewrite "open_complement" 1 :dir rl) (("" (lemma "open_inf_TCC1" ("a" "a!1")) (("" (case-replace "complement({x | x <= a!1})={x | a!1 < x}") (("" (hide-all-but 1) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((open_complement formula-decl nil topology "topology/") (set type-eq-decl nil sets nil) (<= const-decl "bool" reals 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) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (< const-decl "bool" reals nil) (complement const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (open_inf_TCC1 subtype-tcc nil real_topology nil)) nil)) (left_semiclosed_interval_TCC1 0 (left_semiclosed_interval_TCC1-1 nil 3509857231 ("" (inst + "0") nil 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)) nil)) (right_semiclosed_interval_TCC1 0 (right_semiclosed_interval_TCC1-1 nil 3509857231 ("" (inst + "0") nil 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)) nil)) (left_semiclosed_interval_is_interval 0 (left_semiclosed_interval_is_interval-1 nil 3509857231 ("" (skolem + "X!1") (("" (typepred "X!1") (("" (skosimp) (("" (replace -1) (("" (hide -1) (("" (expand "closed_inf") (("" (expand "interval?") (("" (skosimp) (("" (typepred "x!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((left_semiclosed_interval nonempty-type-eq-decl nil real_topology nil) (closed_inf const-decl "closed" real_topology nil) (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (interval? const-decl "bool" real_topology nil)) nil)) (right_semiclosed_interval_is_interval 0 (right_semiclosed_interval_is_interval-1 nil 3509857231 ("" (skolem + "X!1") (("" (typepred "X!1") (("" (skosimp) (("" (replace -1) (("" (hide -1) (("" (expand "inf_closed") (("" (expand "interval?") (("" (skosimp) (("" (typepred "x!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((right_semiclosed_interval nonempty-type-eq-decl nil real_topology nil) (inf_closed const-decl "closed" real_topology nil) (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (interval? const-decl "bool" real_topology nil)) nil)) (left_semiclosed_interval_is_closed 0 (left_semiclosed_interval_is_closed-1 nil 3509857231 ("" (skolem + "X!1") (("" (typepred "X!1") (("" (skosimp) (("" (typepred "closed_inf(a!1)") (("" (replace -2 * rl) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((left_semiclosed_interval nonempty-type-eq-decl nil real_topology nil) (closed_inf const-decl "closed" real_topology nil) (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (right_semiclosed_interval_is_closed 0 (right_semiclosed_interval_is_closed-1 nil 3509857231 ("" (skolem + "X!1") (("" (typepred "X!1") (("" (skosimp) (("" (typepred "inf_closed(a!1)") (("" (replace -2) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((right_semiclosed_interval nonempty-type-eq-decl nil real_topology nil) (inf_closed const-decl "closed" real_topology nil) (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.296Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26