| products/sources/formale sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: metric_space_real_fun.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(convergence_functions
(member_adherent 0 (member_adherent-2 nil 3442327308 ("" (grind :defs nil :rewrites ("adh" "abs_0")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs_nat formula-decl nil abs_lems "reals/") (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) (adh const-decl "setof[real]" convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (member_adherent-1 nil 3442076461 ("" (grind :defs nil :rewrites ("adh" "abs_0")) nil nil) ((abs_nat formula-decl nil abs_lems "reals/")) nil)) (adherence_subset1 0 (adherence_subset1-2 nil 3442327308 ("" (grind :if-match nil :defs nil :rewrites ("subset?" "member" "adh")) (("" (inst? -5) (("" (skosimp) (("" (inst? -4) (("" (inst? 1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (adh const-decl "setof[real]" convergence_functions nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil)) nil) (adherence_subset1-1 nil 3442076461 ("" (grind :if-match nil :defs nil :rewrites ("subset?" "member" "adh")) (("" (inst? -5) (("" (skosimp) (("" (inst? -4) (("" (inst? 1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (adherence_subset2 0 (adherence_subset2-2 nil 3442327308 ("" (expand "subset?" 1 2) (("" (expand "member") (("" (skosimp*) (("" (forward-chain "adherence_subset1") nil nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (adherence_subset1 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) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (subset? const-decl "bool" sets nil)) nil) (adherence_subset2-1 nil 3442076461 ("" (expand "subset?" 1 2) (("" (expand "member") (("" (skosimp*) (("" (forward-chain "adherence_subset1") nil nil)) nil)) nil)) nil) nil nil)) (adherence_prop1 0 (adherence_prop1-2 nil 3442327308 ("" (skolem-typepred) (("" (expand "adh") (("" (inst?) nil nil)) nil)) nil) ((adh const-decl "setof[real]" convergence_functions nil) (setof type-eq-decl nil defined_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (adherence_prop1-1 nil 3442076461 ("" (skolem-typepred) (("" (expand "adh") (("" (inst?) nil nil)) nil)) nil) nil nil)) (adherence_prop2 0 (adherence_prop2-2 nil 3442327308 ("" (skolem!) (("" (use "adherence_prop1" ("e" "min(e1!1, e2!1)" "E" "E!1")) (("" (skosimp) (("" (inst?) (("" (ground) nil nil)) nil)) nil)) nil)) nil) ((posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (adherence_prop1 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (setof type-eq-decl nil defined_types nil) (adh const-decl "setof[real]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (adherence_prop2-1 nil 3442076461 ("" (skolem!) (("" (use "adherence_prop1" ("e" "min(e1!1, e2!1)" "E" "E!1")) (("" (skosimp) (("" (inst?) (("" (ground) nil nil)) nil)) nil)) nil)) nil) nil nil)) (convergence_unicity 0 (convergence_unicity-2 nil 3442327308 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4) (("" (rewrite "abs_diff_0") (("" (name "eps" "abs(l1!1 - l2!1)") (("" (assert) (("" (inst -2 "eps/2") (("" (inst -3 "eps/2") (("" (skosimp*) (("" (lemma "adherence_prop2" ("E" "E!1" "e1" "delta!1" "e2" "delta!2" "a" "a!1")) (("" (skosimp) (("" (inst?) (("" (inst?) (("" (assert) (("" (delete -2 -3 1) (("" (use "triangle2" ("y" "l2!1" "b" "eps/2")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (triangle2 formula-decl nil abs_lems "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (adh const-decl "setof[real]" convergence_functions nil) (setof type-eq-decl nil defined_types nil) (adherence_prop2 formula-decl nil convergence_functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (abs_diff_0 formula-decl nil abs_lems "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_unicity-1 nil 3442076461 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4) (("" (rewrite "abs_diff_0") (("" (name "eps" "abs(l1!1 - l2!1)") (("" (assert) (("" (inst -2 "eps/2") (("" (inst -3 "eps/2") (("" (skosimp*) (("" (lemma "adherence_prop2" ("E" "E!1" "e1" "delta!1" "e2" "delta!2" "a" "a!1")) (("" (skosimp) (("" (inst?) (("" (inst?) (("" (assert) (("" (delete -2 -3 1) (("" (use "triangle2" ("y" "l2!1" "b" "eps/2")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((triangle2 formula-decl nil abs_lems "reals/") (abs_diff_0 formula-decl nil abs_lems "reals/")) nil)) (subset_convergence 0 (subset_convergence-2 nil 3442327308 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (inst? -7) (("" (skolem!) (("" (inst 1 "delta!1") (("" (skosimp) (("" (inst? -5) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (setof type-eq-decl nil defined_types nil) (adh const-decl "setof[real]" convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil)) nil) (subset_convergence-1 nil 3442076461 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (inst? -7) (("" (skolem!) (("" (inst 1 "delta!1") (("" (skosimp) (("" (inst? -5) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (subset_convergence2 0 (subset_convergence2-2 nil 3442327308 ("" (skosimp) (("" (forward-chain "subset_convergence") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((subset_convergence 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) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (adh const-decl "setof[real]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil)) nil) (subset_convergence2-1 nil 3442076461 ("" (skosimp) (("" (forward-chain "subset_convergence") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) nil nil)) (convergence_in_domain 0 (convergence_in_domain-2 nil 3442327308 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (rewrite "abs_diff_0") (("" (inst -5 "abs(l!1 - f!1(x!1))") (("1" (skolem!) (("1" (inst?) (("1" (assert) (("1" (rewrite "abs_diff_commute" -) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((abs_diff_0 formula-decl nil abs_lems "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs_nat formula-decl nil abs_lems "reals/") (adh const-decl "setof[real]" convergence_functions nil) (x!1 skolem-const-decl "T" convergence_functions nil) (abs_diff_commute formula-decl nil abs_lems "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_in_domain-1 nil 3442076461 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (rewrite "abs_diff_0") (("" (assert) (("" (inst -5 "abs(l!1 - f!1(x!1))") (("" (skolem!) (("" (inst?) (("" (assert) (("" (rewrite "abs_0") (("" (assert) (("" (rewrite "abs_diff_commute" -) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_diff_0 formula-decl nil abs_lems "reals/") (abs_nat formula-decl nil abs_lems "reals/") (abs_diff_commute formula-decl nil abs_lems "reals/")) nil)) (convergence_sum 0 (convergence_sum-2 nil 3442327308 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4 -5 -6) (("" (inst -1 "epsilon!1/2") (("" (inst -2 "epsilon!1/2") (("" (skosimp*) (("" (inst 1 "min(delta!1, delta!2)") (("" (skosimp) (("" (inst?) (("" (inst?) (("" (assert) (("" (lemma "triangle" ("x" "f1!1(x!1) - l1!1" "y" "f2!1(x!1) - l2!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (triangle formula-decl nil real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_sum-1 nil 3442076461 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4 -5 -6) (("" (inst -1 "epsilon!1/2") (("" (inst -2 "epsilon!1/2") (("" (skosimp*) (("" (inst 1 "min(delta!1, delta!2)") (("" (skosimp) (("" (inst?) (("" (inst?) (("" (assert) (("" (lemma "triangle" ("x" "f1!1(x!1) - l1!1" "y" "f2!1(x!1) - l2!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (convergence_neg 0 (convergence_neg-2 nil 3442327308 ("" (grind :if-match nil :exclude ("abs" "adh")) (("" (delete -1 -2 -3 -4 -5) (("" (inst -1 "epsilon!1") (("" (skolem!) (("" (inst 1 "delta!1") (("" (skosimp) (("" (inst?) (("" (assert) (("" (lemma "abs_neg" ("x" "f1!1(x!1) - l1!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (abs_neg formula-decl nil abs_lems "reals/") (T_pred const-decl "[real -> boolean]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_neg-1 nil 3442076461 ("" (grind :if-match nil :exclude ("abs" "adh")) (("" (delete -1 -2 -3 -4 -5) (("" (inst -1 "epsilon!1") (("" (skolem!) (("" (inst 1 "delta!1") (("" (skosimp) (("" (inst?) (("" (assert) (("" (lemma "abs_neg" ("x" "f1!1(x!1) - l1!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_neg formula-decl nil abs_lems "reals/")) nil)) (convergence_diff 0 (convergence_diff-2 nil 3442327308 ("" (skosimp) (("" (rewrite "diff_function") (("" (use "convergence_sum" ("f2" "-f2!1" "l2" "-l2!1")) (("" (assert) (("" (rewrite "convergence_neg") nil nil)) nil)) nil)) nil)) nil) ((diff_function formula-decl nil real_fun_ops "reals/") (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]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (convergence_neg formula-decl nil convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (convergence_sum formula-decl nil convergence_functions nil) (minus_real_is_real application-judgement "real" reals nil)) nil) (convergence_diff-1 nil 3442076461 ("" (skosimp) (("" (rewrite "diff_function") (("" (use "convergence_sum" ("f2" "-f2!1" "l2" "-l2!1")) (("" (assert) (("" (rewrite "convergence_neg") nil nil)) nil)) nil)) nil)) nil) ((diff_function formula-decl nil real_fun_ops "reals/")) nil)) (convergence_prod 0 (convergence_prod-2 nil 3442327308 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4 -5 -6) (("" (lemma "prod_epsilon" ("y1" "l1!1" "y2" "l2!1" "e" "epsilon!1")) (("" (skolem!) (("" (inst -2 "e1!1") (("" (inst -3 "e2!1") (("" (skosimp*) (("" (inst 1 "min(delta!1, delta!2)") (("" (skosimp) (("" (inst?) (("" (inst?) (("" (assert) (("" (lemma "prod_bound") (("" (inst -1 "e1!1" "e2!1" "f1!1(x!1)" "f2!1(x!1)" "l1!1" "l2!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (prod_bound formula-decl nil epsilon_lemmas nil) (prod_epsilon formula-decl nil epsilon_lemmas nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_prod-1 nil 3442076461 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4 -5 -6) (("" (lemma "prod_epsilon" ("y1" "l1!1" "y2" "l2!1" "e" "epsilon!1")) (("" (skolem!) (("" (inst -2 "e1!1") (("" (inst -3 "e2!1") (("" (skosimp*) (("" (inst 1 "min(delta!1, delta!2)") (("" (skosimp) (("" (inst?) (("" (inst?) (("" (assert) (("" (lemma "prod_bound") (("" (inst -1 "e1!1" "e2!1" "f1!1(x!1)" "f2!1(x!1)" "l1!1" "l2!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((prod_bound formula-decl nil epsilon_lemmas nil) (prod_epsilon formula-decl nil epsilon_lemmas nil)) nil)) (convergence_const 0 (convergence_const-2 nil 3442327308 ("" (expand "convergence") (("" (skosimp*) (("" (auto-rewrite "abs_0") (("" (expand "const_fun") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((abs_nat formula-decl nil abs_lems "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (convergence const-decl "bool" convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (convergence_const-1 nil 3442076461 ("" (expand "convergence") (("" (skosimp*) (("" (auto-rewrite "abs_0") (("" (expand "const_fun") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((abs_nat formula-decl nil abs_lems "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (convergence_scal 0 (convergence_scal-2 nil 3442327308 ("" (skosimp) (("" (rewrite "scal_function") (("" (rewrite "convergence_prod") (("" (rewrite "convergence_const") (("" (expand "convergence" -) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((scal_function formula-decl nil real_fun_ops "reals/") (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]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (adh const-decl "setof[real]" convergence_functions nil) (convergence_const formula-decl nil convergence_functions nil) (convergence const-decl "bool" convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (convergence_prod formula-decl nil convergence_functions nil)) nil) (convergence_scal-1 nil 3442076461 ("" (skosimp) (("" (rewrite "scal_function") (("" (rewrite "convergence_prod") (("" (rewrite "convergence_const") (("" (expand "convergence" -) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((scal_function formula-decl nil real_fun_ops "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (convergence_inv 0 (convergence_inv-2 nil 3442327308 ("" (grind :if-match nil :exclude ("abs" "adh")) (("" (delete -1 -2 -3 -4 -5) (("" (lemma "inv_epsilon" ("y1" "l1!1" "e" "epsilon!1")) (("" (assert) (("" (skosimp) (("" (inst? -3) (("" (skolem!) (("" (inst 2 "delta!1") (("" (skosimp) (("" (inst?) (("" (assert) (("" (lemma "inv_bound" ("e1" "e1!1" "x1" "g!1(x!1)" "y1" "l1!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (inv_bound formula-decl nil epsilon_lemmas nil) (nzreal nonempty-type-eq-decl nil reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (inv_epsilon formula-decl nil epsilon_lemmas nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (/= const-decl "boolean" notequal nil) (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_inv-1 nil 3442076461 ("" (grind :if-match nil :exclude ("abs" "adh")) (("" (delete -1 -2 -3 -4 -5) (("" (lemma "inv_epsilon" ("y1" "l1!1" "e" "epsilon!1")) (("" (assert) (("" (skosimp) (("" (inst? -3) (("" (skolem!) (("" (inst 2 "delta!1") (("" (skosimp) (("" (inst?) (("" (assert) (("" (lemma "inv_bound" ("e1" "e1!1" "x1" "g!1(x!1)" "y1" "l1!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inv_bound formula-decl nil epsilon_lemmas nil) (inv_epsilon formula-decl nil epsilon_lemmas nil)) nil)) (convergence_div 0 (convergence_div-2 nil 3442327308 ("" (skosimp) (("" (rewrite "div_function") (("" (assert) (("" (use "convergence_prod" ("l2" "1/l2!1")) (("" (assert) (("" (rewrite "convergence_inv") nil nil)) nil)) nil)) nil)) nil)) nil) ((div_function formula-decl nil real_fun_ops "reals/") (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals 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]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions 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) (convergence_prod formula-decl nil convergence_functions nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (convergence_inv formula-decl nil convergence_functions nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil) (convergence_div-1 nil 3442076461 ("" (skosimp) (("" (rewrite "div_function") (("" (assert) (("" (use "convergence_prod" ("l2" "1/l2!1")) (("" (assert) (("" (rewrite "convergence_inv") nil nil)) nil)) nil)) nil)) nil)) nil) ((div_function formula-decl nil real_fun_ops "reals/")) nil)) (convergence_identity 0 (convergence_identity-2 nil 3442327308 ("" (grind :exclude ("adh" "abs")) nil nil) ((real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil) (I const-decl "(bijective?[T, T])" identity nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" 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) (adh const-decl "setof[real]" convergence_functions nil) (setof type-eq-decl nil defined_types 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)) nil) (convergence_identity-1 nil 3442076461 ("" (grind :exclude ("adh" "abs")) nil nil) nil nil)) (convergence_order 0 (convergence_order-2 nil 3442327308 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4) (("" (case "l2!1 < l1!1") (("1" (name "eps" "(l1!1 - l2!1)/2") (("1" (assert) (("1" (inst -3 "eps") (("1" (inst -4 "eps") (("1" (skosimp*) (("1" (lemma "adherence_prop2" ("e1" "delta!1" "e2" "delta!2" "E" "E!1" "a" "a!1")) (("1" (skosimp) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (delete -2 -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (adh const-decl "setof[real]" convergence_functions nil) (setof type-eq-decl nil defined_types nil) (adherence_prop2 formula-decl nil convergence_functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_order-1 nil 3442076461 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4) (("" (case "l2!1 < l1!1") (("1" (name "eps" "(l1!1 - l2!1)/2") (("1" (assert) (("1" (inst -3 "eps") (("1" (inst -4 "eps") (("1" (skosimp*) (("1" (lemma "adherence_prop2" ("e1" "delta!1" "e2" "delta!2" "E" "E!1" "a" "a!1")) (("1" (skosimp) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (delete -2 -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) nil nil)) (convergence_lower_bound 0 (convergence_lower_bound-2 nil 3442327308 ("" (skosimp) (("" (use "convergence_const" ("b" "b!1")) (("1" (use "convergence_order" ("f2" "f!1")) (("1" (auto-rewrite "const_fun") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "convergence") (("2" (propax) nil nil)) nil)) 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) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (adh const-decl "setof[real]" convergence_functions nil) (E!1 skolem-const-decl "setof[real]" convergence_functions nil) (a!1 skolem-const-decl "real" convergence_functions nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (convergence_order formula-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_lower_bound-1 nil 3442076461 ("" (skosimp) (("" (use "convergence_const" ("b" "b!1")) (("1" (use "convergence_order" ("f2" "f!1")) (("1" (auto-rewrite "const_fun") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "convergence") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((const_fun const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (convergence_upper_bound 0 (convergence_upper_bound-2 nil 3442327308 ("" (skosimp) (("" (use "convergence_const" ("b" "b!1")) (("1" (use "convergence_order" ("f1" "f!1")) (("1" (auto-rewrite "const_fun") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "convergence") (("2" (propax) nil nil)) nil)) 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) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (adh const-decl "setof[real]" convergence_functions nil) (E!1 skolem-const-decl "setof[real]" convergence_functions nil) (a!1 skolem-const-decl "real" convergence_functions nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (convergence_order formula-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (T formal-subtype-decl nil convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_upper_bound-1 nil 3442076461 ("" (skosimp) (("" (use "convergence_const" ("b" "b!1")) (("1" (use "convergence_order" ("f1" "f!1")) (("1" (auto-rewrite "const_fun") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "convergence") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((const_fun const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (convergence_locally_constant 0 (convergence_locally_constant-2 nil 3442327308 ("" (grind :if-match nil :exclude ("abs" "adh")) (("" (inst 1 "epsilon!1") (("" (skosimp) (("" (inst?) (("" (assert) (("" (expand "abs") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (setof type-eq-decl nil defined_types nil) (adh const-decl "setof[real]" convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_locally_constant-1 nil 3442076461 ("" (grind :if-match nil :exclude ("abs" "adh")) (("" (inst 1 "epsilon!1") (("" (skosimp) (("" (inst?) (("" (assert) (("" (expand "abs") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (convergence_squeezing 0 (convergence_squeezing-2 nil 3442327308 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4 -5) (("" (inst -1 "epsilon!1/2") (("" (inst -2 "epsilon!1/2") (("" (skosimp*) (("" (inst 1 "min(delta!1, delta!2)") (("" (skosimp) (("" (inst?) (("" (inst?) (("" (inst?) (("" (ground) (("" (delete -6) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (T formal-subtype-decl nil convergence_functions nil) (T_pred const-decl "[real -> boolean]" convergence_functions nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_le_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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_functions nil)) nil) (convergence_squeezing-1 nil 3442076461 ("" (grind :exclude ("abs" "adh") :if-match nil) (("" (delete -1 -2 -3 -4 -5) (("" (inst -1 "epsilon!1/2") (("" (inst -2 "epsilon!1/2") (("" (skosimp*) (("" (inst 1 "min(delta!1, delta!2)") (("" (skosimp) (("" (inst?) (("" (inst?) (("" (inst?) (("" (ground) (("" (delete -6) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil))) ¤ Dauer der Verarbeitung: 0.57 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 |
