| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle compactness.prfSprache: Lisp |
|||||||||||||||
|
(compactness (IMP_metric_spaces_TCC1 0 (IMP_metric_spaces_TCC1-1 nil 3514557102 ("" (lemma "fullset_metric_space") (("" (propax) nil nil)) nil) ((fullset_metric_space formula-decl nil compactness nil)) nil)) (nBalls_open_cover 0 (nBalls_open_cover-1 nil 3459609819 ("" (skosimp*) (("" (expand "open_cover?") (("" (expand "extend") (("" (split +) (("1" (expand "subset?") (("1" (skosimp*) (("1" (assert) (("1" (expand "Union") (("1" (case "EXISTS (n: posnat): n > d(p!1,x!1)") (("1" (skosimp*) (("1" (inst + "ball(p!1,n!1)") (("1" (expand "ball") (("1" (assert) nil nil)) nil) ("2" (ground) (("1" (expand "nBalls") (("1" (expand "restrict") (("1" (inst?) nil nil)) nil)) nil) ("2" (lemma "ball_open") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "axiom_of_archimedes") (("2" (inst?) (("2" (skosimp*) (("2" (inst + "i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((open_cover? const-decl "bool" compactness nil) (Union const-decl "set" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (i!1 skolem-const-decl "int" compactness nil) (axiom_of_archimedes formula-decl nil real_props nil) (restrict const-decl "R" restrict nil) (ball_open formula-decl nil metric_spaces nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (set type-eq-decl nil sets nil) (open? const-decl "bool" metric_spaces nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (ball const-decl "set[T]" metric_spaces nil) (p!1 skolem-const-decl "T" compactness nil) (n!1 skolem-const-decl "posnat" compactness nil) (nBalls const-decl "set[(open?)]" compactness nil) (FALSE const-decl "bool" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (T formal-nonempty-type-decl nil compactness nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (member const-decl "bool" sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (extend const-decl "R" extend nil)) shostak)) (reverse_ball_TCC1 0 (reverse_ball_TCC1-1 nil 3459866641 ("" (inst + "(LAMBDA (H: set[[T, posreal]], a: {s: (nonempty?[T]) | ball_covering(H)(s)}): choose({h: (H) | ball[T, d](h`1, h`2) = a}))" (("1" (skosimp*) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (typepred "a!1") (("1" (expand "ball_covering") (("1" (skosimp*) (("1" (inst - "h!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "fullset_metric_space") nil nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (ball const-decl "set[T]" metric_spaces nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (ball_covering const-decl "set[set[T]]" compactness nil) (nonempty? const-decl "bool" sets 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) (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) (T formal-nonempty-type-decl nil compactness nil)) nil)) (set_compact 0 (set_compact-1 nil 3459849180 ("" (skosimp*) (("" (expand "compact?") (("" (inst - "ball_covering(H!1)") (("" (prop) (("" (skosimp*) (("" (expand "finite_cover?") (("" (prop) (("" (lemma "is_finite_surj[set[T]]") (("" (inst - "YS!1") (("" (skosimp*) (("" (prop) (("" (skosimp*) (("" (expand "surjective?") (("" (inst + "N!1" "(LAMBDA (n: below[N!1]): reverse_ball(H!1,f!1(n)))") (("1" (expand "open_cover?" +) (("1" (expand "subset?") (("1" (expand "member") (("1" (expand "Union") (("1" (expand "ball_covering" +) (("1" (prop) (("1" (skosimp*) (("1" (expand "open_cover?") (("1" (prop) (("1" (expand "subset?") (("1" (expand "member") (("1" (expand "Union") (("1" (case "FORALL (x: T): S!1(x) => (EXISTS (a: (YS!1)): a(x))") (("1" (inst - "x!1") (("1" (prop) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (inst + "ball(reverse_ball(H!1,a!1)`1,reverse_ball(H!1,a!1)`2)") (("1" (typepred "reverse_ball(H!1,a!1)") (("1" (assert) nil nil)) nil) ("2" (expand "ball_covering") (("2" (inst + "reverse_ball(H!1,a!1)") (("1" (inst - "a!1") (("1" (skosimp*) (("1" (inst + "x!2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (x: set[T]): YS!1(x) => (EXISTS (h: (H!1)): x = ball(h`1, h`2))") (("1" (inst - "a!1") (("1" (prop) (("1" (expand "ball_covering") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "ball_covering") (("2" (case "FORALL (x: set[T]): YS!1(x) => (EXISTS (h: (H!1)): x = ball(h`1, h`2))") (("1" (inst - "a!1") (("1" (prop) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "ball_open") (("2" (inst - "h!1`2" "h!1`1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "n!1") (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (typepred "f!1(n!1)") (("1" (expand "subset?") (("1" (case "FORALL (x: set[T]): member(x, YS!1) => member(x, ball_covering(H!1))") (("1" (inst - "f!1(n!1)") (("1" (expand "member") (("1" (expand "ball_covering") (("1" (skosimp*) (("1" (inst - "h!1`1") (("1" (expand "ball") (("1" (assert) (("1" (decompose-equality) (("1" (inst - "h!1`1") (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (prop) (("1" (expand "space_zero?") (("1" (inst - "h!1`1" "h!1`1") (("1" (prop) (("1" (assert) nil nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "f!1(n!1)") (("2" (expand "subset?") (("2" (case "FORALL (x: set[T]): member(x, YS!1) => member(x, ball_covering(H!1))") (("1" (inst - "f!1(n!1)") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((compact? const-decl "bool" compactness nil) (finite_cover? const-decl "bool" compactness nil) (is_finite_surj formula-decl nil finite_sets nil) (H!1 skolem-const-decl "set[[T, posreal]]" compactness nil) (f!1 skolem-const-decl "[below[N!1] -> (YS!1)]" compactness nil) (YS!1 skolem-const-decl "set[set[T]]" compactness nil) (nonempty? const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (N!1 skolem-const-decl "nat" compactness nil) (< const-decl "bool" reals 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) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (ball const-decl "set[T]" metric_spaces nil) (reverse_ball const-decl "{h: (H) | ball(h`1, h`2) = A}" compactness nil) (subset? const-decl "bool" sets nil) (Union const-decl "set" sets nil) (a!1 skolem-const-decl "(YS!1)" compactness nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (ball_open formula-decl nil metric_spaces nil) (member const-decl "bool" sets nil) (open_cover? const-decl "bool" compactness nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_space? const-decl "bool" metric_spaces_def nil) (space_zero? const-decl "bool" metric_spaces_def nil) (h!1 skolem-const-decl "(H!1)" compactness nil) (fullset const-decl "set" sets nil) (fullset_metric_space formula-decl nil compactness nil) (surjective? const-decl "bool" functions nil) (ball_covering const-decl "set[set[T]]" compactness 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) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil compactness nil)) shostak)) (idxCover_TCC1 0 (idxCover_TCC1-1 nil 3459871403 ("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (assert) (("" (lemma "set_compact") (("" (inst?) (("" (inst - "S!1") (("" (assert) (("" (skosimp*) (("" (inst - "(N!1,seq!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (T formal-nonempty-type-decl nil compactness 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) (open_cover? const-decl "bool" compactness nil) (ball_covering const-decl "set[set[T]]" compactness nil) (compact? const-decl "bool" compactness nil) (Htype type-eq-decl nil compactness nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (set_compact formula-decl nil compactness nil) (empty? const-decl "bool" sets nil)) nil)) (idxCover_def 0 (idxCover_def-1 nil 3460202946 ("" (skolem!) (("" (assert) (("" (flatten) (("" (typepred "idxCover(S!1, H!1)") (("1" (expand "ball_covering") (("1" (expand "open_cover?") (("1" (flatten) (("1" (hide -2) (("1" (expand "subset?") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (expand "Union") (("1" (skosimp*) (("1" (typepred "a!1") (("1" (skosimp*) (("1" (typepred "h!1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (assert) (("1" (inst + "h!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((idxCover const-decl "{pair: [N: nat, seq: [below[N] -> (H)]] | open_cover?(ball_covering({h: [T, posreal] | H(h) AND (EXISTS (n: below[pair`1]): h = pair`2(n))}), S)}" compactness nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (Htype type-eq-decl nil compactness nil) (compact? const-decl "bool" compactness nil) (< const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (ball_covering const-decl "set[set[T]]" compactness 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) (open_cover? const-decl "bool" compactness nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil compactness nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (ball const-decl "set[T]" metric_spaces nil) (Union const-decl "set" sets nil) (subset? const-decl "bool" sets nil)) nil)) (set_compact_alt 0 (set_compact_alt-1 nil 3459871447 ("" (skosimp*) (("" (assert) (("" (lemma "set_compact") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (max_min_finite_scaf 0 (max_min_finite_scaf-5 nil 3460115843 ("" (skosimp*) (("" (case "FORALL (n: below(N!1)): nonempty?[nat]({M: nat| FORALL (m: above(M)): P!1(m, n)})") (("1" (case "is_finite[nat]({x: nat | EXISTS (n: below(N!1)): x = min_nat[nat].min({M: nat | FORAL (("1" (name "f" "(LAMBDA (n:below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m,n)}))") (("1" (swap-rel -1) (("1" (inst + "max({K: nat | EXISTS (n1: below(N!1)): K = f(n1)})") (("1" (skosimp*) (("1" (typepred "m!1") (("1" (typepred "n!1") (("1" (replace -3) (("1" (typepred "max({K: nat | EXISTS (n1: below(N!1)): K = (LAMBDA (n: below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n)})) (n1)})") (("1" (skosimp*) (("1" (inst - "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "n!1") (("1" (prop) (("1" (swap-rel -1) (("1" (add-formulas -1 -4) (("1" (assert) (("1" (both-sides "-" "max({K: nat | EXISTS (n1: below(N!1)): K = min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n1)})})" -1) (("1" (assert) (("1" (typepred "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "m!1") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (prop) (("2" (inst - "min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil) ("3" (prop) (("3" (expand "empty?") (("3" (expand "nonempty?") (("3" (expand "empty?") (("3" (expand "member") (("3" (inst - "min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst + "n!1") nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst + "n!1") nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n!1") nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (case "FORALL (n: below(N!1)): EXISTS (M: nat): FORALL (m: above(M)): P!1(m, n)") (("1" (inst - "n!1") (("1" (skosimp*) (("1" (inst -2 "M!1") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst + "n!1") nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (case "FORALL (n: below(N!1)): EXISTS (M: nat): FORALL (m: above(M)): P!1(m, n)") (("1" (inst - "n!1") (("1" (skosimp*) (("1" (inst -2 "M!1") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst-cp - "n!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "f(0)") (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "is_finite_surj[nat]") (("2" (inst - "{x: nat | EXISTS (n: below(N!1)): x = min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n)})}") (("2" (prop) (("2" (inst + "N!1" "(LAMBDA (n: below(N!1)): min_nat[nat].min ({M: nat | FORALL (m: above(M)): P!1(m, n)}))") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst -2 "n!1") (("2" (skosimp*) (("2" (inst - "M!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((above nonempty-type-eq-decl nil integers nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (posint nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals 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) (is_finite_surj formula-decl nil finite_sets nil) (surjective? const-decl "bool" functions nil) (below type-eq-decl nil nat_types nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (N!1 skolem-const-decl "posint" compactness nil) (P!1 skolem-const-decl "[[nat, below(N!1)] -> bool]" compactness nil) (f skolem-const-decl "[n: below(N!1) -> {a | (FORALL (m: above(a)): P!1(m, n)) AND (FORALL (x: nat): (FORALL (m: above(x)): P!1(m, n)) IMPLIES a <= x)}]" compactness nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (restrict const-decl "R" restrict nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_plus_gt2 formula-decl nil real_props nil) (both_sides_plus_ge2 formula-decl nil real_props nil) (both_sides_minus_gt1 formula-decl nil real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (member const-decl "bool" sets nil) (n!1 skolem-const-decl "below(N!1)" compactness nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (is_finite const-decl "bool" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil)) nil) (max_min_finite_scaf-4 nil 3460115556 (";;; Proof max_min_finite_scaf-3 for formula compactness.max_min_finite_scaf" (skosimp*) ((";;; Proof max_min_finite_scaf-3 for formula compactness.max_min_finite_scaf" (name "f" "(LAMBDA (n:below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m,n)}))") (("1" (swap-rel -1) (("1" (inst-cp + "max({K: nat | EXISTS (n1: below(N!1)): K = f(n1)})") (("1" (skosimp*) (("1" (typepred "m!1") (("1" (typepred "n!1") (("1" (replace -3) (("1" (typepred "max({K: nat | EXISTS (n1: below(N!1)): K = (LAMBDA (n: below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n)})) (n1)})") (("1" (skosimp*) (("1" (inst-cp - "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst-cp - "n!1") (("1" (prop) (("1" (swap-rel -1) (("1" (add-formulas -1 -4) (("1" (assert) (("1" (both-sides "-" "max({K: nat | EXISTS (n1: below(N!1)): K = min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n1)})})" -1) (("1" (assert) (("1" (typepred "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst-cp - "m!1") nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst-cp - "M!1") nil))))))))))))) ("2" (expand "nonempty?") (("2" (skosimp*) (("2" (expand "empty?") (("2" (expand "member") (("2" (inst-cp - "M!1") nil))))))))))))) ("2" (postpone) nil) ("3" (postpone) nil) ("4" (postpone) nil))) ("2" (postpone) nil) ("3" (postpone) nil))) ("2" (postpone) nil))))) ("2" (postpone) nil))))) ("2" (postpone) nil) ("3" (postpone) nil))))))))))) ("2" (postpone) nil))))) ("2" (postpone) nil)))) ";;; developed with shostak decision procedures") nil nil) (max_min_finite_scaf-3 nil 3460114454 ("" (skosimp*) (("" (name "f" "(LAMBDA (n:below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m,n)}))") (("1" (swap-rel -1) (("1" (inst + "max({K: nat | EXISTS (n1: below(N!1)): K = f(n1)})") (("1" (skosimp*) (("1" (typepred "m!1") (("1" (typepred "n!1") (("1" (replace -3) (("1" (typepred "max({K: nat | EXISTS (n1: below(N!1)): K = (LAMBDA (n: below(N!1)): min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n)})) (n1)})") (("1" (skosimp*) (("1" (inst - "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "n!1") (("1" (prop) (("1" (swap-rel -1) (("1" (add-formulas -1 -4) (("1" (assert) (("1" (both-sides "-" "max({K: nat | EXISTS (n1: below(N!1)): K = min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n1)})})" -1) (("1" (assert) (("1" (typepred "min_nat[nat].min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "m!1") nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst - "M!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (skosimp*) (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "M!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) nil nil) (max_min_finite_scaf-2 nil 3460114294 ("" (skosimp*) (("" (name "f" "(LAMBDA (n:below(N!1)): min({M: nat | FORALL (m: above(M)): P!1(m,n)}))") (("1" (swap-rel -1) (("1" (inst + "max({K: nat | EXISTS (n1: below(N!1)): K = f(n1)})") (("1" (skosimp*) (("1" (typepred "m!1") (("1" (typepred "n!1") (("1" (replace -3) (("1" (typepred "max({K: nat | EXISTS (n1: below(N!1)): K = (LAMBDA (n: below(N!1)): min({M: nat | FORALL (m: above(M)): P!1(m, n)})) (n1)})") (("1" (skosimp*) (("1" (inst - "min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "n!1") (("1" (prop) (("1" (swap-rel -1) (("1" (add-formulas -1 -4) (("1" (assert) (("1" (both-sides "-" "max({K: nat | EXISTS (n1: below(N!1)): K = min({M: nat | FORALL (m: above(M)): P!1(m, n1)})})" -1) (("1" (assert) (("1" (typepred "min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "m!1") nil nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) nil nil) (max_min_finite_scaf-1 nil 3460111094 ("" (skosimp*) (("" (name "f" "(LAMBDA (n:below(N!1)): min({M: nat | FORALL (m: above(M)): P!1(m,n)}))") (("1" (swap-rel -1) (("1" (inst + "max({K: nat | EXISTS (n1: below(N!1)): K = f(n1)})") (("1" (skosimp*) (("1" (typepred "m!1") (("1" (typepred "n!1") (("1" (replace -3) (("1" (typepred "max({K: nat | EXISTS (n1: below(N!1)): K = (LAMBDA (n: below(N!1)): min({M: nat | FORALL (m: above(M)): P!1(m, n)})) (n1)})") (("1" (skosimp*) (("1" (inst - "min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "n!1") (("1" (prop) (("1" (swap-rel -1) (("1" (add-formulas -1 -4) (("1" (assert) (("1" (both-sides "-" "max({K: nat | EXISTS (n1: below(N!1)): K = min({M: nat | FORALL (m: above(M)): P!1(m, n1)})})" -1) (("1" (assert) (("1" (typepred "min({M: nat | FORALL (m: above(M)): P!1(m, n!1)})") (("1" (inst - "m!1") nil nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) nil shostak)) (compact_sequence_limit 0 (compact_sequence_limit-1 nil 3459784863 ("" (skosimp*) (("" (lemma "max_min_finite_scaf") (("" (name "K" "{h: [T,posreal] | EXISTS (M: nat): FORALL (m: above(M)): d(seq!1(m),h`1) > h`2}") (("" (name "IC" "idxCover(S!1,K)") (("1" (name "PT" "(LAMBDA (j: nat, n: below(IC`1)): (d(seq!1(j), IC`2(n)`1) > IC`2(n)`2))") (("1" (inst - "IC`1" "PT") (("1" (replace -1 - rl) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (lemma "idxCover_def") (("1" (inst - "K" "S!1" "seq!1(TOTAL_M!1 + 1)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (typepred "n!1") (("1" (case-replace "idxCover(S!1, K) = IC") (("1" (inst - "TOTAL_M!1+1" "n!1") (("1" (expand "ball") (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (expand "space_symmetric?") (("1" (prop) (("1" (inst - "seq!1(TOTAL_M!1 + 1)" "IC`2(n!1)`1") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "open_cover?") (("2" (prop) (("1" (expand "subset?") (("1" (expand "Union") (("1" (expand "member") (("1" (skosimp*) (("1" (inst 2 "x!1") (("1" (skosimp*) (("1" (inst + "ball(x!1,epsilon!1/2)") (("1" (expand "ball") (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (expand "space_zero?") (("1" (prop) (("1" (inst - "x!1" "x!1") (("1" (prop) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ball_covering") (("2" (inst + "(x!1,epsilon!1/2)") (("2" (expand "K") (("2" (inst + "N!1") (("2" (skosimp*) (("2" (inst + "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "ball_covering") (("2" (skosimp*) (("2" (lemma "ball_open") (("2" (inst - "h!1`2" "h!1`1") (("2" (replace -2 +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "IC") (("2" (skosimp*) (("2" (typepred "IC`2(n!1)") (("2" (case "K = ({h: [T, posreal] | EXISTS (M: nat): FORALL (m: above(M)): d(seq!1(m), h`1) > h`2})") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (lemma "idxCover_def") (("2" (inst - "{h: [T, posreal] | EXISTS (M: nat): FORALL (m: above(M)): d(seq!1(m), h`1) > h`2}" "S!1" "x!1") (("2" (assert) (("2" (prop) (("1" (skosimp*) nil nil) ("2" (expand "open_cover?") (("2" (expand "subset?") (("2" (expand "member") (("2" (prop) (("1" (skosimp*) (("1" (expand "Union") (("1" (inst 3 "x!2") (("1" (skosimp*) (("1" (inst + "ball(x!2,epsilon!1/2)") (("1" (expand "ball") (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (expand "space_zero?") (("1" (prop) (("1" (inst - "x!2" "x!2") (("1" (prop) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ball_covering") (("2" (inst + "(x!2,epsilon!1/2)") (("2" (inst + "N!1") (("2" (skosimp*) (("2" (inst + "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "ball_covering") (("2" (skosimp*) (("2" (lemma "ball_open") (("2" (inst - "h!1`2" "h!1`1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "open_cover?") (("2" (prop) (("1" (expand "subset?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "Union") (("1" (inst 2 "x!1") (("1" (skosimp*) (("1" (inst + "ball(x!1,epsilon!1/2)") (("1" (expand "ball") (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (expand "space_zero?") (("1" (prop) (("1" (inst - "x!1" "x!1") (("1" (prop) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ball_covering") (("2" (inst + "(x!1,epsilon!1/2)") (("2" (replace -2 + rl) (("2" (assert) (("2" (inst + "N!1") (("2" (skosimp*) (("2" (inst + "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "ball_covering") (("2" (skosimp*) (("2" (lemma "ball_open") (("2" (inst - "h!1`2" "h!1`1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((max_min_finite_scaf formula-decl nil compactness nil) (idxCover const-decl "{pair: [N: nat, seq: [below[N] -> (H)]] | open_cover?(ball_covering({h: [T, posreal] | H(h) AND (EXISTS (n: below[pair`1]): h = pair`2(n))}), S)}" compactness nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Htype type-eq-decl nil compactness nil) (ball_covering const-decl "set[set[T]]" compactness nil) (open_cover? const-decl "bool" compactness nil) (compact? const-decl "bool" compactness nil) (below type-eq-decl nil nat_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (K skolem-const-decl "[[T, posreal] -> boolean]" compactness nil) (S!1 skolem-const-decl "set[T]" compactness nil) (IC skolem-const-decl "{pair: [N: nat, seq: [below[N] -> (K)]] | open_cover?(ball_covering({h: [T, posreal] | K(h) AND (EXISTS (n: below[pair`1]): h = pair`2(n))}), S!1)}" compactness nil) (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (NOT const-decl "[bool -> bool]" booleans nil) (fullset_metric_space formula-decl nil compactness nil) (space_symmetric? const-decl "bool" metric_spaces_def nil) (fullset const-decl "set" sets nil) (seq!1 skolem-const-decl "[nat -> (S!1)]" compactness nil) (TOTAL_M!1 skolem-const-decl "nat" compactness nil) (n!1 skolem-const-decl "below[idxCover(S!1, K)`1]" compactness nil) (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) (int_minus_int_is_int application-judgement "int" integers nil) (metric_space? const-decl "bool" metric_spaces_def nil) (ball const-decl "set[T]" metric_spaces nil) (Union const-decl "set" sets nil) (space_zero? const-decl "bool" metric_spaces_def nil) (epsilon!1 skolem-const-decl "posreal" compactness nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (x!1 skolem-const-decl "T" compactness nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (ball_open formula-decl nil metric_spaces nil) (idxCover_def formula-decl nil compactness nil) (empty? const-decl "bool" sets nil) (epsilon!1 skolem-const-decl "posreal" compactness nil) (x!2 skolem-const-decl "T" compactness nil) (nonempty? const-decl "bool" sets nil) (below type-eq-decl nil naturalnumbers nil) (epsilon!1 skolem-const-decl "posreal" compactness nil) (x!1 skolem-const-decl "T" compactness nil) (T formal-nonempty-type-decl nil compactness 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) (= const-decl "[T, T -> boolean]" equalities nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (above nonempty-type-eq-decl nil integers nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (set type-eq-decl nil sets nil)) shostak)) (compact_open_increasing_seq 0 (compact_open_increasing_seq-1 nil 3465654577 ("" (skeep) (("" (skosimp*) (("" (label "comps" -1) (("" (label "inc" -2) (("" (label "oc" -3) (("" (label "fp" 1) (("" (case "FORALL (i,j: nat): i<=j IMPLIES subset?(seq!1(i),seq!1(j))") (("1" (label "ijcase" -1) (("1" (name "YS!1" "{AZ: set[T] | EXISTS (k: nat): AZ = seq!1(k)}") (("1" (label "ysname" -1) (("1" (expand "compact?") (("1" (inst - "YS!1") (("1" (split) (("1" (skosimp*) (("1" (label "ys2fc" -2) (("1" (name "ysenum" "(lambda (a: (YS!2)): min_nat.min({j: nat | seq!1(j) = a}))") (("1" (label "ysenumname" -1) (("1" (name "K" "max({j: nat| EXISTS (a: (YS!2)): j = ysenum(a)})") (("1" (label "kname" -1) (("1" (inst + "K") (("1" (case "FORALL (a: (YS!2)): subset?(a,seq!1(K))") (("1" (label "kdef" -1) (("1" (copy "ys2fc") (("1" (hide "ys2fc") (("1" (expand "finite_cover?") (("1" (flatten) (("1" (label "isfin" -1) (("1" (label "ysoc" -2) (("1" (expand "open_cover?" "ysoc") (("1" (flatten) (("1" (hide -3) (("1" (expand "subset?") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (assert) (("1" (expand "Union") (("1" (skosimp*) (("1" (inst - "a!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst "ijcase" "ysenum(a!1)" "K") (("2" (split) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (typepred "K") (("2" (inst - "ysenum(a!1)") (("2" (skosimp*) (("2" (prop) (("2" (inst + "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (expand "finite_cover?") (("1" (lemma "is_finite_surj") (("1" (inst - "{j: nat | EXISTS (a: (YS!2)): j = ysenum(a)}") (("1" (assert) (("1" (hide (2 3 4 5)) (("1" (flatten) (("1" (label "ifys" -3) (("1" (lemma "is_finite_surj[set[T]]") (("1" (inst - "YS!2") (("1" (assert) (("1" (skosimp*) (("1" (inst + "N!1" "ysenum o f!1") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (expand "o") (("1" (inst - "a!1") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "o") (("2" (inst + "f!1(x1!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (case "not empty?(YS!2)") (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (inst - "ysenum(x!1)") (("1" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (expand "member") (("2" (expand "finite_cover?") (("2" (expand "open_cover?") (("2" (flatten) (("2" (expand "subset?" "ys2fc") (("2" (inst + "0") (("2" (expand "subset?") (("2" (expand "member" +) (("2" (skosimp*) (("2" (inst "ys2fc" "x!1") (("2" (expand "member" "ys2fc") (("2" (assert) (("2" (expand "Union") (("2" (skosimp*) (("2" (typepred "a!1") (("2" (inst - "a!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) ("2" (skosimp*) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (expand "subset?") (("2" (inst "comps" "a!1") (("2" (expand "member") (("2" (replace "ysname" - rl) (("2" (assert) (("2" (skosimp*) (("2" (inst - "k!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "open_cover?") (("2" (flatten) (("2" (assert) (("2" (skosimp*) (("2" (replace "ysname" - rl) (("2" (assert) (("2" (skosimp*) (("2" (inst "oc" "C!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but ("inc" 1)) (("2" (skosimp*) (("2" (name "K" "min_nat.min({r: nat | r>=i!1 AND not subset?(seq!1(i!1),seq!1(r))})") (("1" (name "rset" "{r: nat | r >= i!1 AND NOT subset?(seq!1(i!1), seq!1(r))}") (("1" (replace -1) (("1" (label "rsetname" -1) (("1" (case "rset(K)") (("1" (replace "rsetname" -1 rl) (("1" (assert) (("1" (flatten) (("1" (case "K = i!1") (("1" (replace -1) (("1" (expand "subset?") (("1" (skosimp*) nil nil)) nil)) nil) ("2" (case "subset?(seq!1(i!1),seq!1(K-1))") (("1" (inst - "K-1") (("1" (assert) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (typepred "K") (("2" (inst - "K-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "j!1") (("2" (expand "subset?") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (i!1 skolem-const-decl "nat" compactness nil) (K skolem-const-decl "{a | (a >= i!1 AND NOT subset?(seq!1(i!1), seq!1(a))) AND (FORALL (x: nat): x >= i!1 AND NOT subset?(seq!1(i!1), seq!1(x)) IMPLIES a <= x)}" compactness nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (nonempty? const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (restrict const-decl "R" restrict nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/") (Union const-decl "set" sets nil) (member const-decl "bool" sets nil) (open_cover? const-decl "bool" compactness nil) (finite_cover? const-decl "bool" compactness nil) (x!1 skolem-const-decl "set[T]" compactness nil) (surjective? const-decl "bool" functions nil) (f!1 skolem-const-decl "[below[N!1] -> (YS!2)]" compactness nil) (ysenum skolem-const-decl "[a: (YS!2) -> {a_1 | seq!1(a_1) = a AND (FORALL (x: nat): seq!1(x) = a IMPLIES a_1 <= x)}]" compactness nil) (seq!1 skolem-const-decl "[nat -> (open?)]" compactness nil) (O const-decl "T3" function_props nil) (YS!2 skolem-const-decl "set[set[T]]" compactness nil) (below type-eq-decl nil nat_types nil) (N!1 skolem-const-decl "nat" compactness nil) (< const-decl "bool" reals nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (is_finite_surj formula-decl nil finite_sets nil) (compact? const-decl "bool" compactness nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T formal-nonempty-type-decl nil compactness nil) (set type-eq-decl nil sets nil) (subset? const-decl "bool" sets nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (open? const-decl "bool" metric_spaces nil)) shostak)) (closed_subset_of_compact 0 (closed_subset_of_compact-1 nil 3465649466 ("" (skeep) (("" (expand "compact?") (("" (skeep) (("" (name "ws" "complement[T](W)") (("" (name "XS!1" "union(singleton(ws),XS)") (("" (label "XS1def" -1) (("" (inst - "XS!1") (("" (split) (("1" (skosimp*) (("1" (label "YS1ss" -1) (("1" (label "YS1fc" -2) (("1" (name "YS!2" "{a: set[T] | YS!1(a) AND a /= ws}") (("1" (label "YS2def" -1) (("1" (case "subset?(YS!2,YS!1)") (("1" (inst + "YS!2") (("1" (split) (("1" (expand "subset?") (("1" (skosimp*) (("1" (expand "member") (("1" (label "x1YS2" -1) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (assert) (("1" (replace "XS1def" "YS1ss" rl) (("1" (expand "union" "YS1ss") (("1" (assert) (("1" (expand "singleton" "YS1ss") (("1" (replace "YS2def" "x1YS2" rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "YS21ss" -1) (("2" (expand "finite_cover?") (("2" (flatten) (("2" (split) (("1" (lemma "finite_subset[set[T]]") (("1" (inst - "YS!1" "YS!2") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "open_cover?") (("2" (flatten) (("2" (split) (("1" (expand "subset?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "Union") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (assert) (("1" (assert) (("1" (skosimp*) (("1" (inst + "a!1") (("1" (replace "YS2def" + rl) (("1" (assert) (("1" (expand "complement") (("1" (replace -9 + rl) (("1" (assert) (("1" (replace -1) (("1" (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" (replace "YS2def" -1 rl) (("2" (assert) (("2" (flatten) (("2" (inst - "C!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (replace "YS2def" - rl) (("2" (assert) (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "open_cover?") (("2" (flatten) (("2" (split) (("1" (expand "subset?") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "Union") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (hide -4) (("1" (split) (("1" (skosimp*) (("1" (inst + "a!1") (("1" (replace "XS1def" + rl) (("1" (expand "union") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "ws") (("1" (expand "complement") (("1" (replace -3 + rl) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "union") (("2" (expand "singleton") (("2" (expand "member") (("2" (replace "XS1def" + rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (expand "union") (("2" (assert) (("2" (skosimp*) (("2" (replace "XS1def" - rl) (("2" (assert) (("2" (inst - "C!1") (("2" (assert) (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (expand "closed?") (("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) ((compact? const-decl "bool" compactness nil) (complement const-decl "set" sets 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-nonempty-type-decl nil compactness nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (finite_cover? const-decl "bool" compactness nil) (is_finite const-decl "bool" finite_sets nil) (YS!1 skolem-const-decl "set[set[T]]" compactness nil) (finite_set type-eq-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (finite_subset formula-decl nil finite_sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (YS!2 skolem-const-decl "[set[T] -> boolean]" compactness nil) (a!1 skolem-const-decl "(YS!1)" compactness nil) (Union const-decl "set" sets nil) (open_cover? const-decl "bool" compactness nil) (closed? const-decl "bool" metric_spaces nil) (ws skolem-const-decl "set[T]" compactness nil) (a!1 skolem-const-decl "(XS)" compactness nil) (XS skolem-const-decl "set[set[T]]" compactness nil) (XS!1 skolem-const-decl "(nonempty?)" compactness nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (nonempty_union1 application-judgement "(nonempty?)" sets nil) (union const-decl "set" sets nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (nonempty? const-decl "bool" sets nil)) shostak)) (compact_closed 0 (compact_closed-1 nil 3465654003 ("" (skeep) (("" (copy -1) (("" (label "scomp" -2) (("" (hide "scomp") (("" (expand "closed?") (("" (expand "open?") (("" (expand "interior") (("" (expand "interior_point?") (("" (expand "subset?") (("" (expand "member") (("" (expand "ball") (("" (expand "complement") (("" (expand "member") (("" (decompose-equality) (("" (iff) (("" (ground) (("" (name "setenum" "(lambda (j: nat): {tz: T | d(x!1,tz) > 1/(j+1)})") (("" (lemma "compact_open_increasing_seq") (("" (reveal "scomp") (("" (inst - "S") (("" (assert) (("" (hide "scomp") (("" (case "forall (zt: nat): open?(setenum(zt))") (("1" (inst -2 "setenum") (("1" (label "setenumopen" -1) (("1" (hide -1) (("1" (split) (("1" (skosimp*) (("1" (inst + "1/(i!1 + 1)") (("1" (skosimp*) (("1" (expand "subset?") (("1" (expand "member") (("1" (inst - "x!2") (("1" (assert) (("1" (replace -2 -1 rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (replace -2 + rl) (("2" (replace -2 - rl) (("2" (assert) (("2" (cross-mult -1) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "open_cover?") (("3" (split) (("1" (expand "subset?") (("1" (expand "member") (("1" (expand "Union") (("1" (skosimp*) (("1" (lemma "axiom_of_archimedes") (("1" (case "d(x!1,x!2) = 0") (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (flatten) (("1" (expand "space_zero?") (("1" (inst - "x!1" "x!2") (("1" (assert) nil nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "1/(d(x!1,x!2)) > 0") (("1" (inst - "1/(d(x!1,x!2)) + 2") (("1" (skosimp*) (("1" (inst + "setenum(i!1)") (("1" (replace -4 + rl) (("1" (assert) (("1" (both-sides "-" "2" -2) (("1" (assert) (("1" (cross-mult 2) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "i!1") (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "setenumopen") (("2" (skosimp*) (("2" (inst - "k!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "open?") (("2" (expand "interior") (("2" (apply-extensionality) (("2" (iff) (("2" (ground) (("2" (expand "interior_point?") (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "ball") (("2" (hide -2) (("2" (hide (2 3 4 5)) (("2" (replace -2 + rl) (("2" (assert) (("2" (replace -2 - rl) (("2" (assert) (("2" (name "newr" "d(x!1,x!2)-1/(1+zt!1)") (("2" (inst + "newr") (("1" (skosimp*) (("1" (replace -1 - rl) (("1" (hide -1) (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (flatten) (("1" (expand "space_triangle?") (("1" (inst - "x!1" "x!3" "x!2") (("1" (assert) (("1" (expand "space_symmetric?") (("1" (inst - "x!2" "x!3") (("1" (assert) nil nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 + rl) (("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) ((open? const-decl "bool" metric_spaces nil) (interior_point? const-decl "bool" metric_spaces nil) (member const-decl "bool" sets nil) (complement const-decl "set" sets nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil compactness nil) (boolean nonempty-type-decl nil booleans nil) (compact_open_increasing_seq formula-decl nil compactness nil) (space_triangle? const-decl "bool" metric_spaces_def nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (space_symmetric? const-decl "bool" metric_spaces_def nil) (x!2 skolem-const-decl "T" compactness nil) (x!3 skolem-const-decl "T" compactness nil) (newr skolem-const-decl "real" compactness nil) (setenum skolem-const-decl "[nat -> [T -> bool]]" compactness nil) (open_cover? const-decl "bool" compactness nil) (Union const-decl "set" sets nil) (axiom_of_archimedes formula-decl nil real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (even? const-decl "bool" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (i!1 skolem-const-decl "int" compactness nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (fullset_metric_space formula-decl nil compactness nil) (fullset const-decl "set" sets nil) (x!1 skolem-const-decl "T" compactness nil) (x!2 skolem-const-decl "T" compactness nil) (space_zero? const-decl "bool" metric_spaces_def nil) (metric_space? const-decl "bool" metric_spaces_def nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_gt2 formula-decl nil extra_real_props 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities 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) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (ball const-decl "set[T]" metric_spaces nil) (subset? const-decl "bool" sets nil) (interior const-decl "set[T]" metric_spaces nil) (closed? const-decl "bool" metric_spaces nil)) shostak)) (compact_bounded 0 (compact_bounded-1 nil 3492532969 ("" (skeep) (("" (lemma "compact_open_increasing_seq") (("" (inst?) (("" (assert) (("" (case "EXISTS (vv:(S)): TRUE") (("1" (skeep -) (("1" (inst - "(LAMBDA (nn:nat): ball(vv,max(nn,1)))") (("1" (split -) (("1" (case "EXISTS (i:posnat): subset?(S,ball(vv,i))") (("1" (hide -2) (("1" (skeep -) (("1" (expand "bounded?") (("1" (inst + "2*i+1") (("1" (skeep) (("1" (expand "subset?") (("1" (inst-cp - "x") (("1" (inst - "y") (("1" (expand "member") (("1" (expand "ball") (("1" (assert) (("1" (lemma "fullset_metric_space") (("1" (expand "metric_space?") (("1" (flatten) (("1" (expand "space_triangle?") (("1" (inst - "x" "vv" "y") (("1" (expand "space_symmetric?") (("1" (inst - "x" "vv") (("1" (assert) nil nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil) ("3" (expand "fullset") (("3" (propax) nil nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -) (("2" (inst + "max(i,1)") nil nil)) nil)) nil) ("2" (skeep) (("2" (expand "subset?") (("2" (expand "ball") (("2" (expand "member") (("2" (skeep) (("2" (expand "max") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 2)) (("3" (lemma "nBalls_open_cover") (("3" (inst - "S" "vv") (("3" (expand "open_cover?") (("3" (flatten) (("3" (split) (("1" (expand "subset?") (("1" (skeep) (("1" (inst - "x") (("1" (assert) (("1" (expand "Union") (("1" (skosimp*) (("1" (inst + "a!1") (("1" (typepred "a!1") (("1" (expand "extend") (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (expand "nBalls") (("1" (expand "restrict") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (expand "max") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "C") (("2" (lemma "ball_open") (("2" (skosimp*) (("2" (inst - "max(k!1,1)" "vv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (lemma "ball_open") (("2" (inst - "max(nn,1)" "vv") nil nil)) nil)) nil) ("3" (skeep) (("3" (expand "max") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "bounded?") (("2" (inst 2 "1") (("2" (skosimp*) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((compact_open_increasing_seq formula-decl nil compactness nil) (x!1 skolem-const-decl "T" compactness nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bounded? const-decl "bool" compactness nil) (member const-decl "bool" sets nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_space? const-decl "bool" metric_spaces_def nil) (space_triangle? const-decl "bool" metric_spaces_def nil) (space_symmetric? const-decl "bool" metric_spaces_def 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) (y skolem-const-decl "T" compactness nil) (x skolem-const-decl "T" compactness nil) (fullset const-decl "set" sets nil) (fullset_metric_space formula-decl nil compactness nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (subset? const-decl "bool" sets nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nBalls_open_cover formula-decl nil compactness nil) (open_cover? const-decl "bool" compactness nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (restrict const-decl "R" restrict nil) (a!1 skolem-const-decl "(extend[set[T], (open?[T, d]), bool, FALSE](nBalls(vv)))" compactness nil) (= const-decl "[T, T -> boolean]" equalities nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (nBalls const-decl "set[(open?)]" compactness nil) (Union const-decl "set" sets nil) (ball_open formula-decl nil metric_spaces nil) (nnreal type-eq-decl nil real_types nil) (d formal-const-decl "[T, T -> nnreal]" compactness nil) (open? const-decl "bool" metric_spaces nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (ball const-decl "set[T]" metric_spaces nil) (S skolem-const-decl "set[T]" compactness nil) (vv skolem-const-decl "(S)" compactness nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (TRUE const-decl "bool" booleans 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-nonempty-type-decl nil compactness nil)) shostak)))
¤ 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.635Bemerkung: (vorverarbeitet am 2026-04-26) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26