|
(limit_vect3_real
(cv_unique 0
(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: Vect3): 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"
(assert)
(("2"
(lemma "vectors_3D.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))
nil)
("2" (hide -4 -5)
(("2" (name "DEL" "min(delta!1,delta!2)")
(("2" (inst + "(a!1`x + DEL/2, a!1`y, a!1`z)")
(("2" (grind) 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/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_3D "vectors/")
(sqv const-decl "nnreal" vectors_3D "vectors/")
(sqrt_square formula-decl nil sqrt "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(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)
(triangle2 formula-decl nil abs_lems "reals/")
(norm_eq_0 formula-decl nil vectors_3D "vectors/")
(norm_zero formula-decl nil vectors_3D "vectors/")
(sub_eq_zero formula-decl nil vectors_3D "vectors/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(- const-decl "Vector" vectors_3D "vectors/")
(norm const-decl "nnreal" vectors_3D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(Vector type-eq-decl nil vectors_3D "vectors/")
(< const-decl "bool" reals nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(posreal nonempty-type-eq-decl nil real_types nil)
(eps skolem-const-decl
"{n: nonneg_real | n >= l1!1 - l2!1 AND n >= -(l1!1 - l2!1)}"
limit_vect3_real nil)
(l2!1 skolem-const-decl "real" limit_vect3_real nil)
(l1!1 skolem-const-decl "real" limit_vect3_real nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal 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)
(= const-decl "[T, T -> boolean]" equalities 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" limit_vect3_real nil))
nil))
(cv_in_domain 0
(cv_in_domain-1 nil 3299406886
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (rewrite "abs_diff_0")
(("" (inst - "abs(l!1 - f!1(x!1))")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert)
(("1" (rewrite "abs_diff_commute" -)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(abs_diff_0 formula-decl nil abs_lems "reals/")
(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)
(sub_eq_args formula-decl nil vectors_3D "vectors/")
(norm_zero formula-decl nil vectors_3D "vectors/")
(abs_diff_commute formula-decl nil abs_lems "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(- 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND 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)
(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)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" limit_vect3_real nil))
nil))
(cv_sum 0
(cv_sum-1 nil 3299406886
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (inst - "epsilon!1/2")
(("" (inst - "epsilon!1/2")
(("" (skosimp*)
(("" (inst 1 "min(delta!1, delta!2)")
(("" (skosimp*)
(("" (inst?)
(("" (inst?)
(("" (assert)
((""
(lemma "triangle"
("x" "f1!1(x!1) - l1!1" "y" "f2!1(x!1) - l2!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
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)
(triangle formula-decl nil real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(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)
(real_gt_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)
(>= 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)
(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)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(convergence const-decl "bool" limit_vect3_real nil))
nil))
(cv_neg 0
(cv_neg-1 nil 3299406886
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (inst - "epsilon!1")
(("" (skolem!)
(("" (inst + "delta!1")
(("" (skosimp)
(("" (inst?)
(("" (assert)
(("" (expand "-")
(("" (lemma "abs_neg")
(("" (inst - "f!1(x!1) - l!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(- const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(- const-decl "Vector" vectors_3D "vectors/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(abs_neg formula-decl nil abs_lems "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_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)
(>= 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)
(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)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" limit_vect3_real nil))
nil))
(cv_diff 0
(cv_diff-1 nil 3299406886
("" (skosimp*)
(("" (rewrite "diff_function")
(("" (lemma "cv_sum")
(("" (inst?)
(("" (inst - "(-f2!1)" "-l2!1")
(("" (assert)
(("" (hide 2)
(("" (lemma "cv_neg")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((diff_function formula-decl nil vect3_fun_ops "vectors/")
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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)
(real_minus_real_is_real application-judgement "real" reals nil)
(cv_neg formula-decl nil limit_vect3_real nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(minus_real_is_real application-judgement "real" reals nil)
(cv_sum formula-decl nil limit_vect3_real nil))
nil))
(cv_prod 0
(cv_prod-2 nil 3442332189
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
((""
(lemma "prod_epsilon" ("y1" "l1!1" "y2" "l2!1" "e" "epsilon!1"))
(("" (skosimp*)
(("" (inst - "e1!1")
(("" (inst - "e2!1")
(("" (skosimp*)
(("" (inst 1 "min(delta!1, delta!2)")
(("" (skosimp*)
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (lemma "prod_bound")
((""
(inst -1 "e1!1" "e2!1" "f1!1(x!1)"
"f2!1(x!1)" "l1!1" "l2!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((prod_epsilon formula-decl nil epsilon_lemmas "analysis/")
(prod_bound formula-decl nil epsilon_lemmas "analysis/")
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(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)
(real_gt_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)
(>= 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)
(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)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(convergence const-decl "bool" limit_vect3_real nil))
nil)
(cv_prod-1 nil 3299406886
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
((""
(lemma "prod_epsilon"
("y1" "l1!1" "y2" "l2!1" "epsilon" "epsilon!1"))
(("" (skosimp*)
(("" (inst - "e1!1")
(("" (inst - "e2!1")
(("" (skosimp*)
(("" (inst 1 "min(delta!1, delta!2)")
(("" (skosimp*)
(("" (inst?)
(("" (inst?)
(("" (assert) (("" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(cv_const 0
(cv_const-1 nil 3299406886
("" (expand "convergence")
(("" (skosimp*)
(("" (expand "const_fun") (("" (assert) nil nil)) nil)) nil))
nil)
((abs_0 formula-decl nil abs_lems "reals/")
(const_fun const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(convergence const-decl "bool" limit_vect3_real nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(cv_scal 0
(cv_scal-1 nil 3299406886
("" (skosimp)
(("" (rewrite "scal_function")
(("" (rewrite "cv_prod")
(("" (hide 2) (("" (rewrite "cv_const") nil nil)) nil)) nil))
nil))
nil)
((scal_function formula-decl nil vect3_fun_ops "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)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(cv_const formula-decl nil limit_vect3_real nil)
(real_times_real_is_real application-judgement "real" reals nil)
(const_fun const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(cv_prod formula-decl nil limit_vect3_real nil))
nil))
(cv_inv 0
(cv_inv-2 nil 3442332397
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (lemma "inv_epsilon" ("y1" "l!1" "e" "epsilon!1"))
(("" (assert)
(("" (skosimp)
(("" (inst? -)
(("" (skosimp*)
(("" (inst + "delta!1")
(("" (skosimp*)
(("" (inst?)
(("" (assert)
((""
(lemma "inv_bound"
("e1" "e1!1" "x1" "g!1(x!1)" "y1" "l!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inv_epsilon formula-decl nil epsilon_lemmas "analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(inv_bound formula-decl nil epsilon_lemmas "analysis/")
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_gt_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)
(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)
(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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(/ const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(/= const-decl "boolean" notequal nil)
(convergence const-decl "bool" limit_vect3_real nil))
nil)
(cv_inv-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_inv[T]") nil nil))
nil)
nil nil))
(cv_div 0
(cv_div-1 nil 3299406886
("" (skosimp*)
(("" (rewrite "div_function")
(("" (assert)
(("" (use "cv_prod" ("l2" "1/l2!1"))
(("" (assert) (("" (rewrite "cv_inv") nil nil)) nil)) nil))
nil))
nil))
nil)
((div_function formula-decl nil vect3_fun_ops "vectors/")
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cv_prod formula-decl nil limit_vect3_real nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(/ const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(cv_inv formula-decl nil limit_vect3_real nil)
(real_div_nzreal_is_real application-judgement "real" reals 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" -)
((""
(lemma "epsilon_ax"
("p" "LAMBDA (l: real): convergence(f!1, x0!1, l)"))
(("" (assert)
(("" (typepred "x0!1")
(("" (expand "convergent?") (("" (propax) nil nil)) 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)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" limit_vect3_real nil)
(lim const-decl "real" limit_vect3_real nil)
(convergence const-decl "bool" limit_vect3_real nil)
(pred type-eq-decl nil defined_types nil)
(epsilon_ax formula-decl nil epsilons nil)
(NOT const-decl "[bool -> bool]" booleans 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_vect3_real nil)
(convergent? const-decl "bool" limit_vect3_real nil)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(cv_unique formula-decl nil limit_vect3_real nil)
(lim const-decl "real" limit_vect3_real 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)
((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)
(convergent? const-decl "bool" limit_vect3_real nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(lim_fun_def formula-decl nil limit_vect3_real 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_vect3_real nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(convergent? const-decl "bool" limit_vect3_real 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_vect3_real nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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)
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" limit_vect3_real nil)
(convergent_in_domain formula-decl nil limit_vect3_real 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)
((Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(cv_sum formula-decl nil limit_vect3_real nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(convergent? const-decl "bool" limit_vect3_real 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)
((numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(minus_real_is_real application-judgement "real" 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)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(cv_neg formula-decl nil limit_vect3_real nil)
(convergent? const-decl "bool" limit_vect3_real 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)
((Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(cv_diff formula-decl nil limit_vect3_real nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergent? const-decl "bool" limit_vect3_real nil))
nil))
(prod_fun_convergent 0
(prod_fun_convergent-1 nil 3299406886
("" (expand "convergent?")
(("" (skosimp*)
(("" (inst 1 "l!1 * l!2") (("" (rewrite "cv_prod") nil nil))
nil))
nil))
nil)
((Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(cv_prod formula-decl nil limit_vect3_real nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(convergent? const-decl "bool" limit_vect3_real 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_vect3_real nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(convergent? const-decl "bool" limit_vect3_real nil))
nil))
(scal_fun_convergent 0
(scal_fun_convergent-1 nil 3299406886
("" (expand "convergent?")
(("" (skosimp*)
(("" (inst 1 "b!1 * l!1") (("" (rewrite "cv_scal") nil nil))
nil))
nil))
nil)
((Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(cv_scal formula-decl nil limit_vect3_real nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(convergent? const-decl "bool" limit_vect3_real nil))
nil))
(inv_fun_convergent 0
(inv_fun_convergent-1 nil 3299406886
("" (skosimp)
(("" (rewrite "lim_fun_def")
(("" (expand "convergent?")
(("" (skosimp)
(("" (assert)
(("" (inst 2 "1/l!1") (("" (rewrite "cv_inv") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lim_fun_def formula-decl nil limit_vect3_real nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" limit_vect3_real nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cv_inv formula-decl nil limit_vect3_real nil))
nil))
(div_fun_convergent 0
(div_fun_convergent-1 nil 3299406886
("" (skosimp)
(("" (rewrite "lim_fun_def")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (assert)
(("" (inst 2 "l!1 / l!2") (("" (rewrite "cv_div") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lim_fun_def formula-decl nil limit_vect3_real nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" limit_vect3_real nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cv_div formula-decl nil limit_vect3_real 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_vect3_real nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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))
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_vect3_real nil)
(cv_sum formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil)
(real_plus_real_is_real application-judgement "real" reals 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_vect3_real 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_vect3_real nil)
(cv_neg formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil)
(minus_real_is_real application-judgement "real" reals 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_vect3_real nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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))
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_vect3_real nil)
(cv_diff formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(lim_prod_fun_TCC1 0
(lim_prod_fun_TCC1-1 nil 3299406886
("" (skosimp) (("" (rewrite "prod_fun_convergent") nil nil)) nil)
((prod_fun_convergent formula-decl nil limit_vect3_real nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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))
nil))
(lim_prod_fun 0
(lim_prod_fun-1 nil 3299406886
(""
(auto-rewrite "lim_fun_lemma" "lim_fun_def" "prod_fun_convergent"
("cv_prod"))
(("" (skosimp) (("" (assert) nil nil)) nil)) nil)
((lim_fun_lemma formula-decl nil limit_vect3_real nil)
(cv_prod formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(lim_const_fun_TCC1 0
(lim_const_fun_TCC1-1 nil 3299406886
("" (lemma "const_fun_convergent") (("" (propax) nil nil)) nil)
((const_fun_convergent formula-decl nil limit_vect3_real nil)) nil))
(lim_const_fun 0
(lim_const_fun-1 nil 3299406886
(""
(auto-rewrite "lim_fun_lemma" "lim_fun_def" "const_fun_convergent"
("cv_const"))
(("" (skosimp) (("" (assert) nil nil)) nil)) nil)
((cv_const formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil))
nil))
(lim_scal_fun_TCC1 0
(lim_scal_fun_TCC1-1 nil 3299406886
("" (lemma "scal_fun_convergent") (("" (propax) nil nil)) nil)
((scal_fun_convergent formula-decl nil limit_vect3_real nil)) nil))
(lim_scal_fun 0
(lim_scal_fun-1 nil 3299406886
(""
(auto-rewrite "lim_fun_lemma" "lim_fun_def" "scal_fun_convergent"
"cv_scal")
(("" (skosimp) (("" (assert) nil nil)) nil)) nil)
((lim_fun_lemma formula-decl nil limit_vect3_real nil)
(cv_scal formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(lim_inv_fun_TCC1 0
(lim_inv_fun_TCC1-1 nil 3299406886
("" (skosimp) (("" (rewrite "inv_fun_convergent") nil nil)) nil)
((inv_fun_convergent formula-decl nil limit_vect3_real nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil))
nil))
(lim_inv_fun 0
(lim_inv_fun-1 nil 3299406886
("" (skosimp)
(("" (assert)
(("" (delete 1)
((""
(auto-rewrite "lim_fun_def" "lim_fun_lemma"
"inv_fun_convergent" ("cv_inv"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(lim_fun_lemma formula-decl nil limit_vect3_real nil)
(cv_inv formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil))
nil))
(lim_div_fun_TCC1 0
(lim_div_fun_TCC1-1 nil 3299406886
("" (skosimp) (("" (rewrite "div_fun_convergent") nil nil)) nil)
((div_fun_convergent formula-decl nil limit_vect3_real nil)
(real nonempty-type-from-decl nil reals nil)
(Vect3 type-eq-decl nil vectors_3D_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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil))
nil))
(lim_div_fun 0
(lim_div_fun-1 nil 3299406886
("" (skosimp)
(("" (assert)
(("" (delete 1)
((""
(auto-rewrite "lim_fun_def" "lim_fun_lemma"
"div_fun_convergent" "cv_div")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(lim_fun_lemma formula-decl nil limit_vect3_real nil)
(cv_div formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil))
nil))
(convergence_order 0
(convergence_order-1 nil 3442333462
("" (grind :exclude ("abs" "norm" "-") :if-match nil)
(("" (case "l2!1 < l1!1")
(("1" (case "l2!1 < l1!1")
(("1" (name "eps" "(l1!1 - l2!1)/2")
(("1" (assert)
(("1" (inst - "eps")
(("1" (inst - "eps")
(("1" (skosimp*)
(("1" (inst?)
(("1" (inst?)
(("1" (inst?)
(("1" (assert) (("1" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((< const-decl "bool" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_gt_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)
(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)
(sub_eq_args formula-decl nil vectors_3D "vectors/")
(norm_zero formula-decl nil vectors_3D "vectors/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(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)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" limit_vect3_real nil))
shostak))
(convergence_lower_bound 0
(convergence_lower_bound-1 nil 3442333554
("" (skosimp*)
(("" (lemma "cv_const")
(("" (inst - "b!1" "a!1")
(("" (use "convergence_order" ("f2" "f!1"))
(("" (assert)
(("" (skosimp*)
(("" (expand "const_fun")
(("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cv_const formula-decl nil limit_vect3_real nil)
(convergence_order formula-decl nil limit_vect3_real nil)
(const_fun const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(convergence_upper_bound 0
(convergence_upper_bound-1 nil 3442333686
("" (skosimp*)
(("" (lemma "cv_const")
(("" (inst - "b!1" "a!1")
(("" (assert)
(("" (use "convergence_order" ("f1" "f!1"))
(("" (expand "const_fun") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((cv_const formula-decl nil limit_vect3_real nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(const_fun const-decl "[Vect3 -> real]" vect3_fun_ops "vectors/")
(convergence_order formula-decl nil limit_vect3_real nil)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(lim_le1 0
(lim_le1-1 nil 3299406886
("" (skosimp)
(("" (assert)
(("" (name-replace "ll" "lim(f!1, a!1)" :hide? nil)
(("" (rewrite "lim_fun_def")
(("" (use "convergence_upper_bound") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(lim_fun_def formula-decl nil limit_vect3_real nil)
(convergence_upper_bound formula-decl nil limit_vect3_real nil)
(lim const-decl "real" limit_vect3_real nil)
(convergent? const-decl "bool" limit_vect3_real nil)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(lim_ge1 0
(lim_ge1-1 nil 3299406886
("" (skosimp)
(("" (assert)
(("" (name-replace "ll" "lim(f!1, a!1)" :hide? nil)
(("" (rewrite "lim_fun_def")
(("" (use "convergence_lower_bound" ("b" "b!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(lim_fun_def formula-decl nil limit_vect3_real nil)
(convergence_lower_bound formula-decl nil limit_vect3_real nil)
(lim const-decl "real" limit_vect3_real nil)
(convergent? const-decl "bool" limit_vect3_real nil)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(lim_order1 0
(lim_order1-1 nil 3299406886
("" (skosimp)
(("" (assert)
(("" (name-replace "ll1" "lim(f1!1, a!1)" :hide? nil)
(("" (name-replace "ll2" "lim(f2!1, a!1)" :hide? nil)
(("" (rewrite "lim_fun_def")
(("" (rewrite "lim_fun_def")
(("" (use "convergence_order" ("l1" "ll1" "l2" "ll2"))
(("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(convergence_order formula-decl nil limit_vect3_real nil)
(lim_fun_def formula-decl nil limit_vect3_real nil)
(lim const-decl "real" limit_vect3_real nil)
(convergent? const-decl "bool" limit_vect3_real nil)
(bool nonempty-type-eq-decl nil booleans 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)
(Vect3 type-eq-decl nil vectors_3D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil)))
¤ Dauer der Verarbeitung: 0.826 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.
|
