| products/sources/formale sprachen/PVS/vect_analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: table.vdmpp Sprache: PostscriptOriginal von: PVS© |
|
||||||
|
(vect2_Heine
(IMP_cross_metric_real_fun_TCC1 0 (IMP_cross_metric_real_fun_TCC1-1 nil 3476029646 ("" (rewrite "real_metric_space") nil nil) ((fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_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 3476029646 ("" (rewrite "vect2_metric_space") nil nil) ((vect2_metric_space formula-decl nil vect2_metric_space nil)) nil)) (curried_min_exists_2D_TCC1 0 (curried_min_exists_2D_TCC1-1 nil 3610811549 ("" (subtype-tcc) nil nil) nil nil)) (curried_min_exists_2D 0 (curried_min_exists_2D-2 nil 3476029922 ("" (lemma "curried_min_exists") (("" (skosimp*) (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "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[Vect2]" "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" vect2_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect2_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_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, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_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, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_Heine nil) (y!2 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_Heine nil) (y!2 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_Heine nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_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/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (dist const-decl "nnreal" distance_2D "vectors/")) nil) (curried_min_exists_2D-1 nil 3476029872 ("" (lemma "curried_min_exists") (("" (skosimp*) (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1") (("" (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" (prop) nil))))) ("2" (inst - "y!1") (("2" (expand "fullset") (("2" (assert) nil))))) ("4" (inst - "y!1") (("4" (expand "fullset") (("4" (prop) 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" (inst - "(A!1 + B!1)/2") (("7" (expand "member") (("7" (propax) nil))))))))) ("8" (expand "nonempty?") (("8" (expand "empty?") (("8" (expand "member") (("8" (inst - "(A!1 + B!1)/2") (("8" (assert) nil))))))))) ("9" (expand "nonempty?") (("9" (expand "empty?") (("9" (expand "member") (("9" (inst - "f!1(A!1,y!1)") (("9" (inst + "A!1") 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) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (prop) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) 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) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))))))))))))))) ("12" (expand "nonempty?") (("12" (expand "empty?") (("12" (expand "member") (("12" (inst - "f!1(A!1,y!1)") (("12" (inst + "A!1") 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) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (prop) nil))))) ("2" (typepred "y!2") (("2" (expand "extend") (("2" (assert) nil))))))))))))))))))))))) ("2" (expand "extend") (("2" (prop) (("1" (expand "fullset") (("1" (propax) nil))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))) ("2" (typepred "x!1") (("2" (expand "extend") (("2" (assert) nil))))))))))))))))))) ("14" (lemma "curried_min_exists") (("14" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1") (("14" (assert) (("14" (prop) (("1" (inst - "y!1") (("1" (expand "fullset") (("1" (propax) nil))))) ("2" (lemma "closed_intervals_compact") (("2" (inst - "A!1" "B!1") nil))))))))))) ("15" (lemma "closed_intervals_compact") (("15" (inst - "A!1" "B!1") nil))) ("16" (lemma "closed_intervals_compact") (("16" (inst - "A!1" "B!1") nil)))))))))) nil) nil nil)) (curried_min_is_cont_2D_TCC1 0 (curried_min_is_cont_2D_TCC1-2 nil 3476029777 ("" (lemma "curried_min_exists") (("" (skosimp*) (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "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" (prop) nil nil)) nil)) nil) ("3" (inst - "y!1") (("3" (expand "fullset") (("3" (assert) 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" (assert) nil nil)) nil)) nil) ("3" (typepred "y!2") (("3" (expand "extend") (("3" (prop) 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[Vect2]" "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" vect2_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect2_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_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, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_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, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_Heine nil) (y!2 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_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/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (dist const-decl "nnreal" distance_2D "vectors/")) nil) (curried_min_is_cont_2D_TCC1-1 nil 3476029646 ("" (subtype-tcc) nil nil) nil nil)) (curried_min_is_cont_2D 0 (curried_min_is_cont_2D-1 nil 3476030045 ("" (skosimp*) (("" (lemma "curried_min_is_cont") (("" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "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_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_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" vect2_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect2_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_Heine nil) (ball const-decl "set[T]" metric_spaces "analysis/") (y!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool, FALSE] (fullset [[(LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" vect2_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_2D_ed_TCC1 0 (curried_min_is_cont_2D_ed_TCC1-2 nil 3476029826 ("" (lemma "curried_min_is_cont_2D_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[Vect2]" "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[Vect2]" "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[Vect2]" "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" vect2_Heine nil) (B!1 skolem-const-decl "{x: real | A!1 < x}" vect2_Heine nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" vect2_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, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" vect2_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_2D "vectors/") (y!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" vect2_Heine nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" vect2_Heine nil) (y!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" vect2_Heine nil) (x!1 skolem-const-decl "(extend [[real, Vect2], [(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2], bool, FALSE] (fullset[[(LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" vect2_Heine nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_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_2D_TCC1 subtype-tcc nil vect2_Heine nil)) nil) (curried_min_is_cont_2D_ed_TCC1-1 nil 3476029646 ("" (subtype-tcc) nil nil) nil nil)) (curried_min_is_cont_2D_ed 0 (curried_min_is_cont_2D_ed-3 nil 3476030194 ("" (skosimp*) (("" (skoletin 1) (("1" (skosimp*) (("1" (lemma "curried_min_is_cont_2D") (("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[Vect2]" "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" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.98 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
