| products/Sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sigma_bijection.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.56 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.Bot Zugriff |
