(test_cont
(IMP_continuity_subspace_TCC1 0
(IMP_continuity_subspace_TCC1-1 nil 3431788742
("" (expand "metric?")
(("" (expand "metric_zero?")
(("" (expand "metric_symmetric?")
(("" (expand "metric_triangle?") (("" (grind) nil nil)) nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(metric_zero? const-decl "bool" metric_def nil)
(metric_triangle? const-decl "bool" metric_def nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(metric_symmetric? const-decl "bool" metric_def nil)
(metric? const-decl "bool" metric_def nil))
nil))
(recip_continuous_TCC1 0
(recip_continuous_TCC1-1 nil 3431795137
("" (expand "restrict")
(("" (expand "metric?")
(("" (expand "metric_zero?")
(("" (expand "metric_symmetric?")
(("" (expand "metric_triangle?") (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((metric? const-decl "bool" metric_def nil)
(metric_symmetric? const-decl "bool" metric_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal 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)
(nzreal nonempty-type-eq-decl nil reals 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(metric_triangle? const-decl "bool" metric_def nil)
(metric_zero? const-decl "bool" metric_def nil)
(restrict const-decl "R" restrict nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(recip_continuous 0
(recip_continuous-1 nil 3431788749
("" (expand "metric_continuous?")
(("" (skosimp)
(("" (expand "metric_continuous_at?")
(("" (skosimp)
(("" (expand "member")
(("" (expand "ball")
(("" (expand "restrict")
((""
(case "forall (x,y:nzreal): 1 / x - 1 / y = (y-x)/(x*y)")
(("1"
(case "FORALL (x, y: nzreal,delta:posreal): abs(x-y) (abs(x)/2)
(("1"
(inst +
"min(abs(x!1)/3,epsilon!1*(abs(x!1)*abs(x!1)/2))")
(("1" (skosimp)
(("1" (inst -2 "x!1" "x!2")
(("1" (replace -2)
(("1" (rewrite "abs_div")
(("1"
(rewrite "abs_mult")
(("1"
(rewrite "div_mult_pos_lt1" 1)
(("1"
(inst
-
"x!1"
"x!2"
"min(abs(x!1) / 3, epsilon!1 * (abs(x!1) * abs(x!1) / 2))")
(("1"
(assert)
(("1"
(flatten)
(("1"
(lemma
"both_sides_times_pos_lt1"
("pz"
"epsilon!1 * abs(x!1)"
"x"
"abs(x!1) / 2"
"y"
"abs(x!2)"))
(("1"
(assert)
(("1"
(hide -4 -2 -3)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(ball const-decl "set[T]" metric_space_def 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(abs_div formula-decl nil real_props nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs_mult formula-decl nil real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(restrict const-decl "R" restrict nil)
(member const-decl "bool" sets nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(metric_continuous_at? const-decl "bool" metric_continuity nil)
(metric_continuous? const-decl "bool" metric_continuity nil))
shostak)))
¤ Dauer der Verarbeitung: 0.3 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.
|
