|
(limit_real_vect2
(cv_unique 0
(cv_unique-4 nil 3473161988
("" (grind :exclude ("abs" "norm" "-" "sigma") :if-match nil)
(("" (case "norm(l1!1 - l2!1) = 0")
(("1" (hide -2 -3 -4)
(("1" (lemma "norm_eq_0")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "add_move_right")
(("1" (inst?)
(("1" (inst -1 "zero") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (name "eps" "norm(l1!1 - l2!1)")
(("2" (replace -1)
(("2" (inst -3 "eps/2")
(("1" (inst -4 "eps/2")
(("1" (skosimp*)
(("1"
(case " EXISTS (x: T): a!1 /= x AND abs(x - a!1) < delta!1 AND abs(x - a!1) < delta!2")
(("1" (skosimp*)
(("1" (inst?)
(("1" (inst?)
(("1" (lemma "dist_triangle")
(("1" (inst - "l1!1" "f!1(x!1)" "l2!1")
(("1" (rewrite "dist_norm")
(("1"
(rewrite "dist_norm")
(("1"
(rewrite "dist_norm")
(("1"
(case-replace
"norm(l1!1 - l2!1) > 0")
(("1"
(assert)
(("1"
(lemma "norm_sym")
(("1"
(inst - "l1!1" "f!1(x!1)")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma "norm_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (name "DEL" "min(delta!1,delta!2)")
(("2" (inst - "a!1")
(("2" (inst - "a!1")
(("2" (assert)
(("2" (lemma "norm_triangle")
(("2" (inst?)
(("2"
(inst - "f!1(a!1)")
(("2"
(assert)
(("2"
(lemma "norm_sym")
(("2"
(inst - "l1!1" "f!1(a!1)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(add_zero_left formula-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(add_move_right formula-decl nil vectors_2D "vectors/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals 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)
(dist_triangle formula-decl nil distance_2D "vectors/")
(dist_norm formula-decl nil distance_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)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(norm_sym formula-decl nil vectors_2D "vectors/")
(abs_0 formula-decl nil abs_lems "reals/")
(norm_triangle formula-decl nil vectors_2D "vectors/")
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(eps skolem-const-decl "nnreal" limit_real_vect2 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)
(> const-decl "bool" reals nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" limit_real_vect2 nil))
nil)
(cv_unique-3 nil 3445160510
("" (grind :exclude ("abs" "norm" "-" "sigma") :if-match nil)
(("" (case "norm(l1!1 - l2!1) = 0")
(("1" (hide -2 -3 -4)
(("1" (lemma "norm_eq_0")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "add_move_right")
(("1" (inst?)
(("1" (inst -1 "zero") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (name "eps" "norm(l1!1 - l2!1)")
(("2" (replace -1)
(("2" (inst -3 "eps/2")
(("1" (inst -4 "eps/2")
(("1" (skosimp*)
(("1"
(case " EXISTS (x: real): a!1 /= x AND abs(x - a!1) < delta!1 AND abs(x - a!1) < delta!2")
(("1" (skosimp*)
(("1" (inst?)
(("1" (inst?)
(("1" (lemma "dist_triangle")
(("1" (inst - "l1!1" "f!1(x!1)" "l2!1")
(("1" (rewrite "dist_norm")
(("1"
(rewrite "dist_norm")
(("1"
(rewrite "dist_norm")
(("1"
(case-replace
"norm(l1!1 - l2!1) > 0")
(("1"
(assert)
(("1"
(lemma "norm_sym")
(("1"
(inst - "l1!1" "f!1(x!1)")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma "norm_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (name "DEL" "min(delta!1,delta!2)")
(("2" (inst + "a!1+DEL/2")
(("2" (assert)
(("2" (hide -2 -3 -4 -5 3)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(add_zero_left formula-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(add_move_right formula-decl nil vectors_2D "vectors/")
(dist_triangle formula-decl nil distance_2D "vectors/")
(dist_norm formula-decl nil distance_2D "vectors/")
(norm_sym formula-decl nil vectors_2D "vectors/"))
nil)
(cv_unique-2 nil 3442578793
("" (grind :exclude ("abs" "norm" "-" "sigma") :if-match nil)
(("" (case "norm(l1!1 - l2!1) = 0")
(("1" (hide -2 -3 -4)
(("1" (lemma "norm_eq_0")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "add_move_right")
(("1" (inst?)
(("1" (inst -1 "zero") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (name "eps" "norm(l1!1 - l2!1)")
(("2" (replace -1)
(("2" (inst -3 "eps/2")
(("1" (inst -4 "eps/2")
(("1" (skosimp*)
(("1"
(case " EXISTS (x: real): a!1 /= x AND abs(x - a!1) < delta!1 AND abs(x - a!1) < delta!2")
(("1" (skosimp*)
(("1" (inst?)
(("1" (inst?)
(("1" (lemma "dist_triangle_lt")
(("1" (inst - "l1!1" "f!1(x!1)" "l2!1")
(("1" (rewrite "dist_norm")
(("1"
(rewrite "dist_norm")
(("1"
(rewrite "dist_norm")
(("1"
(case-replace
"norm(l1!1 - l2!1) > 0")
(("1"
(assert)
(("1"
(lemma "norm_sym")
(("1"
(inst - "l1!1" "f!1(x!1)")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma "norm_eq_0")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (name "DEL" "min(delta!1,delta!2)")
(("2" (inst + "a!1+DEL/2")
(("2" (assert)
(("2" (hide -2 -3 -4 -5 3)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((norm_sym formula-decl nil vectors_2D "vectors/")
(dist_norm formula-decl nil distance_2D "vectors/")
(add_move_right formula-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(add_zero_left formula-decl nil vectors_2D "vectors/")
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
nil)
(cv_unique-1 nil 3299406886
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (rewrite "abs_diff_0")
(("" (name "eps" "abs(l1!1 - l2!1)")
(("" (replace -1)
(("" (inst -4 "eps/2")
(("1" (inst -5 "eps/2")
(("1" (assert)
(("1" (skosimp*)
(("1"
(case " EXISTS (x: Vector): a!1 /= x AND norm(x - a!1) < delta!1 AND norm(x - a!1) < delta!2")
(("1" (skosimp*)
(("1" (inst?)
(("1" (inst?)
(("1" (assert)
(("1" (case "0 < norm(x!1 - a!1)")
(("1"
(assert)
(("1"
(lemma "triangle2")
(("1"
(inst
-
"eps/2"
"eps/2"
"l1!1"
"f!1(x!1)"
"l2!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma "norm_eq_0")
(("2"
(inst?)
(("2"
(assert)
(("2"
(replace -1 * lr)
(("2"
(assert)
(("2"
(rewrite "sub_eq_zero")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -4 -5)
(("2" (name "DEL" "min(delta!1,delta!2)")
(("2"
(name AA "a!1 WITH [0 := a!1(0) + DEL/2]")
(("1" (inst + "AA")
(("1" (case "norm(AA - a!1) = abs(DEL/2)")
(("1"
(replace -1 * lr)
(("1"
(hide -1)
(("1"
(case "a!1 /= AA")
(("1"
(assert)
(("1"
(hide -1 -2)
(("1" (grind) nil nil))
nil))
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(hide 1 -3 -4)
(("2"
(replace -1 * lr)
(("2"
(hide -1)
(("2"
(case
"AA WITH [(0) := AA(0) + DEL / 2](0) = AA(0)")
(("1"
(hide -2)
(("1"
(assert)
nil
nil))
nil)
("2"
(replace -1 * lr)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1)
(("2"
(reveal -1)
(("2"
(hide 2)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(expand "norm")
(("2"
(case-replace
"a!1 WITH [(0) := a!1(0) + DEL / 2] - a!1 =
(LAMBDA (i: Index): IF i = 0 THEN DEL/2 ELSE 0 ENDIF)")
(("1"
(hide -1)
(("1"
(expand "sqv")
(("1"
(expand "*")
(("1"
(lemma
"sigma_first")
(("1"
(inst?)
(("1"
(postpone)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((abs_diff_0 formula-decl nil abs_lems "reals/")
(* const-decl "real" vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sqrt_square formula-decl nil sqrt "reals/")
(triangle2 formula-decl nil abs_lems "reals/")
(sub_eq_zero formula-decl nil vectors_2D "vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/")
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/"))
nil))
(cv_in_domain 0
(cv_in_domain-1 nil 3299406886
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (case "norm(l!1 - f!1(x!1)) = 0")
(("1" (lemma "norm_eq_0")
(("1" (inst?)
(("1" (assert) (("1" (rewrite "sub_eq_zero") nil nil)) nil))
nil))
nil)
("2" (inst - "norm(l!1 - f!1(x!1))")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert)
(("1" (rewrite "norm_sym") (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(sub_eq_zero formula-decl nil vectors_2D "vectors/")
(norm_eq_0 formula-decl nil vectors_2D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs_0 formula-decl nil abs_lems "reals/")
(norm_sym formula-decl nil vectors_2D "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(x!1 skolem-const-decl "T" limit_real_vect2 nil)
(f!1 skolem-const-decl "[T -> Vect2]" limit_real_vect2 nil)
(l!1 skolem-const-decl "Vect2" limit_real_vect2 nil)
(> const-decl "bool" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" limit_real_vect2 nil))
nil))
(cv_sum 0
(cv_sum-1 nil 3299406886
("" (skeep)
(("" (grind :exclude ("abs" "norm" "+" "-") :if-match nil)
(("" (inst - "epsilon!1/4")
(("" (inst - "epsilon!1/4")
(("" (skosimp*)
(("" (inst 1 "min(delta!1, delta!2)")
(("" (skosimp*)
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (lemma "norm_add_le")
(("" (inst - "f1(x!1) - l1" "f2(x!1)-l2")
((""
(case-replace
"norm(f1(x!1) - l1 + (f2(x!1) - l2)) = norm((f1 + f2)(x!1) - (l1 + l2))")
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (grind :exclude "norm") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((convergence const-decl "bool" limit_real_vect2 nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(T formal-subtype-decl nil limit_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" limit_real_vect2 nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(norm_add_le formula-decl nil vectors_2D "vectors/")
(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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil))
(cv_neg 0
(cv_neg-2 nil 3445161748
("" (skeep)
(("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (inst - "epsilon!1")
(("" (skolem!)
(("" (inst + "delta!1")
(("" (skosimp)
(("" (inst?)
(("" (assert)
((""
(case-replace
"norm((-f)(x!1) - -l) = norm(f(x!1) -l)")
(("" (assert)
(("" (hide-all-but 1)
(("" (lemma "norm_neg")
(("" (inst - "f(x!1) - l")
(("" (grind :exclude "norm") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((convergence const-decl "bool" limit_real_vect2 nil)
(real_minus_real_is_real application-judgement "real" reals 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)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(norm_neg formula-decl nil vectors_2D "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T_pred const-decl "[real -> boolean]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil))
nil)
(cv_neg-1 nil 3299406886
("" (skeep)
(("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (inst - "epsilon!1")
(("" (skolem!)
(("" (inst + "delta!1")
(("" (skosimp)
(("" (inst?)
(("" (assert)
((""
(case-replace
"norm((-f)(x!1) - -l) = norm(f(x!1) -l)")
(("" (assert)
(("" (hide-all-but 1)
(("" (lemma "norm_neg")
(("" (inst - "f(x!1) - l")
(("" (grind :exclude "norm") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((norm_neg formula-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/"))
nil))
(cv_diff 0
(cv_diff-1 nil 3299406886
("" (skosimp*)
(("" (case-replace "f1!1 - f2!1 = f1!1 + (-f2!1)")
(("1" (lemma "cv_sum")
(("1" (inst?)
(("1" (inst - "(-f2!1)" "-l2!1")
(("1" (assert)
(("1" (hide 2)
(("1" (lemma "cv_neg")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (grind) (("2" (apply-extensionality 1 :hide? t) nil nil))
nil))
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)
(T_pred const-decl "[real -> boolean]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(add_neg_sub formula-decl nil vectors_2D "vectors/")
(cv_neg formula-decl nil limit_real_vect2 nil)
(cv_sum formula-decl nil limit_real_vect2 nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(cv_const 0
(cv_const-2 nil 3473594761
(";;; Proof cv_const-1 for formula limit_real_vect2.cv_const"
(expand "convergence")
((";;; Proof cv_const-1 for formula limit_real_vect2.cv_const"
(skosimp*)
((";;; Proof cv_const-1 for formula limit_real_vect2.cv_const"
(expand "const_vfun")
((";;; Proof cv_const-1 for formula limit_real_vect2.cv_const"
(assert) nil))))))
";;; developed with shostak decision procedures")
((sub_eq_args formula-decl nil vectors_2D "vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/")
(const_vfun const-decl "[T -> Vect2]" vect_fun_ops_rv nil)
(convergence const-decl "bool" limit_real_vect2 nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(cv_const-1 nil 3299406886
("" (expand "convergence")
(("" (skosimp*)
(("" (expand "const_fun") (("" (assert) nil nil)) nil)) nil))
nil)
((sub_eq_args formula-decl nil vectors_2D "vectors/")
(norm_zero formula-decl nil vectors_2D "vectors/"))
nil))
(cv_scal 0
(cv_scal-2 nil 3445182373
("" (skeep)
(("" (case-replace "b = 0")
(("1" (assert)
(("1" (lemma "cv_const")
(("1" (inst - "a" "zero")
(("1" (expand "const_vfun") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "convergence")
(("2" (skosimp*)
(("2" (inst - "epsilon!1/abs(b)")
(("1" (skosimp*)
(("1" (inst + "delta!1")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert)
(("1" (cross-mult -1)
(("1" (lemma "norm_scal")
(("1" (inst - "b" "f(x!1)-l")
(("1" (rewrite "scal_sub_right")
(("1"
(expand "*" 2 1)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (case "epsilon!1 / abs(b) > 0")
(("1" (assert) nil nil)
("2" (cross-mult 1) (("2" (assert) nil nil)) nil)
("3" (lemma "abs_eq_0")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(cv_const formula-decl nil limit_real_vect2 nil)
(const_vfun const-decl "[T -> Vect2]" vect_fun_ops_rv nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(scal_0 formula-decl nil vectors_2D "vectors/")
(abs_eq_0 formula-decl nil abs_lems "reals/")
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(abs_nat formula-decl nil abs_lems "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(norm_scal formula-decl nil vectors_2D "vectors/")
(scal_sub_right formula-decl nil vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(- const-decl "Vector" vectors_2D "vectors/")
(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)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(epsilon!1 skolem-const-decl "posreal" limit_real_vect2 nil)
(/= const-decl "boolean" notequal nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(b skolem-const-decl "T" limit_real_vect2 nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(convergence const-decl "bool" limit_real_vect2 nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(cv_scal-1 nil 3445182023
("" (skeep)
(("" (expand "convergence")
(("" (skosimp*)
(("" (inst - "epsilon!1/b")
(("1" (skosimp*)
(("1" (inst + "delta!1")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert)
(("1" (lemma "norm_scal")
(("1" (inst - "b" "f(x!1)")
(("1" (cross-mult -2)
(("1" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil) ("3" (postpone) nil nil))
nil))
nil))
nil))
nil)
nil nil))
(lim_TCC1 0
(lim_TCC1-1 nil 3445162155
("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (typepred "x0!1")
(("" (expand "convergent?")
(("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets 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]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(convergent? const-decl "bool" limit_real_vect2 nil)
(empty? const-decl "bool" sets nil))
nil))
(lim_fun_lemma 0
(lim_fun_lemma-1 nil 3299406886
("" (skolem!)
(("" (name-replace "ll" "lim(f!1, x0!1)" :hide? nil)
(("" (expand "lim" -)
(("" (typepred "choose(LAMBDA l: convergence(f!1, x0!1, l))")
(("1" (assert) nil nil)
("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(T_pred const-decl "[real -> boolean]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" limit_real_vect2 nil)
(lim const-decl "Vect2" limit_real_vect2 nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(convergence const-decl "bool" limit_real_vect2 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil))
nil))
(lim_fun_def 0
(lim_fun_def-1 nil 3299406886
("" (skolem!)
(("" (use "lim_fun_lemma")
(("" (ground)
(("" (use "cv_unique" ("l2" "lim(f!1, x0!1)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((lim_fun_lemma formula-decl nil limit_real_vect2 nil)
(convergent? const-decl "bool" limit_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 limit_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" limit_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)
(cv_unique formula-decl nil limit_real_vect2 nil)
(lim const-decl "Vect2" limit_real_vect2 nil))
nil))
(convergence_equiv 0
(convergence_equiv-1 nil 3299406886
("" (skolem!)
(("" (prop)
(("1" (expand "convergent?") (("1" (inst?) nil nil)) nil)
("2" (rewrite "lim_fun_def")
(("2" (expand "convergent?") (("2" (inst?) nil nil)) nil)) nil)
("3" (rewrite "lim_fun_def") nil nil))
nil))
nil)
((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" limit_real_vect2 nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" limit_real_vect2 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)
(lim_fun_def formula-decl nil limit_real_vect2 nil))
nil))
(convergent_in_domain 0
(convergent_in_domain-1 nil 3299406886
("" (grind :exclude "convergence")
(("" (forward-chain "cv_in_domain") (("" (assert) nil nil)) nil))
nil)
((cv_in_domain formula-decl nil limit_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(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]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(convergent? const-decl "bool" limit_real_vect2 nil))
nil))
(lim_in_domain 0
(lim_in_domain-1 nil 3299406886
("" (skosimp)
(("" (rewrite "lim_fun_def")
(("" (rewrite "convergent_in_domain") nil nil)) nil))
nil)
((lim_fun_def formula-decl nil limit_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]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" limit_real_vect2 nil)
(convergent_in_domain formula-decl nil limit_real_vect2 nil))
nil))
(sum_fun_convergent 0
(sum_fun_convergent-1 nil 3299406886
("" (expand "convergent?")
(("" (skosimp*)
(("" (inst 1 "l!1 + l!2") (("" (rewrite "cv_sum") nil nil)) nil))
nil))
nil)
((cv_sum formula-decl nil limit_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)
(T_pred const-decl "[real -> boolean]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(+ const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" limit_real_vect2 nil))
nil))
(neg_fun_convergent 0
(neg_fun_convergent-1 nil 3299406886
("" (expand "convergent?")
(("" (skosimp*)
(("" (forward-chain "cv_neg") (("" (inst?) nil nil)) nil)) nil))
nil)
((Vector type-eq-decl nil vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T formal-subtype-decl nil limit_real_vect2 nil)
(T_pred const-decl "[real -> boolean]" limit_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)
(cv_neg formula-decl nil limit_real_vect2 nil)
(convergent? const-decl "bool" limit_real_vect2 nil))
nil))
(diff_fun_convergent 0
(diff_fun_convergent-1 nil 3299406886
("" (expand "convergent?")
(("" (skosimp*)
(("" (inst 1 "l!1 - l!2") (("" (rewrite "cv_diff") nil nil))
nil))
nil))
nil)
((cv_diff formula-decl nil limit_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)
(T_pred const-decl "[real -> boolean]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(- const-decl "Vector" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" limit_real_vect2 nil))
nil))
(const_fun_convergent 0
(const_fun_convergent-1 nil 3299406886
("" (expand "convergent?")
(("" (skolem!)
(("" (inst?) (("" (rewrite "cv_const") nil nil)) nil)) nil))
nil)
((cv_const formula-decl nil limit_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)
(T_pred const-decl "[real -> boolean]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(convergent? const-decl "bool" limit_real_vect2 nil))
nil))
(lim_sum_fun_TCC1 0
(lim_sum_fun_TCC1-1 nil 3299406886
("" (skosimp) (("" (rewrite "sum_fun_convergent") nil nil)) nil)
((sum_fun_convergent formula-decl nil limit_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]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
nil))
(lim_sum_fun 0
(lim_sum_fun-1 nil 3299406886
(""
(auto-rewrite "lim_fun_lemma" "lim_fun_def" "sum_fun_convergent"
("cv_sum"))
(("" (skosimp) (("" (assert) nil nil)) nil)) nil)
((lim_fun_lemma formula-decl nil limit_real_vect2 nil)
(cv_sum formula-decl nil limit_real_vect2 nil)
(lim_fun_def formula-decl nil limit_real_vect2 nil))
nil))
(lim_neg_fun_TCC1 0
(lim_neg_fun_TCC1-1 nil 3299406886
("" (lemma "neg_fun_convergent") (("" (propax) nil nil)) nil)
((neg_fun_convergent formula-decl nil limit_real_vect2 nil)) nil))
(lim_neg_fun 0
(lim_neg_fun-1 nil 3299406886
(""
(auto-rewrite "lim_fun_lemma" "lim_fun_def" "neg_fun_convergent"
("cv_neg"))
(("" (skosimp) (("" (assert) nil nil)) nil)) nil)
((lim_fun_lemma formula-decl nil limit_real_vect2 nil)
(cv_neg formula-decl nil limit_real_vect2 nil)
(lim_fun_def formula-decl nil limit_real_vect2 nil))
nil))
(lim_diff_fun_TCC1 0
(lim_diff_fun_TCC1-1 nil 3299406886
("" (skosimp) (("" (rewrite "diff_fun_convergent") nil nil)) nil)
((diff_fun_convergent formula-decl nil limit_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]" limit_real_vect2 nil)
(T formal-subtype-decl nil limit_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
nil))
(lim_diff_fun 0
(lim_diff_fun-1 nil 3299406886
(""
(auto-rewrite "lim_fun_lemma" "lim_fun_def" "diff_fun_convergent"
("cv_diff"))
(("" (skosimp) (("" (assert) nil nil)) nil)) nil)
((lim_fun_lemma formula-decl nil limit_real_vect2 nil)
(cv_diff formula-decl nil limit_real_vect2 nil)
(lim_fun_def formula-decl nil limit_real_vect2 nil))
nil)))
¤ Dauer der Verarbeitung: 0.97 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.
|
