|
(cont_real_vect2
(continuity_def 0
(continuity_def-1 nil 3302273405
("" (skosimp*)
(("" (split +)
(("1" (expand "continuous_rv?")
(("1" (expand "convergence") (("1" (flatten) nil nil)) nil))
nil)
("2" (flatten)
(("2" (expand "convergence")
(("2" (expand "continuous_rv?") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((convergence const-decl "bool" limit_real_vect2 nil)
(continuous_rv? const-decl "bool" cont_real_vect2 nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(continuity_def2 0
(continuity_def2-1 nil 3302273405
("" (skosimp*)
(("" (rewrite "continuity_def")
(("" (rewrite "convergent_in_domain") (("" (assert) nil nil))
nil))
nil))
nil)
((continuity_def formula-decl nil cont_real_vect2 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)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(convergent_in_domain formula-decl nil limit_real_vect2 nil))
nil))
(continuous_iff_comps 0
(continuous_iff_comps-1 nil 3474200152
("" (skosimp*)
(("" (split +)
(("1" (flatten)
(("1" (expand "continuous?")
(("1" (expand "continuous_rv?")
(("1" (split +)
(("1" (skosimp*)
(("1" (inst - "epsilon!1")
(("1" (skosimp*)
(("1" (inst + delta!1)
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert)
(("1" (hide -1)
(("1"
(lemma "norm_ge_comps")
(("1"
(inst?)
(("1"
(expand "-")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst - "epsilon!1")
(("2" (skosimp*)
(("2" (inst + delta!1)
(("2" (skosimp*)
(("2" (inst?)
(("2" (assert)
(("2" (hide -1)
(("2"
(lemma "norm_ge_comps")
(("2"
(inst?)
(("2"
(flatten)
(("2"
(hide -1)
(("2"
(expand "-")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "continuous_rv?")
(("2" (expand "continuous?")
(("2" (skosimp*)
(("2" (inst -1 "epsilon!1/sqrt(2)")
(("2" (inst -2 "epsilon!1/sqrt(2)")
(("2" (skosimp*)
(("2" (inst + "min(delta!1,delta!2)")
(("2" (skeep)
(("2" (inst - "x")
(("2" (inst - "x")
(("2" (assert)
(("2"
(lemma "sq_lt")
(("2"
(inst
-
"norm(f!1(x) - f!1(a!1))"
"epsilon!1")
(("2"
(assert)
(("2"
(hide 2)
(("2"
(lemma "sq_lt")
(("2"
(inst
-
"abs(f!1(x)`x - f!1(a!1)`x)"
"epsilon!1 / sqrt(2)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(lemma "sq_lt")
(("2"
(inst
-
"abs(f!1(x)`y - f!1(a!1)`y)"
"epsilon!1 / sqrt(2)")
(("2"
(assert)
(("2"
(hide -3)
(("2"
(add-formulas
-1
-2)
(("2"
(case-replace
"2 * sq(epsilon!1 / sqrt(2)) = sq(epsilon!1)")
(("1"
(case
"sq(norm(f!1(x) - f!1(a!1))) = sq(f!1(x)`x - f!1(a!1)`x) + sq(f!1(x)`y - f!1(a!1)`y)")
(("1"
(assert)
nil
nil)
("2"
(hide
-
2)
(("2"
(rewrite
"sq_norm")
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
(("2"
(field
1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(continuous? const-decl "bool" continuous_functions "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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(norm_ge_comps formula-decl nil vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(continuous_rv? const-decl "bool" cont_real_vect2 nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq_norm formula-decl nil vectors_2D "vectors/")
(times_div1 formula-decl nil real_props nil)
(div_times formula-decl nil real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_abs formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_lt formula-decl nil sq "reals/")
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types 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)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil))
(cont_rv_iff_comps 0
(cont_rv_iff_comps-1 nil 3474198054
("" (skosimp*)
(("" (split +)
(("1" (flatten)
(("1" (expand "continuous?")
(("1" (expand "continuous_rv?")
(("1" (expand "continuous_rv?")
(("1" (expand "continuous?")
(("1" (split +)
(("1" (skeep)
(("1" (skosimp*)
(("1" (inst - x0)
(("1" (inst - "epsilon!1")
(("1" (skosimp*)
(("1" (inst + delta!1)
(("1"
(skosimp*)
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide -1)
(("1"
(lemma "norm_ge_comps")
(("1"
(inst?)
(("1"
(expand "-")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skosimp*)
(("2" (inst - x0)
(("2" (inst - "epsilon!1")
(("2" (skosimp*)
(("2" (inst + delta!1)
(("2"
(skosimp*)
(("2"
(inst?)
(("2"
(assert)
(("2"
(hide -1)
(("2"
(lemma "norm_ge_comps")
(("2"
(inst?)
(("2"
(flatten)
(("2"
(hide -1)
(("2"
(expand "-")
(("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)
("2" (flatten)
(("2" (expand "continuous_rv?")
(("2" (expand "continuous?")
(("2" (expand "continuous_rv?")
(("2" (expand "continuous?")
(("2" (skeep)
(("2" (skosimp*)
(("2" (inst - x0)
(("2" (inst -2 x0)
(("2" (inst -1 "epsilon!1/sqrt(2)")
(("2" (inst -2 "epsilon!1/sqrt(2)")
(("2" (skosimp*)
(("2"
(inst + "min(delta!1,delta!2)")
(("2"
(skeep)
(("2"
(inst - "x")
(("2"
(inst - "x")
(("2"
(assert)
(("2"
(lemma "sq_lt")
(("2"
(inst
-
"norm(f!1(x) - f!1(x0))"
"epsilon!1")
(("2"
(assert)
(("2"
(hide 2)
(("2"
(lemma "sq_lt")
(("2"
(inst
-
"abs(f!1(x)`x - f!1(x0)`x)"
"epsilon!1 / sqrt(2)")
(("2"
(assert)
(("2"
(hide -2)
(("2"
(lemma
"sq_lt")
(("2"
(inst
-
"abs(f!1(x)`y - f!1(x0)`y)"
"epsilon!1 / sqrt(2)")
(("2"
(assert)
(("2"
(hide
-3)
(("2"
(add-formulas
-1
-2)
(("2"
(case-replace
"2 * sq(epsilon!1 / sqrt(2)) = sq(epsilon!1)")
(("1"
(case
"sq(norm(f!1(x) - f!1(x0))) = sq(f!1(x)`x - f!1(x0)`x) + sq(f!1(x)`y - f!1(x0)`y)")
(("1"
(assert)
nil
nil)
("2"
(hide
-
2)
(("2"
(rewrite
"sq_norm")
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
(("2"
(field
1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous? const-decl "bool" continuous_functions "analysis/")
(real_minus_real_is_real application-judgement "real" reals nil)
(continuous_rv? const-decl "bool" cont_real_vect2 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)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(norm_ge_comps formula-decl nil vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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)
(continuous? const-decl "bool" continuous_functions "analysis/")
(continuous_rv? const-decl "bool" cont_real_vect2 nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(sq_lt formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_abs formula-decl nil sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(div_times formula-decl nil real_props nil)
(times_div1 formula-decl nil real_props nil)
(sq_norm formula-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil))
nil))
(sum_continuous_rv 0
(sum_continuous_rv-1 nil 3302273405
(""
(grind :defs nil :rewrites
("continuity_def2" "sum_fun_convergent[T]"))
nil 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)
(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)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(sum_fun_convergent formula-decl nil limit_real_vect2 nil)
(continuity_def2 formula-decl nil cont_real_vect2 nil))
nil))
(diff_continuous_rv 0
(diff_continuous_rv-3 nil 3473595198
(""
(grind :defs nil :rewrites
("continuity_def2" "diff_fun_convergent[T]"))
nil 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)
(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)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(diff_fun_convergent formula-decl nil limit_real_vect2 nil)
(continuity_def2 formula-decl nil cont_real_vect2 nil))
nil)
(diff_continuous_rv-2 nil 3442334818
(""
(grind :defs nil :rewrites
("continuity_def2" "diff_fun_convergent"))
nil nil)
((diff_fun_convergent formula-decl nil limit_real_vect2 nil)) nil)
(diff_continuous_rv-1 nil 3302273405
(""
(grind :defs nil :rewrites
("continuity_def2" "diff_fun_convergent"))
nil nil)
nil nil))
(const_continuous_rv 0
(const_continuous_rv-1 nil 3302273405
("" (skosimp*)
(("" (rewrite "continuity_def2")
(("" (lemma "const_fun_convergent")
(("" (expand "const_vfun") (("" (inst?) nil nil)) nil)) nil))
nil))
nil)
((continuity_def2 formula-decl nil cont_real_vect2 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)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(const_vfun const-decl "[T -> Vect2]" vect_fun_ops_rv nil)
(const_fun_convergent formula-decl nil limit_real_vect2 nil))
nil))
(scal_continuous_rv 0
(scal_continuous_rv-1 nil 3445183264
("" (skeep)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (case "abs(a) = 0")
(("1" (case-replace "a = 0")
(("1" (inst + "100")
(("1" (skosimp*)
(("1" (hide -)
(("1"
(case-replace "(0 * f)(x!1) - (0 * f)(x0) = zero")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (grind)
(("2" (apply-extensionality 1 :hide? t) nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2)
(("2" (lemma "abs_eq_0")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (inst - "epsilon!1/abs(a)")
(("1" (skosimp*)
(("1" (inst + delta!1)
(("1" (skosimp*)
(("1" (inst - x!1)
(("1" (assert)
(("1" (cross-mult -1)
(("1" (assert)
(("1" (expand "*")
(("1" (lemma "norm_scal")
(("1"
(inst - a "f(x!1) - f(x0)")
(("1"
(assert)
(("1"
(replace -1 * rl)
(("1"
(hide -1)
(("1"
(grind :exclude "norm")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide 2)
(("2" (case "epsilon!1 / abs(a) > 0")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (case "abs(a) = 0")
(("1" (propax) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(continuous_rv? const-decl "bool" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_eq_0 formula-decl nil abs_lems "reals/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(comp_zero_y formula-decl nil vectors_2D "vectors/")
(comp_zero_x formula-decl nil vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(scal_0 formula-decl nil vectors_2D "vectors/")
(neg_zero formula-decl nil vectors_2D "vectors/")
(sub_zero_left formula-decl nil vectors_2D "vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(norm_scal formula-decl nil vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(epsilon!1 skolem-const-decl "posreal" cont_real_vect2 nil)
(a skolem-const-decl "T" cont_real_vect2 nil)
(/= const-decl "boolean" notequal nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(prod_continuous_rv 0
(prod_continuous_rv-3 nil 3474199783
("" (skosimp*)
(("" (lemma "continuous_iff_comps")
(("" (inst - "x0!1" "hh!1 * f!1")
(("" (assert)
(("" (hide 2)
(("" (lemma "continuous_iff_comps")
(("" (inst?)
(("" (assert)
(("" (hide -3)
(("" (flatten)
(("" (lemma prod_continuous)
((""
(inst - "(LAMBDA (t: T): hh!1(t))"
"(LAMBDA (t: T): f!1(t)`x)" "x0!1")
(("" (expand "*" -1)
(("" (assert)
((""
(split -1)
(("1"
(assert)
(("1"
(expand "*" 1)
(("1"
(expand "*")
(("1"
(hide -1 -2)
(("1"
(lemma prod_continuous)
(("1"
(inst
-
"(LAMBDA (t: T): hh!1(t))"
"(LAMBDA (t: T): f!1(t)`y)"
"x0!1")
(("1"
(expand "*" -1)
(("1"
(case-replace
"(LAMBDA (t: T): hh!1(t)) = hh!1")
(("1" (assert) nil nil)
("2"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace
"(LAMBDA (t: T): hh!1(t)) = hh!1")
(("2"
(apply-extensionality 1 :hide? t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous_iff_comps formula-decl nil cont_real_vect2 nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "Vector" vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(prod_continuous formula-decl nil continuous_functions "analysis/")
(* const-decl "[T -> Vect2]" vect_fun_ops_rv nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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))
nil)
(prod_continuous_rv-2 nil 3473596718
("" (skosimp*)
(("" (lemma "cont_rv_iff_comps")
(("" (inst - "hh!1 * f!1")
(("" (assert)
(("" (flatten)
(("" (hide -1)
(("" (split -1)
(("1" (hide -2 -3)
(("1" (expand "continuous_rv?" -1)
(("1" (inst?) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (expand "*")
(("2" (expand "*")
(("2" (lemma "cont_rv_iff_comps")
(("2" (inst?)
(("2" (assert)
(("2" (flatten)
(("2"
(hide -2)
(("2"
(split -1)
(("1"
(flatten)
(("1"
(hide -2)
(("1"
(hide -3)
(("1"
(lemma prod_cont_fun)
(("1"
(inst
-
"(LAMBDA (t: T): hh!1(t))"
"(LAMBDA (t: T): f!1(t)`x)")
(("1"
(expand "*" -1)
(("1"
(hide 2)
(("1"
(expand
"continuous?"
1)
(("1"
(postpone)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil)
(prod_continuous_rv-1 nil 3473595230
("" (skeep)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (expand "*")
((""
(name "MAXH"
"max({h: real | EXISTS (xx: T): x0 - 1 <= xx AND xx <= x0+1 AND hh(xx) = h})")
(("1" (inst - "epsilon!1/MAXH")
(("1" (skosimp*)
(("1" (inst + "min(1,delta!1)")
(("1" (skosimp*)
(("1" (inst - x!1)
(("1" (assert)
(("1" (cross-mult -2)
(("1" (assert) (("1" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil) ("3" (postpone) nil nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(neg_continuous_rv 0
(neg_continuous_rv-1 nil 3302273405
(""
(grind :defs nil :rewrites
("continuity_def2" "neg_fun_convergent"))
nil 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)
(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)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(neg_fun_convergent formula-decl nil limit_real_vect2 nil)
(continuity_def2 formula-decl nil cont_real_vect2 nil))
nil))
(sum_cont_rv_fun 0
(sum_cont_rv_fun-1 nil 3393866517
("" (skosimp*)
(("" (assert)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (inst?)
(("" (inst?)
(("" (lemma "sum_continuous_rv")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(sum_continuous_rv formula-decl nil cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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)
(continuous_rv? const-decl "bool" cont_real_vect2 nil))
shostak))
(diff_cont_rv_fun 0
(diff_cont_rv_fun-1 nil 3393866553
("" (skosimp*)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (inst?)
(("" (inst?) (("" (rewrite "diff_continuous_rv") nil nil))
nil))
nil))
nil))
nil))
nil)
((continuous_rv? const-decl "bool" cont_real_vect2 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)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(diff_continuous_rv formula-decl nil cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
shostak))
(const_cont_rv_fun 0
(const_cont_rv_fun-1 nil 3393866606
("" (skosimp*)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (lemma "const_continuous_rv")
(("" (inst?)
(("" (expand "const_vfun") (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((continuous_rv? const-decl "bool" cont_real_vect2 nil)
(const_continuous_rv formula-decl nil cont_real_vect2 nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil))
shostak))
(const_vfun_cont_rv 0
(const_vfun_cont_rv-1 nil 3474118434
("" (skosimp*)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (lemma "const_continuous_rv")
(("" (inst?)
(("" (expand "const_vfun") (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((continuous_rv? const-decl "bool" cont_real_vect2 nil)
(const_continuous_rv formula-decl nil cont_real_vect2 nil)
(const_vfun const-decl "[T -> Vect2]" vect_fun_ops_rv 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)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 nil)
(T formal-subtype-decl nil cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
nil))
(scal_cont_rv_fun 0
(scal_cont_rv_fun-1 nil 3473598583
("" (skosimp*)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (lemma "scal_continuous_rv")
(("" (inst?) (("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((continuous_rv? const-decl "bool" cont_real_vect2 nil)
(scal_continuous_rv formula-decl nil cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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))
shostak))
(prod_cont_rv_fun 0
(prod_cont_rv_fun-2 nil 3474198595
("" (skosimp*)
(("" (lemma "cont_rv_iff_comps")
(("" (inst - "hh!1 * f!1")
(("" (assert)
(("" (hide 2)
(("" (lemma "cont_rv_iff_comps")
(("" (inst?)
(("" (assert)
(("" (hide -3)
(("" (flatten)
(("" (lemma prod_cont_fun)
((""
(inst - "(LAMBDA (t: T): hh!1(t))"
"(LAMBDA (t: T): f!1(t)`x)")
(("" (expand "*" -1)
(("" (assert)
((""
(split -1)
(("1"
(assert)
(("1"
(expand "*" 1)
(("1"
(expand "*")
(("1"
(hide -1 -2)
(("1"
(lemma prod_cont_fun)
(("1"
(inst
-
"(LAMBDA (t: T): hh!1(t))"
"(LAMBDA (t: T): f!1(t)`y)")
(("1"
(expand "*" -1)
(("1"
(case-replace
"(LAMBDA (t: T): hh!1(t)) = hh!1")
(("1" (assert) nil nil)
("2"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace
"(LAMBDA (t: T): hh!1(t)) = hh!1")
(("2"
(apply-extensionality 1 :hide? t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cont_rv_iff_comps formula-decl nil cont_real_vect2 nil)
(* const-decl "Vector" vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(prod_cont_fun formula-decl nil continuous_functions "analysis/")
(* const-decl "[T -> Vect2]" vect_fun_ops_rv nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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))
nil)
(prod_cont_rv_fun-1 nil 3473598431
("" (skosimp*)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (inst?)
(("" (lemma prod_continuous_rv)
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")) shostak))
(neg_cont_rv_fun 0
(neg_cont_rv_fun-1 nil 3393866960
("" (skosimp*)
(("" (assert)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (inst?) (("" (rewrite "neg_continuous_rv") nil nil))
nil))
nil))
nil))
nil))
nil)
((neg_continuous_rv formula-decl nil cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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)
(continuous_rv? const-decl "bool" cont_real_vect2 nil))
shostak))
(continuous_rv_fun_TCC1 0
(continuous_rv_fun_TCC1-1 nil 3302273405
("" (inst + "(LAMBDA (x: T): zero)")
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (inst + "1")
(("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(continuous_rv? const-decl "bool" cont_real_vect2 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)
(neg_zero formula-decl nil vectors_2D "vectors/")
(sub_zero_left formula-decl nil vectors_2D "vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/")
(real_ge_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)
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(continuous_rv? const-decl "bool" cont_real_vect2 nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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))
nil))
(sum_fun_continuous_rv 0
(sum_fun_continuous_rv-1 nil 3302273405
("" (skosimp*)
(("" (typepred "h1!1")
(("" (typepred "h2!1")
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (inst?)
(("" (inst?) (("" (rewrite "sum_continuous_rv") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous_rv_fun nonempty-type-eq-decl nil cont_real_vect2 nil)
(continuous_rv? const-decl "bool" cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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)
(sum_continuous_rv formula-decl nil cont_real_vect2 nil))
nil))
(diff_fun_continuous_rv 0
(diff_fun_continuous_rv-1 nil 3302273405
("" (skosimp*)
(("" (typepred "h1!1")
(("" (typepred "h2!1")
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (inst?)
(("" (inst?)
(("" (rewrite "diff_continuous_rv") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous_rv_fun nonempty-type-eq-decl nil cont_real_vect2 nil)
(continuous_rv? const-decl "bool" cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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)
(diff_continuous_rv formula-decl nil cont_real_vect2 nil))
nil))
(const_fun_continuous_rv 0
(const_fun_continuous_rv-1 nil 3302273405
("" (skosimp*)
(("" (lemma "const_vfun_cont_rv") (("" (inst?) nil nil)) nil)) nil)
((const_vfun_cont_rv formula-decl nil cont_real_vect2 nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
nil))
(neg_fun_continuous_rv 0
(neg_fun_continuous_rv-1 nil 3302273405
("" (skosimp*)
(("" (typepred "h!1")
(("" (expand "continuous_rv?")
(("" (skosimp*)
(("" (inst?) (("" (rewrite "neg_continuous_rv") nil nil))
nil))
nil))
nil))
nil))
nil)
((continuous_rv_fun nonempty-type-eq-decl nil cont_real_vect2 nil)
(continuous_rv? const-decl "bool" cont_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil cont_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" cont_real_vect2 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)
(neg_continuous_rv formula-decl nil cont_real_vect2 nil))
nil)))
¤ Dauer der Verarbeitung: 0.63 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.
|
