| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 182 kB |
|
Quellcode-Bibliothek vect3_Heine.prfSprache: Lisp |
|||||||||||||||
|
(vect3_Heine (IMP_cross_metric_real_fun_TCC1 0 (IMP_cross_metric_real_fun_TCC1-1 nil 3462097826 ("" (lemma "real_metric_space") (("" (inst - "fullset[real]") nil nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (real_metric_space formula-decl nil real_metric_space "analysis/")) nil)) (IMP_cross_metric_real_fun_TCC2 0 (IMP_cross_metric_real_fun_TCC2-1 nil 3462097826 ("" (lemma "vect3_metric_space") (("" (propax) nil nil)) nil) ((vect3_metric_space formula-decl nil vect3_metric_space nil)) nil)) (curried_min_exists_3D_TCC1 0 (curried_min_exists_3D_TCC1-1 nil 3610811544 ("" (subtype-tcc) nil nil) nil nil)) (curried_min_exists_3D 0 (curried_min_exists_3D-4 nil 3462267937 ("" (lemma "curried_min_exists") (("" (skosimp*) (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil nil)) nil)) nil) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (prop) nil nil)) nil)) nil) ("4" (inst - "y!1") (("4" (expand "fullset") (("4" (prop) nil nil)) nil)) nil) ("5" (expand "nonempty?") (("5" (expand "empty?") (("5" (copy -2) (("5" (inst - "(A!1 + B!1)/2") (("5" (expand "member") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand "nonempty?") (("6" (expand "empty?") (("6" (copy -2) (("6" (inst - "(A!1 + B!1)/2") (("6" (expand "member") (("6" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (inst - "(A!1 + B!1)/2") (("7" (expand "member") (("7" (propax) nil nil)) nil)) nil)) nil)) nil) ("8" (expand "nonempty?") (("8" (expand "empty?") (("8" (expand "member") (("8" (inst - "(A!1 + B!1)/2") (("8" (assert) nil nil)) nil)) nil)) nil)) nil) ("9" (expand "nonempty?") (("9" (expand "empty?") (("9" (expand "member") (("9" (inst - "f!1(A!1,y!1)") (("9" (inst + "A!1") nil nil)) nil)) nil)) nil)) nil) ("10" (expand "continuous?") (("10" (expand "continuous_at?") (("10" (skosimp*) (("10" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (prop) nil nil)) nil)) nil) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("11" (expand "continuous?") (("11" (expand "continuous_at?") (("11" (skosimp*) (("11" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("12" (hide 1) (("12" (expand "continuous?") (("12" (expand "continuous_at?") (("12" (skosimp*) (("12" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (prop) nil nil)) nil)) nil) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("13" (expand "nonempty?") (("13" (expand "empty?") (("13" (expand "member") (("13" (inst - "f!1(A!1,y!1)") (("13" (inst + "A!1") nil nil)) nil)) nil)) nil)) nil) ("14" (lemma "curried_min_exists") (("14" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("14" (assert) (("14" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "closed_intervals_compact") (("2" (inst - "A!1" "B!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("15" (lemma "closed_intervals_compact") (("15" (inst - "A!1" "B!1") nil nil)) nil) ("16" (lemma "closed_intervals_compact") (("16" (inst - "A!1" "B!1") nil nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (real_div_nzreal_is_real application-judgement "real" 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_plus_real_is_real application-judgement "real" reals nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (A!1 skolem-const-decl "real" vect3_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (ball const-decl "set[T]" metric_spaces "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (y!2 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine 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) (continuous? const-decl "bool" continuity_ms_def "analysis/") (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (y!2 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (y!2 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (closed_intervals_compact formula-decl nil real_metric_space "analysis/") (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (fullset const-decl "set" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (curried_min_exists formula-decl nil cross_metric_real_fun "analysis/") (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) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space "analysis/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (dist const-decl "nnreal" distance_3D "vectors/")) nil) (curried_min_exists_3D-3 nil 3462266266 ("" (lemma "curried_min_exists") (("" (skosimp*) (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil nil)) nil)) nil) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (prop) nil nil)) nil)) nil) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (copy -2) (("4" (expand "member") (("4" (postpone) nil nil)) nil)) nil)) nil)) nil) ("5" (expand "nonempty?") (("5" (expand "empty?") (("5" (copy -2) (("5" (inst - "(A!1 + B!1)/2") (("5" (expand "member") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand "nonempty?") (("6" (expand "empty?") (("6" (copy -2) (("6" (inst - "(A!1 + B!1)/2") (("6" (expand "member") (("6" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (expand "member") (("7" (inst - "f!1(A!1,y!1)") (("7" (postpone) nil nil)) nil)) nil)) nil)) nil) ("8" (expand "continuous?") (("8" (expand "continuous_at?") (("8" (expand "member") (("8" (expand "ball") (("8" (assert) (("8" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("9" (expand "continuous?") (("9" (expand "continuous_at?") (("9" (skosimp*) (("9" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("10" (postpone) nil nil) ("11" (lemma "curried_min_exists") (("11" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("11" (assert) (("11" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "closed_intervals_compact") (("2" (inst - "A!1" "B!1") (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("12" (lemma "closed_intervals_compact") (("12" (inst - "A!1" "B!1") (("12" (postpone) nil nil)) nil)) nil) ("13" (postpone) nil nil) ("14" (postpone) nil nil) ("15" (postpone) nil nil) ("16" (postpone) nil nil)) nil)) nil)) nil)) nil) ((ball const-decl "set[T]" metric_spaces "analysis/") (closed_intervals_compact formula-decl nil real_metric_space "analysis/") (curried_min_exists formula-decl nil cross_metric_real_fun "analysis/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (dist const-decl "nnreal" distance_3D "vectors/")) nil) (curried_min_exists_3D-2 nil 3462098999 ("" (lemma "curried_min_exists") (("" (skosimp*) (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (prop) nil))))))))))) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil))))) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (prop) nil))))) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (copy -2) (("4" (inst - "(A!1 + B!1)/2") (("4" (expand "member") (("4" (propax) nil))))))))))) ("5" (expand "nonempty?") (("5" (expand "empty?") (("5" (copy -2) (("5" (inst - "(A!1 + B!1)/2") (("5" (expand "member") (("5" (propax) nil))))))))))) ("6" (expand "nonempty?") (("6" (expand "empty?") (("6" (copy -2) (("6" (inst - "(A!1 + B!1)/2") (("6" (expand "member") (("6" (propax) nil))))))))))) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (expand "member") (("7" (inst - "f(A!1,y!1)") (("7" (inst + "A!1") nil))))))))) ("8" (expand "continuous?") (("8" (expand "continuous_at?") (("8" (skosimp*) (("8" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (prop) nil))))) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))) ("9" (expand "continuous?") (("9" (expand "continuous_at?") (("9" (skosimp*) (("9" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))) ("10" (expand "nonempty?") (("10" (expand "empty?") (("10" (expand "member") (("10" (inst - "f(A!1,y!1)") (("10" (inst + "A!1") nil))))))))) ("11" (lemma "curried_min_exists") (("11" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("11" (assert) (("11" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (propax) nil))))) ("2" (lemma "closed_intervals_compact") (("2" (inst - "A!1" "B!1") nil))))))))))) ("12" (lemma "closed_intervals_compact") (("12" (inst - "A!1" "B!1") nil)))))))))) nil) ((ball const-decl "set[T]" metric_spaces "analysis/") (closed_intervals_compact formula-decl nil real_metric_space "analysis/") (curried_min_exists formula-decl nil cross_metric_real_fun "analysis/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (dist const-decl "nnreal" distance_3D "vectors/")) nil) (curried_min_exists_3D-1 nil 3462098804 (";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3D (lemma "curried_min_exists") ((";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3 (skosimp*) ((";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3 (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") ((";;; Proof curried_min_exists_3D-1 for formula real_3D_problem.curried_min_exists_3 (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (prop) nil))))))))))) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil))))) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (prop) nil))))) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (copy -2) (("4" (inst - "(A!1 + B!1)/2") (("4" (expand "member") (("4" (propax) nil))))))))))) ("5" (expand "nonempty?") (("5" (expand "empty?") (("5" (copy -2) (("5" (inst - "(A!1 + B!1)/2") (("5" (expand "member") (("5" (propax) nil))))))))))) ("6" (expand "nonempty?") (("6" (expand "empty?") (("6" (copy -2) (("6" (inst - "(A!1 + B!1)/2") (("6" (expand "member") (("6" (propax) nil))))))))))) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (expand "member") (("7" (inst - "f(A!1,y!1)") (("7" (inst + "A!1") nil))))))))) ("8" (expand "continuous?") (("8" (expand "continuous_at?") (("8" (skosimp*) (("8" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (prop) nil))))) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))) ("9" (expand "continuous?") (("9" (expand "continuous_at?") (("9" (skosimp*) (("9" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))) ("10" (expand "nonempty?") (("10" (expand "empty?") (("10" (expand "member") (("10" (inst - "f(A!1,y!1)") (("10" (inst + "A!1") nil))))))))) ("11" (lemma "curried_min_exists") (("11" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("11" (assert) (("11" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (propax) nil))))) ("2" (lemma "closed_intervals_compact") (("2" (inst - "A!1" "B!1") nil))))))))))) ("12" (lemma "closed_intervals_compact") (("12" (inst - "A!1" "B!1") nil)))))))))) ";;; developed with shostak decision procedures") nil nil)) (curried_min_is_cont_3D_TCC1 0 (curried_min_is_cont_3D_TCC1-3 nil 3462268033 ("" (lemma "curried_min_exists") (("" (skosimp*) (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil nil)) nil)) nil) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (prop) nil nil)) nil)) nil) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (copy -2) (("4" (inst - "(A!1 + B!1)/2") (("4" (expand "member") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand "nonempty?") (("5" (expand "empty?") (("5" (copy -2) (("5" (inst - "(A!1 + B!1)/2") (("5" (expand "member") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand "nonempty?") (("6" (expand "empty?") (("6" (copy -2) (("6" (inst - "(A!1 + B!1)/2") (("6" (expand "member") (("6" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (expand "member") (("7" (inst - "f!1(A!1,y!1)") (("7" (inst + "A!1") nil nil)) nil)) nil)) nil)) nil) ("8" (expand "continuous?") (("8" (expand "continuous_at?") (("8" (skosimp*) (("8" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (prop) nil nil)) nil)) nil) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("9" (expand "continuous?") (("9" (expand "continuous_at?") (("9" (skosimp*) (("9" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("10" (expand "nonempty?") (("10" (expand "empty?") (("10" (expand "member") (("10" (inst - "f!1(A!1,y!1)") (("10" (inst + "A!1") nil nil)) nil)) nil)) nil)) nil) ("11" (lemma "curried_min_exists") (("11" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("11" (assert) (("11" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "closed_intervals_compact") (("2" (inst - "A!1" "B!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("12" (lemma "closed_intervals_compact") (("12" (inst - "A!1" "B!1") nil nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (real_div_nzreal_is_real application-judgement "real" 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_plus_real_is_real application-judgement "real" reals nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (A!1 skolem-const-decl "real" vect3_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (ball const-decl "set[T]" metric_spaces "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (y!2 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine 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) (continuous? const-decl "bool" continuity_ms_def "analysis/") (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (y!2 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (closed_intervals_compact formula-decl nil real_metric_space "analysis/") (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (fullset const-decl "set" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (curried_min_exists formula-decl nil cross_metric_real_fun "analysis/") (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) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space "analysis/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (dist const-decl "nnreal" distance_3D "vectors/")) nil) (curried_min_is_cont_3D_TCC1-2 nil 3462099667 (";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is_ (lemma "curried_min_is_cont_TCC1") ((";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is (skosimp*) ((";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") ((";;; Proof curried_min_is_cont_3D_TCC1-1 for formula real_3D_problem.curried_min_is (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (prop) nil))))))))))) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil))))) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (prop) nil))))) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (copy -2) (("4" (inst - "(A!1 + B!1)/2") (("4" (expand "member") (("4" (propax) nil))))))))))) ("5" (expand "nonempty?") (("5" (expand "empty?") (("5" (copy -2) (("5" (inst - "(A!1 + B!1)/2") (("5" (expand "member") (("5" (propax) nil))))))))))) ("6" (expand "nonempty?") (("6" (expand "empty?") (("6" (copy -2) (("6" (inst - "(A!1 + B!1)/2") (("6" (expand "member") (("6" (propax) nil))))))))))) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (expand "member") (("7" (inst - "f(A!1,y!1)") (("7" (inst + "A!1") nil))))))))) ("8" (expand "continuous?") (("8" (expand "continuous_at?") (("8" (skosimp*) (("8" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (prop) nil))))) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))) ("9" (expand "continuous?") (("9" (expand "continuous_at?") (("9" (skosimp*) (("9" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (inst - "y!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))) ("10" (expand "nonempty?") (("10" (expand "empty?") (("10" (expand "member") (("10" (inst - "f(A!1,y!1)") (("10" (inst + "A!1") nil))))))))) ("11" (lemma "curried_min_is_cont_TCC1") (("11" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("11" (assert) (("11" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (propax) nil))))) ("2" (lemma "closed_intervals_compact") (("2" (inst - "A!1" "B!1") nil))))))))))) ("12" (lemma "closed_intervals_compact") (("12" (inst - "A!1" "B!1") nil)))))))))) ";;; developed with shostak decision procedures") nil nil) (curried_min_is_cont_3D_TCC1-1 nil 3462097826 ("" (subtype-tcc) nil nil) nil nil)) (curried_min_is_cont_3D 0 (curried_min_is_cont_3D-3 nil 3462266508 ("" (skosimp*) (("" (lemma "curried_min_is_cont") (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("" (prop) (("1" (expand "continuous?" +) (("1" (expand "fullset") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "closed_intervals_compact") (("2" (inst?) nil nil)) nil) ("3" (hide 2) (("3" (expand "continuous?") (("3" (skosimp*) (("3" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta !1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (typepred "y!1") (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (expand "member") (("4" (inst - "(A!1 + B!1)/2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((dist const-decl "nnreal" distance_3D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (curried_min_is_cont formula-decl nil cross_metric_real_fun "analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (closed_intervals_compact formula-decl nil real_metric_space "analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (A!1 skolem-const-decl "real" vect3_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (ball const-decl "set[T]" metric_spaces "analysis/") (y!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets 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) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (empty? const-decl "bool" sets nil) (real_div_nzreal_is_real application-judgement "real" 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_plus_real_is_real application-judgement "real" reals nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (fullset const-decl "set" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (curried_min_is_cont_3D-2 nil 3462099117 ("" (skosimp*) (("" (lemma "curried_min_is_cont") (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("" (prop) (("1" (expand "continuous?" +) (("1" (expand "fullset") (("1" (propax) nil))))) ("2" (lemma "closed_intervals_compact") (("2" (inst?) nil))) ("3" (hide 2) (("3" (expand "continuous?") (("3" (skosimp*) (("3" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta !1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (typepred "y!1") (("1" (inst - "y!1") (("1" (assert) nil) ("2" (hide -2 2) (("2" (grind) nil))))))))))))))))))))))) ("2" (hide 2) (("2" (typepred "x!1") (("2" (grind) nil))))))))))))) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (expand "member") (("4" (inst - "(A!1 + B!1)/2") (("4" (assert) nil)))))))))))))))) nil) ((dist const-decl "nnreal" distance_3D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (curried_min_is_cont formula-decl nil cross_metric_real_fun "analysis/") (closed_intervals_compact formula-decl nil real_metric_space "analysis/") (ball const-decl "set[T]" metric_spaces "analysis/")) nil) (curried_min_is_cont_3D-1 nil 3462098832 (";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont_ (skosimp*) ((";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont (lemma "curried_min_is_cont") ((";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") ((";;; Proof curried_min_is_cont_3D-1 for formula real_3D_problem.curried_min_is_cont (prop) (("1" (expand "continuous?" +) (("1" (expand "fullset") (("1" (propax) nil))))) ("2" (lemma "closed_intervals_compact") (("2" (inst?) nil))) ("3" (hide 2) (("3" (expand "continuous?") (("3" (skosimp*) (("3" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta !1") (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (typepred "y!1") (("1" (inst - "y!1") (("1" (assert) nil) ("2" (hide -2 2) (("2" (grind) nil))))))))))))))))))))))) ("2" (hide 2) (("2" (typepred "x!1") (("2" (grind) nil))))))))))))) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (expand "member") (("4" (inst - "(A!1 + B!1)/2") (("4" (assert) nil)))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (curried_min_is_cont_3D_ed_TCC1 0 (curried_min_is_cont_3D_ed_TCC1-4 nil 3462268254 ("" (lemma "curried_min_is_cont_3D_TCC1") (("" (skosimp*) (("" (inst - "f!1" "A!1" "B!1") (("" (prop) (("1" (inst - "y1!1") (("1" (prop) nil nil)) nil) ("2" (inst - "y1!1") (("2" (prop) nil nil)) nil) ("3" (inst - "y1!1") (("3" (prop) nil nil)) nil) ("4" (lemma "product_cont_product_subset") (("4" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("4" (prop) (("1" (hide-all-but (-1 2)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 1) (("5" (lemma "product_cont_product_subset") (("5" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("5" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 1) (("6" (lemma "product_cont_product_subset") (("6" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("6" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("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) (fullset const-decl "set" sets nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (ball const-decl "set[T]" metric_spaces "analysis/") (A!1 skolem-const-decl "real" vect3_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (y!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (member const-decl "bool" sets nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (product_cont_product_subset formula-decl nil cross_metric_cont "analysis/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space "analysis/") (dist const-decl "nnreal" distance_3D "vectors/") (y!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (y!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (curried_min_is_cont_3D_TCC1 subtype-tcc nil vect3_Heine nil)) nil) (curried_min_is_cont_3D_ed_TCC1-3 nil 3462268134 ("" (lemma "curried_min_is_cont_3D_TCC1") (("" (skosimp*) (("" (inst - "A!1" "B!1") (("" (prop) (("1" (inst - "y1!1") (("1" (prop) nil))) ("2" (inst - "y1!1") (("2" (prop) nil))) ("3" (inst - "y1!1") (("3" (prop) nil))) ("4" (lemma "product_cont_product_subset") (("4" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("4" (prop) (("1" (hide-all-but (-1 2)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil))))))))))))))))))))) ("5" (hide 1) (("5" (lemma "product_cont_product_subset") (("5" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("5" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil))))))))))))))))))))))) ("6" (hide 1) (("6" (lemma "product_cont_product_subset") (("6" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("6" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil)))))))))))))))))))))))))))))) nil) nil nil) (curried_min_is_cont_3D_ed_TCC1-2 nil 3462099695 (";;; Proof curried_min_is_cont_3D_ed_TCC1-1 for formula real_3D_problem.curried_min_ (lemma "curried_min_is_cont_3D_TCC1") ((";;; Proof curried_min_is_cont_3D_ed_TCC1-1 for formula real_3D_problem.curried_min (skosimp*) ((";;; Proof curried_min_is_cont_3D_ed_TCC1-1 for formula real_3D_problem.curried_min (inst - "A!1" "B!1") ((";;; Proof curried_min_is_cont_3D_ed_TCC1-1 for formula real_3D_problem.curried_min (prop) (("1" (inst - "y1!1") (("1" (prop) nil))) ("2" (inst - "y1!1") (("2" (prop) nil))) ("3" (inst - "y1!1") (("3" (prop) nil))) ("4" (lemma "product_cont_product_subset") (("4" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("4" (prop) (("1" (hide-all-but (-1 2)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil))))))))))))))))))))) ("5" (hide 1) (("5" (lemma "product_cont_product_subset") (("5" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("5" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil))))))))))))))))))))))) ("6" (hide 1) (("6" (lemma "product_cont_product_subset") (("6" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("6" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil)))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil) (curried_min_is_cont_3D_ed_TCC1-1 nil 3462097826 ("" (subtype-tcc) nil nil) nil nil)) (curried_min_is_cont_3D_ed 0 (curried_min_is_cont_3D_ed-3 nil 3462266557 ("" (skosimp*) (("" (skoletin 1) (("1" (skosimp*) (("1" (lemma "curried_min_is_cont_3D") (("1" (inst - "f!1" "A!1" "B!1") (("1" (prop) (("1" (assert) (("1" (replace -2 - rl) (("1" (expand "continuous?") (("1" (expand "continuous?") (("1" (inst - "y!1") (("1" (expand "continuous_at?") (("1" (inst - "epsilon!1") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "q!1") (("1" (assert) nil nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "product_cont_product_subset") (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!2") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!2") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "x!1" "y!2" "epsilon!2") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -) (("2" (lemma "curried_min_is_cont_TCC1") (("2" (skosimp*) (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("2" (case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)") (("1" (assert) (("1" (reveal -2) (("1" (label "cont_ed" -1) (("1" (label "nonempty" -2) (("1" (label "bigpred" -3) (("1" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil nil)) nil)) nil) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (expand "member") (("4" (inst - "f!1(A!1,y!1)") (("4" (inst + "A!1") nil nil)) nil)) nil)) nil)) nil) ("5" (lemma "product_cont_product_subset") (("5" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("5" (assert) (("5" (hide-all-but ("cont_ed" 1)) (("5" (skosimp*) (("5" (inst - "x!1" "y!2" "epsilon!1") (("5" (skosimp*) (("5" (inst + "delta!1") (("5" (skosimp*) (("5" (inst - "z!1" "w!1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (lemma "product_cont_product_subset") (("6" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("6" (assert) (("6" (hide-all-but ("cont_ed" 1)) (("6" (skosimp*) (("6" (inst - "x!1" "y!2" "epsilon!1") (("6" (skosimp*) (("6" (inst + "delta!1") (("6" (skosimp*) (("6" (inst - "z!1" "w!1") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (expand "member") (("7" (inst - "f!1(A!1,y!1)") (("7" (inst + "A!1") nil nil)) nil)) nil)) nil)) nil) ("8" (lemma "closed_intervals_compact") (("8" (inst - "A!1" "B!1") nil nil)) nil) ("9" (lemma "closed_intervals_compact") (("9" (inst - "A!1" "B!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "A!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (setof type-eq-decl nil defined_types nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (ext const-decl "set[real]" bounded_reals "reals/") (pred type-eq-decl nil defined_types nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (min const-decl "T" bounded_reals "reals/") (min_set type-eq-decl nil bounded_reals "reals/") (>= 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) (nnreal type-eq-decl nil real_types nil) (dist const-decl "nnreal" distance_3D "vectors/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (curried_min_is_cont_3D formula-decl nil vect3_Heine nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (q!1 skolem-const-decl "Vect3" vect3_Heine nil) (ball const-decl "set[T]" metric_spaces "analysis/") (y!1 skolem-const-decl "Vect3" vect3_Heine nil) (fullset const-decl "set" sets nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (product_cont_product_subset formula-decl nil cross_metric_cont "analysis/") (y!2 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (NOT const-decl "[bool -> bool]" booleans nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil) (A!1 skolem-const-decl "real" vect3_Heine nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (curried_min_is_cont_3D_ed-2 nil 3462099137 ("" (skosimp*) (("" (skoletin 1) (("1" (skosimp*) (("1" (lemma "curried_min_is_cont_3D") (("1" (inst - "A!1" "B!1") (("1" (prop) (("1" (assert) (("1" (replace -2 - rl) (("1" (expand "continuous?") (("1" (expand "continuous?") (("1" (inst - "y!1") (("1" (expand "continuous_at?") (("1" (inst - "epsilon!1") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "q!1") (("1" (assert) nil) ("2" (expand "fullset") (("2" (propax) nil))))))))))))))))))) ("2" (expand "fullset") (("2" (propax) nil))))))))))))) ("2" (hide 2) (("2" (lemma "product_cont_product_subset") (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!2") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (skosimp*) (("2" (inst - "x!1" "y!2" "epsilon!2") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil))))))))))))))))))))))))))))) ("2" (hide 2) (("2" (hide -) (("2" (lemma "curried_min_is_cont_TCC1") (("2" (skosimp*) (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("2" (case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)") (("1" (assert) (("1" (reveal -2) (("1" (label "cont_ed" -1) (("1" (label "nonempty" -2) (("1" (label "bigpred" -3) (("1" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (assert) nil))))) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil))))) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (assert) nil))))) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (expand "member") (("4" (inst - "f(A!1,y!1)") (("4" (inst + "A!1") nil))))))))) ("5" (lemma "product_cont_product_subset") (("5" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("5" (assert) (("5" (hide-all-but ("cont_ed" 1)) (("5" (skosimp*) (("5" (inst - "x!1" "y!2" "epsilon!1") (("5" (skosimp*) (("5" (inst + "delta!1") (("5" (skosimp*) (("5" (inst - "z!1" "w!1") (("5" (assert) nil))))))))))))))))))))) ("6" (lemma "product_cont_product_subset") (("6" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("6" (assert) (("6" (hide-all-but ("cont_ed" 1)) (("6" (skosimp*) (("6" (inst - "x!1" "y!2" "epsilon!1") (("6" (skosimp*) (("6" (inst + "delta!1") (("6" (skosimp*) (("6" (inst - "z!1" "w!1") (("6" (assert) nil))))))))))))))))))))) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (expand "member") (("7" (inst - "f(A!1,y!1)") (("7" (inst + "A!1") nil))))))))) ("8" (lemma "closed_intervals_compact") (("8" (inst - "A!1" "B!1") nil))) ("9" (lemma "closed_intervals_compact") (("9" (inst - "A!1" "B!1") nil))))))))))))))) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "A!1") (("2" (assert) nil)))))))))))))))))))))))) nil) ((min const-decl "T" bounded_reals "reals/") (min_set type-eq-decl nil bounded_reals "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (greatest_lower_bound const-decl "bool" bound_defs "reals/") (ext const-decl "set[real]" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (dist const-decl "nnreal" distance_3D "vectors/") (ball const-decl "set[T]" metric_spaces "analysis/") (product_cont_product_subset formula-decl nil cross_metric_cont "analysis/") (closed_intervals_compact formula-decl nil real_metric_space "analysis/") (curried_min_is_cont_TCC1 subtype-tcc nil cross_metric_real_fun "analysis/")) nil) (curried_min_is_cont_3D_ed-1 nil 3462098864 (";;; Proof curried_min_is_cont_3D_ed-1 for formula real_3D_problem.curried_min_is_co (skosimp*) ((";;; Proof curried_min_is_cont_3D_ed-1 for formula real_3D_problem.curried_min_is_c (skoletin 1) (("1" (skosimp*) (("1" (lemma "curried_min_is_cont_3D") (("1" (inst - "A!1" "B!1") (("1" (prop) (("1" (assert) (("1" (replace -2 - rl) (("1" (expand "continuous?") (("1" (expand "continuous?") (("1" (inst - "y!1") (("1" (expand "continuous_at?") (("1" (inst - "epsilon!1") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "q!1") (("1" (assert) nil) ("2" (expand "fullset") (("2" (propax) nil))))))))))))))))))) ("2" (expand "fullset") (("2" (propax) nil))))))))))))) ("2" (hide 2) (("2" (lemma "product_cont_product_subset") (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!2") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!2") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (skosimp*) (("2" (inst - "x!1" "y!2" "epsilon!2") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil))))))))))))))))))))))))))))) ("2" (hide 2) (("2" (hide -) (("2" (lemma "curried_min_is_cont_TCC1") (("2" (skosimp*) (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("2" (case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)") (("1" (assert) (("1" (reveal -2) (("1" (label "cont_ed" -1) (("1" (label "nonempty" -2) (("1" (label "bigpred" -3) (("1" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (assert) nil))))) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil))))) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (assert) nil))))) ("4" (expand "nonempty?") (("4" (expand "empty?") (("4" (expand "member") (("4" (inst - "f(A!1,y!1)") (("4" (inst + "A!1") nil))))))))) ("5" (lemma "product_cont_product_subset") (("5" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("5" (assert) (("5" (hide-all-but ("cont_ed" 1)) (("5" (skosimp*) (("5" (inst - "x!1" "y!2" "epsilon!1") (("5" (skosimp*) (("5" (inst + "delta!1") (("5" (skosimp*) (("5" (inst - "z!1" "w!1") (("5" (assert) nil))))))))))))))))))))) ("6" (lemma "product_cont_product_subset") (("6" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("6" (assert) (("6" (hide-all-but ("cont_ed" 1)) (("6" (skosimp*) (("6" (inst - "x!1" "y!2" "epsilon!1") (("6" (skosimp*) (("6" (inst + "delta!1") (("6" (skosimp*) (("6" (inst - "z!1" "w!1") (("6" (assert) nil))))))))))))))))))))) ("7" (expand "nonempty?") (("7" (expand "empty?") (("7" (expand "member") (("7" (inst - "f(A!1,y!1)") (("7" (inst + "A!1") nil))))))))) ("8" (lemma "closed_intervals_compact") (("8" (inst - "A!1" "B!1") nil))) ("9" (lemma "closed_intervals_compact") (("9" (inst - "A!1" "B!1") nil))))))))))))))) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "A!1") (("2" (assert) nil)))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (multiary_Heine_3D 0 (multiary_Heine_3D-3 nil 3462267300 ("" (skosimp*) (("" (lemma "multiary_Heine") (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("" (assert) (("" (prop) (("1" (lemma "closed_intervals_compact") (("1" (inst - "A!1" "B!1") nil nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((dist const-decl "nnreal" distance_3D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (multiary_Heine formula-decl nil cross_metric_uniform_continuity "analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (A!1 skolem-const-decl "real" vect3_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (y!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect3])]]))" vect3_Heine 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) (ball const-decl "set[T]" metric_spaces "analysis/") (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (closed_intervals_compact formula-decl nil real_metric_space "analysis/") (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (fullset const-decl "set" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (multiary_Heine_3D-2 nil 3462099162 ("" (skosimp*) (("" (lemma "multiary_Heine") (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("" (assert) (("" (prop) (("1" (lemma "closed_intervals_compact") (("1" (inst - "A!1" "B!1") nil))) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil)))))))))))))))))))))))) nil) ((dist const-decl "nnreal" distance_3D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (multiary_Heine formula-decl nil cross_metric_uniform_continuity "analysis/") (ball const-decl "set[T]" metric_spaces "analysis/") (closed_intervals_compact formula-decl nil real_metric_space "analysis/")) nil) (multiary_Heine_3D-1 nil 3462098883 (";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" (skosimp*) ((";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" (lemma "multiary_Heine") ((";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") ((";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" (assert) ((";;; Proof multiary_Heine_3D-1 for formula real_3D_problem.multiary_Heine_3D" (prop) (("1" (lemma "closed_intervals_compact") (("1" (inst - "A!1" "B!1") nil))) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil)))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (multiary_Heine_3D_ed 0 (multiary_Heine_3D_ed-3 nil 3462267342 ("" (skosimp*) (("" (lemma "multiary_Heine_3D") (("" (inst - "f!1" "A!1" "B!1") (("" (expand "uniformly_continuous_in_first?") (("" (prop) (("1" (inst - "y1!1" "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "x1!1" "x2!1" "y2!1") (("1" (assert) nil nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "product_cont_product_subset") (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f!1") (("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!2") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil nil)) nil) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil) ("4" (expand "fullset") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!2") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((multiary_Heine_3D formula-decl nil vect3_Heine nil) (uniformly_continuous_in_first? const-decl "bool" cross_metric_cont "analysis/") (dist const-decl "nnreal" distance_3D "vectors/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (nnreal type-eq-decl nil real_types nil) (product_cont_product_subset formula-decl nil cross_metric_cont "analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (member const-decl "bool" sets nil) (y!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (NOT const-decl "[bool -> bool]" booleans nil) (x!1 skolem-const-decl "(extend [[real, Vect3], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect3]]))" vect3_Heine nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect3_Heine nil) (A!1 skolem-const-decl "real" vect3_Heine nil) (ball const-decl "set[T]" metric_spaces "analysis/") (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (y1!1 skolem-const-decl "Vect3" vect3_Heine 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) (y2!1 skolem-const-decl "Vect3" vect3_Heine nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (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) (multiary_Heine_3D_ed-2 nil 3462099184 ("" (skosimp*) (("" (lemma "multiary_Heine_3D") (("" (inst - "A!1" "B!1") (("" (expand "uniformly_continuous_in_first?") (("" (prop) (("1" (inst - "y1!1" "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "x1!1" "x2!1" "y2!1") (("1" (assert) nil) ("2" (expand "fullset") (("2" (propax) nil))))))))))) ("2" (expand "fullset") (("2" (propax) nil))))) ("2" (lemma "product_cont_product_subset") (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!2") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!2") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil)))))))))))))))))))))))))))) nil) ((uniformly_continuous_in_first? const-decl "bool" cross_metric_cont "analysis/") (dist const-decl "nnreal" distance_3D "vectors/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (product_cont_product_subset formula-decl nil cross_metric_cont "analysis/") (ball const-decl "set[T]" metric_spaces "analysis/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/")) nil) (multiary_Heine_3D_ed-1 nil 3462098901 (";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" (skosimp*) ((";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" (lemma "multiary_Heine_3D") ((";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" (inst - "A!1" "B!1") ((";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" (expand "uniformly_continuous_in_first?") ((";;; Proof multiary_Heine_3D_ed-1 for formula real_3D_problem.multiary_Heine_3D_ed" (prop) (("1" (inst - "y1!1" "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "x1!1" "x2!1" "y2!1") (("1" (assert) nil) ("2" (expand "fullset") (("2" (propax) nil))))))))))) ("2" (expand "fullset") (("2" (propax) nil))))) ("2" (lemma "product_cont_product_subset") (("2" (inst - "closed_intv(A!1,B!1)" "fullset[Vect3]" "f") (("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "continuous?") (("1" (expand "continuous_at?") (("1" (expand "member") (("1" (expand "ball") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "epsilon!2") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "y!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil))))) ("4" (expand "fullset") (("4" (propax) nil))))))))))))))))))))) ("2" (skosimp*) (("2" (inst - "x!1" "y!1" "epsilon!2") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "z!1" "w!1") (("2" (assert) nil)))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)))
¤ 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.158Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26