| products/sources/formale sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: csequence_merge.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(riesz_representation
(IMP_rs_integral_cont_TCC1 0 (IMP_rs_integral_cont_TCC1-1 nil 3511191506 ("" (expand "connected?") (("" (skosimp*) (("" (ground) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def nil)) nil)) (IMP_rs_integral_cont_TCC2 0 (IMP_rs_integral_cont_TCC2-1 nil 3511191506 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "a") (("" (inst + "b") (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_representation nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def nil)) nil)) (integral_norm_bounded_TCC1 0 (integral_norm_bounded_TCC1-1 nil 3492953409 ("" (subtype-tcc) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (integral_norm_bounded_TCC2 0 (integral_norm_bounded_TCC2-1 nil 3492953409 ("" (subtype-tcc) nil 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)) nil)) (integral_norm_bounded_TCC3 0 (integral_norm_bounded_TCC3-1 nil 3492953409 ("" (skolem 1 ("ff" "gg")) (("" (flatten) (("" (lemma "continuous_implies_bounded[a,b]") (("" (inst - "ff") (("" (expand "zero_off_int_and_bounded?") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (INTab type-eq-decl nil riesz_interval_funs nil) (continuous_on_int? const-decl "bool" riesz_interval_funs nil) (Continuous_Function type-eq-decl nil riesz_interval_funs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (continuous_implies_bounded formula-decl nil riesz_interval_funs 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) (a formal-const-decl "real" riesz_representation nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation nil)) nil)) (integral_norm_bounded 0 (integral_norm_bounded-1 nil 3492953409 ("" (skolem 1 ("ff" "gg")) (("" (case "NOT integrable?(a,b,gg,ff)") (("1" (hide 2) (("1" (lemma "RS_integrable_cont_BV") (("1" (inst - "a" "b" "ff" "gg") (("1" (assert) (("1" (typepred "ff") (("1" (expand "continuous_on_int?") (("1" (expand "continuous?") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "restrict" +) (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict" +) (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "fint" -1) (("2" (assert) (("2" (name "SS" "integral(a,b,gg,ff)") (("2" (label "SSname" -1) (("2" (lemma "integral_def") (("2" (inst - "a" "b" "ff" "gg" "SS") (("2" (split -) (("1" (flatten) (("1" (hide -2) (("1" (split -) (("1" (label "integrall?" -1) (("1" (case "FORALL (P:partition(a,b),xis:xis?(a,b,P)): abs(Rie_sum(a,b,gg,P,xis,ff)) <= total_variation(a,b,gg)(b)*fun_norm(ff)") (("1" (case "FORALL (eps:posreal): abs(integral(a, b, gg, ff)) <= total_variation(a, b, gg)(b) * fun_norm(ff)+eps") (("1" (inst - "(abs(integral(a, b, gg, ff)) - total_variation(a, b, gg)(b) * fun_norm(ff))/10") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "integral?") (("2" (skeep) (("2" (inst "integrall?" "eps/10") (("2" (skosimp*) (("2" (lemma "partition_exists") (("2" (inst - "a" "b" "delta!1") (("2" (assert) (("2" (skosimp*) (("2" (name "xis" "gen_xis(a,b,P!1)") (("2" (inst - "P!1" "xis") (("2" (inst - "P!1") (("2" (assert) (("2" (inst - "Rie_sum(a,b,gg,P!1,xis,ff)") (("1" (grind :exclude ("gen_xis" "width" "Rie_sum" "total_variation" "integral" "integrable?")) nil nil) ("2" (lemma "Riemann?_Rie") (("2" (inst - "a" "b" "ff" "gg") (("2" (split -) (("1" (inst - "P!1" "xis") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "Rie_sum") (("2" (lemma "sigma_abs[below(P`length-1)]") (("2" (inst?) (("2" (case "sigma(0, P`length - 2, LAMBDA (n_1: below(P`length - 1)): abs(ff(xis`seq(n_1)) * gg(P`seq(1 + n_1)) - ff(xis`seq(n_1)) * gg(P`seq(n_1)))) <= total_variation(a, b, gg)(b) * fun_norm(ff)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (typepred "total_variation(a,b,gg)(b)") (("2" (assert) (("2" (inst - "P") (("2" (case "sigma(0, P`length - 2, LAMBDA (n_1: below(P`length - 1)): abs(ff(xis`seq(n_1)) * gg(P`seq(1 + n_1)) - ff(xis`seq(n_1)) * gg(P`seq(n_1)))) <= variation_on(a, b, P)(gg) * fun_norm(ff)") (("1" (mult-by -4 "fun_norm[a,b](ff)") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "variation_on") (("2" (lemma "sigma_scal[below(P`length-1)]") (("2" (inst - "LAMBDA (n: below(P`length - 1)): abs(gg(P`seq(1 + n)) - gg(P`seq(n)))" "fun_norm[a,b](ff)" "P`length-2" "0") (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (rewrite "sigma_le") (("2" (hide 2) (("2" (skeep) (("2" (typepred "n") (("2" (lemma "abs_mult") (("2" (inst - "ff(xis`seq(n))" "gg(P`seq(1 + n)) -gg(P`seq(n))") (("2" (replace -1) (("2" (case "abs(ff(xis`seq(n))) <= fun_norm(ff)") (("1" (mult-by -1 "abs(gg(P`seq(1 + n)) - gg(P`seq(n)))") nil nil) ("2" (typepred "fun_norm(ff)") (("2" (inst - "xis`seq(n)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (typepred "b") (("3" (assert) nil nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil) ((Continuous_Function type-eq-decl nil riesz_interval_funs nil) (continuous_on_int? const-decl "bool" riesz_interval_funs nil) (bounded_variation? const-decl "bool" bounded_variation nil) (integrable? const-decl "bool" rs_integral_def nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_representation nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" 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) (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_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) (RS_integrable_cont_BV formula-decl nil rs_integral_cont nil) (continuous_at? const-decl "bool" continuity_ms_def 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) (y!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (member const-decl "bool" sets nil) (x!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (TRUE const-decl "bool" booleans nil) (Intab const-decl "set[real]" riesz_interval_funs nil) (set type-eq-decl nil sets nil) (restrict const-decl "R" restrict nil) (continuous? const-decl "bool" continuity_ms_def nil) (fun_norm const-decl "{M: nnreal | (FORALL (x): abs(f(x)) <= M) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}" riesz_interval_funs nil) (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (total_variation const-decl "{M: nnreal | (x = a IMPLIES M = 0) AND (x > a IMPLIES (FORALL (P: partition(a, x)): variation_on(a, x, P)(f) <= M)) AND (FORALL (M1: nnreal): M1 < M IMPLIES (EXISTS (P: partition(a, x)): variation_on(a, x, P)(f) > M1))}" bounded_variation nil) (variation_on const-decl "nnreal" bounded_variation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (Rie_sum const-decl "real" rs_integral_def nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (xis? type-eq-decl nil rs_integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (increasing? const-decl "bool" sort_fseq "structures/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Riemann?_Rie formula-decl nil rs_integral_def nil) (minus_real_is_real application-judgement "real" reals nil) (xis skolem-const-decl "xis?[INTab](a, b, P!1)" riesz_representation nil) (ff skolem-const-decl "Continuous_Function[a, b]" riesz_representation nil) (gg skolem-const-decl "(bounded_variation?(a, b))" riesz_representation nil) (P!1 skolem-const-decl "partition[INTab](a, b)" riesz_representation nil) (Riemann_sum? const-decl "bool" rs_integral_def nil) (gen_xis const-decl "xis?(a, b, P)" rs_integral_def nil) (partition_exists formula-decl nil rs_partition 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_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (/= const-decl "boolean" notequal nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (sigma_abs formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_nnreal application-judgement "nnreal" sigma_below "reals/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (subrange type-eq-decl nil integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (abs_mult formula-decl nil real_props nil) (sigma_le formula-decl nil sigma "reals/") (sigma_scal formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (integral_def formula-decl nil rs_integral_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (integral? const-decl "bool" rs_integral_def nil) (integral const-decl "{S: real | integral?(a, b, gg, ff, S)}" rs_integral_def nil)) shostak)) (fun_to_op_TCC1 0 (fun_to_op_TCC1-1 nil 3492949849 ("" (skolem 1 ("gg" "ff")) (("" (lemma "RS_integrable_cont_BV") (("" (inst - "a" "b" "ff" "gg") (("" (assert) (("" (hide 2) (("" (typepred "ff") (("" (expand "continuous_on_int?") (("" (expand "restrict") (("" (expand "continuous?") (("" (skosimp*) (("" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_representation nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (RS_integrable_cont_BV formula-decl nil rs_integral_cont nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (restrict const-decl "R" restrict nil) (continuous_at? const-decl "bool" continuity_ms_def 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) (y!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (member const-decl "bool" sets nil) (x!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (TRUE const-decl "bool" booleans nil) (Intab const-decl "set[real]" riesz_interval_funs nil) (set type-eq-decl nil sets nil) (continuous? const-decl "bool" continuity_ms_def nil) (bounded_variation? const-decl "bool" bounded_variation nil) (Continuous_Function type-eq-decl nil riesz_interval_funs nil) (continuous_on_int? const-decl "bool" riesz_interval_funs nil)) nil)) (fun_to_op_TCC2 0 (fun_to_op_TCC2-1 nil 3492953553 ("" (skolem 1 "gg") (("" (expand "bounded_linear_operator?") (("" (split) (("1" (expand "bounded_op?") (("1" (inst + "total_variation(a,b,gg)(b)") (("1" (skolem 1 "f") (("1" (lemma "integral_norm_bounded") (("1" (inst - "f" "gg") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "b") (("2" (assert) nil nil)) nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil) ("2" (expand "linear_op?") (("2" (split) (("1" (expand "additive_op?") (("1" (skolem 1 ("ff" "hh")) (("1" (lemma "integral_sum") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (expand "+") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (typepred "ff") (("2" (lemma "RS_integrable_cont_BV") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (expand "continuous_on_int?") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "restrict") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "RS_integrable_cont_BV") (("3" (inst?) (("3" (assert) (("3" (hide 2) (("3" (typepred "hh") (("3" (expand "continuous_on_int?") (("3" (expand "continuous?") (("3" (skosimp*) (("3" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "restrict") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "const_inv_op?") (("2" (skolem 1 ("f" "c")) (("2" (lemma "integral_scal") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (lemma "RS_integrable_cont_BV") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (typepred "f") (("2" (expand "continuous_on_int?") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "restrict") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (expand "Intab") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_linear_operator? const-decl "bool" riesz_bounded_functionals nil) (linear_op? const-decl "bool" riesz_linear_functionals nil) (const_inv_op? const-decl "bool" riesz_linear_functionals nil) (integral_scal formula-decl nil rs_integral_prep nil) (real_times_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (y!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (additive_op? const-decl "bool" riesz_linear_functionals nil) (integral_sum formula-decl nil rs_integral_prep nil) (real_plus_real_is_real application-judgement "real" reals nil) (y!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (x!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (RS_integrable_cont_BV formula-decl nil rs_integral_cont nil) (continuous_at? const-decl "bool" continuity_ms_def nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (y!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (member const-decl "bool" sets nil) (x!1 skolem-const-decl "(LAMBDA (x: INTab[a, b]): TRUE)" riesz_representation nil) (TRUE const-decl "bool" booleans nil) (Intab const-decl "set[real]" riesz_interval_funs nil) (set type-eq-decl nil sets nil) (continuous? const-decl "bool" continuity_ms_def nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (bounded_op? const-decl "bool" riesz_bounded_functionals nil) (NOT const-decl "[bool -> bool]" booleans nil) (Continuous_Function type-eq-decl nil riesz_interval_funs nil) (continuous_on_int? const-decl "bool" riesz_interval_funs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (integral_norm_bounded formula-decl nil riesz_representation nil) (total_variation const-decl "{M: nnreal | (x = a IMPLIES M = 0) AND (x > a IMPLIES (FORALL (P: partition(a, x)): variation_on(a, x, P)(f) <= M)) AND (FORALL (M1: nnreal): M1 < M IMPLIES (EXISTS (P: partition(a, x)): variation_on(a, x, P)(f) > M1))}" bounded_variation nil) (variation_on const-decl "nnreal" bounded_variation nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bounded_variation? const-decl "bool" bounded_variation nil) (INTab type-eq-decl nil riesz_interval_funs nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (a formal-const-decl "real" riesz_representation nil) (< const-decl "bool" reals nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation 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)) nil)) (fun_to_op_bound_TCC1 0 (fun_to_op_bound_TCC1-1 nil 3492957266 ("" (subtype-tcc) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (fun_to_op_bound 0 (fun_to_op_bound-1 nil 3492957266 ("" (skolem 1 ("ff" "gg")) (("" (lemma "integral_norm_bounded") (("" (expand "fun_to_op") (("" (inst - "ff" "gg") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((integral_norm_bounded formula-decl nil riesz_representation 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (a formal-const-decl "real" riesz_representation nil) (< const-decl "bool" reals nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation nil) (INTab type-eq-decl nil riesz_interval_funs nil) (continuous_on_int? const-decl "bool" riesz_interval_funs nil) (Continuous_Function type-eq-decl nil riesz_interval_funs nil) (bounded_variation? const-decl "bool" bounded_variation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (fun_to_op const-decl "C_Bounded_Linear_Operator" riesz_representation nil)) shostak)) (char_fun_minus 0 (char_fun_minus-1 nil 3492957695 ("" (skeep) (("" (expand "-") (("" (expand "char_fun") (("" (decompose-equality) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((- const-decl "[T -> real]" real_fun_ops "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_representation nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (char_fun const-decl "nnreal" riesz_representation nil)) shostak)) (step_approx_TCC1 0 (step_approx_TCC1-1 nil 3492959104 ("" (subtype-tcc) nil nil) nil nil)) (step_approx_TCC2 0 (step_approx_TCC2-1 nil 3492959104 ("" (subtype-tcc) nil nil) nil nil)) (step_approx_TCC3 0 (step_approx_TCC3-1 nil 3492959104 ("" (subtype-tcc) 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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (a formal-const-decl "real" riesz_representation nil) (< const-decl "bool" reals nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation nil) (INTab type-eq-decl nil riesz_interval_funs nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (increasing? const-decl "bool" sort_fseq "structures/") (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil rs_partition nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (xis? type-eq-decl nil rs_integral_def nil) (bounded_on_int? const-decl "bool" riesz_interval_funs nil) (integer nonempty-type-from-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (step_approx_TCC4 0 (step_approx_TCC4-1 nil 3492959104 ("" (skeep) (("" (typepred "fr") (("" (expand "bounded_on_int?") (("" (skosimp*) (("" (inst + "M!1*(P`length+2)") (("" (skosimp*) (("" (case "FORALL (nnn:below(P`length-1)): abs(sigma[below(P`length - 1)] (0, nnn, LAMBDA (n: below(P`length - 1)): fr(xis`seq(n)) * char_fun(P`seq(n), P`seq(1 + n))(x!1))) <= M!1 * (nnn+4)") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "nnn") (("1" (flatten) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst - "xis`seq(0)") (("1" (expand "char_fun") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "nnn") (("2" (flatten) (("2" (expand "sigma" +) (("2" (inst - "xis`seq(1+nnn)") (("2" (grind :exclude "sigma") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_on_int? const-decl "bool" riesz_interval_funs nil) (INTab type-eq-decl nil riesz_interval_funs nil) (b formal-const-decl "{bb: real | a < bb}" riesz_representation nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riesz_representation nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" 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) (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) (minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_nat formula-decl nil abs_lems "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (below_induction formula-decl nil bounded_nat_inductions nil) (pred type-eq-decl nil defined_types 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (xis? type-eq-decl nil rs_integral_def nil) (char_fun const-decl "nnreal" riesz_representation nil) (partition type-eq-decl nil rs_partition nil) (below type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (increasing? const-decl "bool" sort_fseq "structures/") (restrict const-decl "R" restrict nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (step_approx_def 0 (step_approx_def-1 nil 3492960304 ("" (skeep) (("" (typepred "f") (("" (expand "continuous_on_int?") (("" (case "uniformly_continuous?[INTab,real_dist,real,real_dist](f,Intab)") (("1" (expand "uniformly_continuous?") (("1" (inst - "eps") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skeep) (("1" (label "Pwidth" -4) (("1" (label "Pinc" -3) (("1" (label "funif" -1) (("1" (hide -2) (("1" (skosimp*) (("1" (lemma "part_in") (("1" (case "FORALL (x: INTab, P: partition(a, b)): strictly_increasing?(P) IMPLIES (EXISTS (ii: below(P`length - 1)): P`seq(ii) <= x AND x <= P`seq(ii + 1) AND char_fun(P`seq(ii),P`seq(ii+1))(x) = 1)") (("1" (hide -2) (("1" (inst - "x!1" "P") (("1" (assert) (("1" (skosimp*) (("1" (case "step_approx(P,xis)(f)(x!1) = f(xis`seq(ii!1))") (("1" (inst "funif" "x!1" "xis`seq(ii!1)") (("1" (expand "real_dist") (("1" (assert) (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.102 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 |
