|
(cross_metric_real_fun
(IMP_cross_metric_uniform_continuity_TCC1 0
(IMP_cross_metric_uniform_continuity_TCC1-1 nil 3460386756
("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil)
((fullset_metric_space1 formula-decl nil cross_metric_real_fun nil))
nil))
(IMP_cross_metric_uniform_continuity_TCC2 0
(IMP_cross_metric_uniform_continuity_TCC2-1 nil 3460386756
("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil)
((fullset_metric_space2 formula-decl nil cross_metric_real_fun nil))
nil))
(IMP_cross_metric_uniform_continuity_TCC3 0
(IMP_cross_metric_uniform_continuity_TCC3-1 nil 3460386756
("" (expand "metric_space?")
(("" (expand "space_zero?")
(("" (expand "space_symmetric?")
(("" (expand "space_triangle?") (("" (grind) nil nil)) nil))
nil))
nil))
nil)
((space_zero? const-decl "bool" metric_spaces_def nil)
(space_triangle? const-decl "bool" metric_spaces_def nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_dist const-decl "nnreal" real_metric_space nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(space_symmetric? const-decl "bool" metric_spaces_def nil)
(metric_space? const-decl "bool" metric_spaces_def nil))
nil))
(curried_min_exists 0
(curried_min_exists-1 nil 3461589573
("" (skosimp*)
(("" (label "nonempty" -1)
(("" (label "cont" -2)
(("" (label "compact" -3)
(("" (label "t1in" -4)
(("" (label "final" 1)
(("" (lemma "cont_on_compact_min")
(("" (inst - "X!1" "(LAMBDA (x: T1): f!1(x,t!1))")
(("" (lemma "curried_is_uniform")
(("" (inst - "X!1" "Y!1" "f!1")
(("" (lemma "multiary_Heine")
(("" (inst - "X!1" "Y!1" "f!1")
(("" (lemma "unif_cont_implies_cont")
((""
(inst - "X!1"
"(LAMBDA (x: T1): f!1(x,t!1))")
((""
(assert)
((""
(inst - "t!1")
((""
(assert)
((""
(expand "nonempty?")
((""
(assert)
((""
(label "contLam" -1)
((""
(label "ucif" -2)
((""
(label "uclam" -3)
((""
(label "min_exists" -4)
((""
(prop)
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(skosimp*)
(("1"
(inst
"final"
"f!1(x!1,t!1)")
(("1"
(inst
+
"x!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"below_bounded")
(("2"
(lemma
"axiom_of_archimedes")
(("2"
(skosimp*)
(("2"
(inst
-1
"-f!1(s!1,t!1)")
(("2"
(skosimp*)
(("2"
(inst
+
"-i!1-2")
(("2"
(expand
"lower_bound")
(("2"
(skosimp*)
(("2"
(typepred
"z!1")
(("2"
(skosimp*)
(("2"
(inst
"min_exists"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(expand "ext")
(("3"
(skosimp*)
(("3"
(inst + "s!1")
(("3"
(lemma
"inf_def")
(("3"
(inst
-1
"{r: real | EXISTS (x: (X!1)): r = f!1(x, t!1)}"
"f!1(s!1,t!1)")
(("1"
(replace
-1)
(("1"
(expand
"greatest_lower_bound")
(("1"
(expand
"lower_bound")
(("1"
(split)
(("1"
(skosimp*)
(("1"
(typepred
"z!1")
(("1"
(skosimp*)
(("1"
(inst
"min_exists"
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst
-
"f!1(s!1,t!1)")
(("2"
(inst
+
"s!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"nonempty?")
(("2"
(split)
(("1"
(expand
"empty?")
(("1"
(expand
"member")
(("1"
(skosimp*)
(("1"
(inst
-
"f!1(x!1,t!1)")
(("1"
(inst
+
"x!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"below_bounded")
(("2"
(lemma
"axiom_of_archimedes")
(("2"
(inst
-
"-f!1(s!1,t!1)")
(("2"
(skosimp*)
(("2"
(inst
+
"-i!1-2")
(("2"
(expand
"lower_bound")
(("2"
(skosimp*)
(("2"
(typepred
"z!1")
(("2"
(skosimp*)
(("2"
(inst
"min_exists"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(skosimp*)
(("4"
(inst + "s!1")
(("4"
(skosimp*)
(("4"
(inst
-
"y!1")
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T2 formal-nonempty-type-decl nil cross_metric_real_fun nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "T1" cross_metric_real_fun nil)
(X!1 skolem-const-decl "set[T1]" cross_metric_real_fun nil)
(empty? const-decl "bool" sets nil)
(axiom_of_archimedes formula-decl nil real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(lower_bound const-decl "bool" bound_defs "reals/")
(minus_int_is_int application-judgement "int" integers nil)
(below_bounded const-decl "bool" bounded_reals "reals/")
(inf_def formula-decl nil bounded_reals "reals/")
(x!1 skolem-const-decl "T1" cross_metric_real_fun nil)
(s!1 skolem-const-decl "(X!1)" cross_metric_real_fun nil)
(greatest_lower_bound const-decl "bool" bound_defs "reals/")
(inf_set type-eq-decl nil bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(t!1 skolem-const-decl "T2" cross_metric_real_fun nil)
(f!1 skolem-const-decl "[[T1, T2] -> real]" cross_metric_real_fun
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(ext const-decl "set[real]" bounded_reals "reals/")
(unif_cont_implies_cont formula-decl nil uniform_continuity nil)
(multiary_Heine formula-decl nil cross_metric_uniform_continuity
nil)
(curried_is_uniform formula-decl nil cross_metric_cont nil)
(d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_real_fun
nil)
(real_dist const-decl "nnreal" real_metric_space nil)
(cont_on_compact_min formula-decl nil real_fun_on_compact_sets nil)
(T1 formal-nonempty-type-decl nil cross_metric_real_fun nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_real_fun
nil))
nil))
(curried_min_is_cont_TCC1 0
(curried_min_is_cont_TCC1-1 nil 3460892462
("" (skosimp*)
(("" (label "nonempty" -1)
(("" (label "cont" -2)
(("" (label "compact" -3)
(("" (label "t1in" -4)
(("" (label "final" 1)
(("" (lemma "cont_on_compact_min")
(("" (inst - "X!1" "(LAMBDA (x: T1): f!1(x,t!1))")
(("" (lemma "curried_is_uniform")
(("" (inst - "X!1" "Y!1" "f!1")
(("" (lemma "multiary_Heine")
(("" (inst - "X!1" "Y!1" "f!1")
(("" (lemma "unif_cont_implies_cont")
((""
(inst - "X!1"
"(LAMBDA (x: T1): f!1(x,t!1))")
((""
(assert)
((""
(inst - "t!1")
((""
(assert)
((""
(expand "nonempty?")
((""
(assert)
((""
(label "contLam" -1)
((""
(label "ucif" -2)
((""
(label "uclam" -3)
((""
(label "min_exists" -4)
((""
(prop)
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(skosimp*)
(("1"
(inst
"final"
"f!1(x!1,t!1)")
(("1"
(inst
+
"x!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"below_bounded")
(("2"
(lemma
"axiom_of_archimedes")
(("2"
(skosimp*)
(("2"
(inst
-1
"-f!1(s!1,t!1)")
(("2"
(skosimp*)
(("2"
(inst
+
"-i!1-2")
(("2"
(expand
"lower_bound")
(("2"
(skosimp*)
(("2"
(typepred
"z!1")
(("2"
(skosimp*)
(("2"
(inst
"min_exists"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(expand "ext")
(("3"
(skosimp*)
(("3"
(inst + "s!1")
(("3"
(lemma
"inf_def")
(("3"
(inst
-1
"{r: real | EXISTS (x: (X!1)): r = f!1(x, t!1)}"
"f!1(s!1,t!1)")
(("1"
(replace
-1)
(("1"
(expand
"greatest_lower_bound")
(("1"
(expand
"lower_bound")
(("1"
(split)
(("1"
(skosimp*)
(("1"
(typepred
"z!1")
(("1"
(skosimp*)
(("1"
(inst
"min_exists"
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst
-
"f!1(s!1,t!1)")
(("2"
(inst
+
"s!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"nonempty?")
(("2"
(split)
(("1"
(expand
"empty?")
(("1"
(expand
"member")
(("1"
(skosimp*)
(("1"
(inst
-
"f!1(x!1,t!1)")
(("1"
(inst
+
"x!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"below_bounded")
(("2"
(lemma
"axiom_of_archimedes")
(("2"
(inst
-
"-f!1(s!1,t!1)")
(("2"
(skosimp*)
(("2"
(inst
+
"-i!1-2")
(("2"
(expand
"lower_bound")
(("2"
(skosimp*)
(("2"
(typepred
"z!1")
(("2"
(skosimp*)
(("2"
(inst
"min_exists"
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T2 formal-nonempty-type-decl nil cross_metric_real_fun nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "T1" cross_metric_real_fun nil)
(X!1 skolem-const-decl "set[T1]" cross_metric_real_fun nil)
(empty? const-decl "bool" sets nil)
(axiom_of_archimedes formula-decl nil real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(lower_bound const-decl "bool" bound_defs "reals/")
(minus_int_is_int application-judgement "int" integers nil)
(below_bounded const-decl "bool" bounded_reals "reals/")
(inf_def formula-decl nil bounded_reals "reals/")
(x!1 skolem-const-decl "T1" cross_metric_real_fun nil)
(s!1 skolem-const-decl "(X!1)" cross_metric_real_fun nil)
(greatest_lower_bound const-decl "bool" bound_defs "reals/")
(inf_set type-eq-decl nil bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(t!1 skolem-const-decl "T2" cross_metric_real_fun nil)
(f!1 skolem-const-decl "[[T1, T2] -> real]" cross_metric_real_fun
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(ext const-decl "set[real]" bounded_reals "reals/")
(unif_cont_implies_cont formula-decl nil uniform_continuity nil)
(multiary_Heine formula-decl nil cross_metric_uniform_continuity
nil)
(curried_is_uniform formula-decl nil cross_metric_cont nil)
(d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_real_fun
nil)
(real_dist const-decl "nnreal" real_metric_space nil)
(cont_on_compact_min formula-decl nil real_fun_on_compact_sets nil)
(T1 formal-nonempty-type-decl nil cross_metric_real_fun nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_real_fun
nil))
nil))
(curried_min_is_cont 0
(curried_min_is_cont-1 nil 3460390218
("" (skosimp*)
(("" (label "compact" -1)
(("" (label "continuous" -2)
(("" (label "nonempty" -3)
(("" (label "final" 1)
(("" (assert)
(("" (lemma "multi_Heine_Corollary1")
(("" (inst?)
(("" (assert)
(("" (lemma "cont_on_compact_min")
(("" (label "cocm" -1)
(("" (label "mhc1" -2)
(("" (lemma "curried_is_uniform")
(("" (label "cmic" -1)
((""
(lemma "multiary_Heine")
((""
(inst?)
((""
(assert)
((""
(label "ucif" -1)
((""
(inst "cmic" "X!1" "Y!1" "f!1")
((""
(assert)
((""
(expand
"continuous?"
"final")
((""
(skosimp*)
((""
(typepred "x!1")
((""
(label "tpx!1" -1)
((""
(expand
"continuous_at?")
((""
(expand "member")
((""
(expand "ball")
((""
(expand
"real_dist")
((""
(skosimp*)
((""
(inst
"mhc1"
"x!1"
"epsilon!1")
((""
(skosimp*)
((""
(inst
"final"
"delta!1")
((""
(skosimp*)
((""
(typepred
"y!1")
((""
(label
"tpy!1"
-1)
((""
(name
"main_min"
"min({r: real | EXISTS (x: (X!1)): r = f!1(x, x!1)})")
(("1"
(label
"main_min"
-1)
(("1"
(name
"sec_min"
"min({r: real | EXISTS (x: (X!1)): r = f!1(x, y!1)})")
(("1"
(label
"sec_min"
-1)
(("1"
(replace
"main_min")
(("1"
(replace
"sec_min")
(("1"
(name
"main_slice"
"{r: real | EXISTS (x: (X!1)): r = f!1(x, x!1)}")
(("1"
(label
"main_slice"
-1)
(("1"
(name
"sec_slice"
"{r: real | EXISTS (x: (X!1)): r = f!1(x, y!1)}")
(("1"
(label
"sec_slice"
-1)
(("1"
(replace
"main_slice")
(("1"
(replace
"sec_slice")
(("1"
(inst-cp
"cmic"
"x!1")
(("1"
(inst
"cmic"
"y!1")
(("1"
(lemma
"unif_cont_implies_cont")
(("1"
(inst-cp
-1
"X!1"
"LAMBDA (t: T1): f!1(t, y!1)")
(("1"
(inst-cp
-1
"X!1"
"LAMBDA (t: T1): f!1(t, x!1)")
(("1"
(hide
-1)
(("1"
(label
"cmicx"
-1)
(("1"
(label
"cmicy"
-2)
(("1"
(hide
"cmic")
(("1"
(copy
"cocm")
(("1"
(hide
"cocm")
(("1"
(inst-cp
-1
"X!1"
"LAMBDA (t: T1): f!1(t, x!1)")
(("1"
(label
"cocmx"
-2)
(("1"
(inst
-1
"X!1"
"LAMBDA (t: T1): f!1(t, y!1)")
(("1"
(label
"comcy"
-1)
(("1"
(hide
("tpy!1"
"tpx!1"))
(("1"
(lemma
"curried_is_uniform")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"nonempty?")
(("1"
(prop)
(("1"
(skosimp*)
(("1"
(expand
"min")
(("1"
(lemma
"inf_def")
(("1"
(inst-cp
-1
"main_slice"
"f!1(s!1,x!1)")
(("1"
(inst
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.65 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.
|
