|
(lim_of_functions
(convergence_def 0
(convergence_def-1 nil 3299406886
("" (expand "convergence")
(("" (expand "convergence")
(("" (expand "fullset") (("" (propax) nil nil)) nil)) nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_functions nil)
(fullset const-decl "set" sets nil)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(adherence_fullset 0
(adherence_fullset-1 nil 3299406886
("" (auto-rewrite "fullset" "member_adherent[T]")
(("" (skolem!) (("" (assert) nil nil)) nil)) nil)
((fullset const-decl "set" sets nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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)
(member_adherent formula-decl nil convergence_functions nil))
nil))
(cv_unique 0
(cv_unique-1 nil 3299406886
("" (skosimp)
(("" (expand "convergence")
(("" (use "convergence_unicity[T]") (("" (assert) nil nil)) nil))
nil))
nil)
((convergence const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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)
(convergence_unicity formula-decl nil convergence_functions nil))
nil))
(cv_in_domain 0
(cv_in_domain-1 nil 3299406886
("" (skosimp)
(("" (expand "convergence")
(("" (use "convergence_in_domain[T]")
(("" (expand "fullset") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((convergence const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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)
(convergence_in_domain formula-decl nil convergence_functions nil))
nil))
(cv_sum 0
(cv_sum-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_sum[T]") nil nil))
nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(convergence_sum formula-decl nil convergence_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_diff 0
(cv_diff-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_diff[T]") nil nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(convergence_diff formula-decl nil convergence_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_prod 0
(cv_prod-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_prod[T]") nil nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(convergence_prod formula-decl nil convergence_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_const 0
(cv_const-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_const[T]") nil nil))
nil)
((convergence_const formula-decl nil convergence_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_scal 0
(cv_scal-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_scal[T]") nil nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(convergence_scal formula-decl nil convergence_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_neg 0
(cv_neg-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_neg[T]") nil nil))
nil)
((minus_real_is_real application-judgement "real" reals nil)
(convergence_neg formula-decl nil convergence_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_div 0
(cv_div-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_div[T]") nil nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(convergence_div formula-decl nil convergence_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_inv 0
(cv_inv-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_inv[T]") nil nil))
nil)
((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(convergence_inv formula-decl nil convergence_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_identity 0
(cv_identity-1 nil 3299406886
("" (expand "convergence")
(("" (grind :defs nil :rewrites "convergence_identity[T]") nil
nil))
nil)
((convergence_identity formula-decl nil convergence_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(cv_abs 0
(cv_abs-2 nil 3299407298
("" (expand "convergence")
(("" (skosimp*)
(("" (expand "restrict")
(("" (expand "convergence")
(("" (skosimp*)
(("" (expand "fullset")
(("" (inst + "epsilon!1")
(("" (skosimp*) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_functions nil)
(fullset const-decl "set" sets nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_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)
(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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(restrict const-decl "R" restrict nil)
(convergence const-decl "bool" lim_of_functions nil))
nil)
(cv_abs-1 nil 3299406896
("" (expand "convergence")
(("" (skosimp*)
(("" (expand "restrict")
(("" (expand "convergence")
(("" (prop)
(("1" (lemma "adherence_fullset")
(("1" (inst?)
(("1" (assert)
(("1" (typepred "a!1") (("1" (postpone) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "fullset")
(("2" (inst + "epsilon!1")
(("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(conv_0_0_abs 0
(conv_0_0_abs-1 nil 3299423322
("" (skosimp*)
(("" (prop)
(("1" (expand "convergence")
(("1" (expand "fullset")
(("1" (expand "convergence")
(("1" (flatten)
(("1" (assert)
(("1" (skosimp*)
(("1" (inst -2 "epsilon!1")
(("1" (skosimp*)
(("1" (inst + "delta!1")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "convergence")
(("2" (expand "fullset")
(("2" (expand "convergence")
(("2" (flatten)
(("2" (assert)
(("2" (skosimp*)
(("2" (inst -2 "epsilon!1")
(("2" (skosimp*)
(("2" (inst + "delta!1")
(("2" (skosimp*)
(("2" (inst?)
(("2" (assert) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fullset const-decl "set" sets nil)
(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)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(adh const-decl "setof[real]" convergence_functions nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(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)
(convergence const-decl "bool" convergence_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" lim_of_functions nil))
nil))
(lim_TCC1 0
(lim_TCC1-1 nil 3445335777
(""
(inst + "(LAMBDA (d: [f: [T -> real], {a | convergent?(f, a)}]):
choose(LAMBDA l : convergence(d`1, d`2, l)))")
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (expand "convergence")
(("" (typepred "d!1`2")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (inst - "l!1")
(("" (expand "convergence" -1)
(("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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))
(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)
(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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(epsilon_ax formula-decl nil epsilons nil)
(pred type-eq-decl nil defined_types 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 lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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 lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil))
nil))
(lim_e_del 0
(lim_e_del-1 nil 3474799555
("" (skosimp*)
(("" (rewrite "lim_fun_def")
(("" (expand "convergence")
(("" (expand "fullset")
(("" (expand "convergence")
(("" (typepred "l!1")
(("" (split +)
(("1" (flatten) nil nil)
("2" (flatten)
(("2" (split +)
(("1" (expand "adh")
(("1" (skosimp*)
(("1" (assert)
(("1" (expand "convergent?")
(("1" (skosimp*)
(("1"
(expand "convergence")
(("1"
(expand "convergence")
(("1"
(flatten)
(("1"
(expand "adh")
(("1"
(inst -3 "e!1")
(("1"
(skosimp*)
(("1"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lim_fun_def formula-decl nil lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" lim_of_functions nil)
(fullset const-decl "set" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(adh const-decl "setof[real]" convergence_functions 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)
(convergence const-decl "bool" convergence_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(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" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions nil))
nil))
(convergent_in_domain 0
(convergent_in_domain-1 nil 3445684497
("" (grind :exclude "convergence")
(("" (forward-chain "cv_in_domain") (("" (assert) nil nil)) nil))
nil)
((cv_in_domain formula-decl nil lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions 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 lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(convergent? const-decl "bool" lim_of_functions nil)
(convergent_in_domain formula-decl nil lim_of_functions nil))
nil))
(sum_fun_convergent 0
(sum_fun_convergent-2 nil 3445684383
("" (expand "convergent?")
(("" (skosimp*)
(("" (inst 1 "l!1 + l!2") (("" (rewrite "cv_sum") nil nil)) nil))
nil))
nil)
((T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(cv_sum formula-decl nil lim_of_functions 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" lim_of_functions nil))
nil)
(sum_fun_convergent-1 nil 3299406886
("" (expand "convergent")
(("" (skosimp*)
(("" (inst 1 "l!1 + l!2") (("" (rewrite "cv_sum") nil nil)) nil))
nil))
nil)
nil nil))
(neg_fun_convergent 0
(neg_fun_convergent-2 nil 3445684395
("" (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)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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 lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil))
nil)
(neg_fun_convergent-1 nil 3299406886
("" (expand "convergent")
(("" (skosimp*)
(("" (forward-chain "cv_neg") (("" (inst?) nil nil)) nil)) nil))
nil)
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)
((T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(cv_diff formula-decl nil lim_of_functions 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" lim_of_functions 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)
((T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(cv_prod formula-decl nil lim_of_functions 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" lim_of_functions 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 lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions nil)
(adh const-decl "setof[real]" convergence_functions nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(convergent? const-decl "bool" lim_of_functions 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)
((T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(cv_scal formula-decl nil lim_of_functions 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" lim_of_functions 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 lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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" lim_of_functions 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 lim_of_functions 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 lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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" lim_of_functions 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 lim_of_functions nil))
nil))
(convergent_identity 0
(convergent_identity-1 nil 3299406886
("" (skolem!)
(("" (expand "convergent?")
(("" (use "cv_identity") (("" (inst?) nil nil)) nil)) nil))
nil)
((convergent? const-decl "bool" lim_of_functions nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions nil)
(adh const-decl "setof[real]" convergence_functions nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(cv_identity formula-decl nil lim_of_functions 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 lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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 lim_of_functions nil)
(cv_sum formula-decl nil lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions 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 lim_of_functions 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 lim_of_functions nil)
(cv_neg formula-decl nil lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions 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 lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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 lim_of_functions nil)
(cv_diff formula-decl nil lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions 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 lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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 lim_of_functions nil)
(cv_prod formula-decl nil lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions 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 lim_of_functions 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 lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions 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 lim_of_functions 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 lim_of_functions nil)
(cv_scal formula-decl nil lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions 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 lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(cv_inv formula-decl nil lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions 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 lim_of_functions 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]" lim_of_functions nil)
(T formal-subtype-decl nil lim_of_functions 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)
(cv_div formula-decl nil lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions nil))
nil))
(lim_identity_TCC1 0
(lim_identity_TCC1-1 nil 3299406886
("" (lemma "convergent_identity") (("" (propax) nil nil)) nil)
((convergent_identity formula-decl nil lim_of_functions nil)) nil))
(lim_identity 0
(lim_identity-1 nil 3299406886
(""
(auto-rewrite "lim_fun_lemma" "lim_fun_def" "convergent_identity"
"cv_identity")
(("" (skolem!) (("" (assert) nil nil)) nil)) nil)
((cv_identity formula-decl nil lim_of_functions nil)
(lim_fun_def formula-decl nil lim_of_functions nil))
nil))
(lim_le1 0
(lim_le1-1 nil 3299406886
("" (skosimp)
(("" (assert)
(("" (name-replace "ll" "lim(f!1, a!1)" :hide? nil)
(("" (rewrite "lim_fun_def")
(("" (expand "convergence")
(("" (use "convergence_upper_bound[T]")
(("" (ground)
(("" (delete -1 -2 2) (("" (grind) nil nil)) nil))
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 lim_of_functions nil)
(convergence_upper_bound formula-decl nil convergence_functions
nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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))
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")
(("" (expand "convergence")
(("" (use "convergence_lower_bound[T]" ("b" "b!1"))
(("" (ground)
(("" (delete -1 -2 2)
(("" (grind :if-match nil)
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
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 lim_of_functions nil)
(convergence_lower_bound formula-decl nil convergence_functions
nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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))
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")
(("" (expand "convergence")
((""
(use "convergence_order[T]" ("l1" "ll1" "l2" "ll2"))
(("" (ground)
(("" (expand "fullset" +) (("" (propax) nil nil))
nil))
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 convergence_functions nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(lim_fun_def formula-decl nil lim_of_functions nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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))
nil))
(lim_le2 0
(lim_le2-1 nil 3299406886
("" (skosimp)
(("" (assert)
(("" (name-replace "ll" "lim(f!1, a!1)" :hide? nil)
(("" (rewrite "lim_fun_def")
(("" (expand "convergence")
(("" (use "subset_convergence2[T]" ("E1" "E!1"))
(("" (ground)
(("1" (delete -2 -3)
(("1" (use "convergence_upper_bound[T]")
(("1" (assert) nil nil)) nil))
nil)
("2" (rewrite "subset_fullset") nil nil))
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 lim_of_functions nil)
(setof type-eq-decl nil defined_types nil)
(subset_convergence2 formula-decl nil convergence_functions nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(adh const-decl "setof[real]" convergence_functions nil)
(subset_fullset formula-decl nil sets_lemmas nil)
(convergence_upper_bound formula-decl nil convergence_functions
nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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))
nil))
(lim_ge2 0
(lim_ge2-1 nil 3299406886
("" (skosimp)
(("" (assert)
(("" (name-replace "ll" "lim(f!1, a!1)" :hide? nil)
(("" (rewrite "lim_fun_def")
(("" (expand "convergence")
(("" (use "subset_convergence2[T]" ("E1" "E!1"))
(("" (ground)
(("1" (delete -2 -3)
(("1" (use "convergence_lower_bound[T]" ("b" "b!1"))
(("1" (ground)
(("1" (delete -1 -2 2)
(("1" (skosimp)
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "subset_fullset") nil nil))
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 lim_of_functions nil)
(setof type-eq-decl nil defined_types nil)
(subset_convergence2 formula-decl nil convergence_functions nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(adh const-decl "setof[real]" convergence_functions nil)
(subset_fullset formula-decl nil sets_lemmas nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(convergence_lower_bound formula-decl nil convergence_functions
nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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))
nil))
(lim_order2 0
(lim_order2-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")
(("" (expand "convergence")
(("" (use "subset_convergence2[T]" ("E1" "E!1"))
((""
(use "subset_convergence2[T]"
("E1" "E!1" "f" "f1!1"))
(("" (rewrite "subset_fullset")
(("" (ground)
(("" (delete -3 -4 -5 -6)
(("" (forward-chain "convergence_order[T]")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(setof type-eq-decl nil defined_types nil)
(subset_convergence2 formula-decl nil convergence_functions nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(adh const-decl "setof[real]" convergence_functions nil)
(subset_fullset formula-decl nil sets_lemmas nil)
(convergence_order formula-decl nil convergence_functions nil)
(lim_fun_def formula-decl nil lim_of_functions nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil lim_of_functions nil)
(T_pred const-decl "[real -> boolean]" lim_of_functions 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))
nil)))
[ Dauer der Verarbeitung: 0.235 Sekunden
(vorverarbeitet)
]
|
