| products/sources/formale Sprachen/PVS/lnexp_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: allen_interval.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
(convergence_special
(conv_1_div_n 0 (conv_1_div_n-1 nil 3301929090 ("" (expand "convergence") (("" (skosimp*) (("" (inst + "ceiling(1/epsilon!1)") (("" (skosimp*) (("" (grind) (("" (cross-mult 1) (("" (assert) (("" (typepred "ceiling(1 / epsilon!1)") (("" (cross-mult -1) (("" (name-replace "C1dn" "ceiling(1 / epsilon!1)") (("" (mult-by -4 "epsilon!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_mult_pos_lt1 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs 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 "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil) (convergence const-decl "bool" convergence_sequences "analysis/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (conv_x_to_1_div_n_TCC1 0 (conv_x_to_1_div_n_TCC1-1 nil 3298641456 ("" (subtype-tcc) (("" (postpone) nil nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (conv_x_to_1_div_n 0 (conv_x_to_1_div_n-2 nil 3302276361 ("" (skosimp*) (("" (case-replace "convergence(LAMBDA n: 1/(n+1)*ln(px!1), 0)") (("1" (lemma "convergence_fun_of[real]") (("1" (assert) (("1" (inst - "0" "(LAMBDA n: 1 / (n + 1) * ln(px!1))" "exp") (("1" (expand "^^") (("1" (assert) (("1" (lemma "exp_continuous") (("1" (expand "continuous?" -1) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "conv_1_div_n") (("2" (lemma "cnv_seq_scal") (("2" (inst?) (("2" (inst - "ln(px!1)") (("2" (assert) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_times_real_is_real application-judgement "real" 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (convergence const-decl "bool" convergence_sequences "analysis/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (ln const-decl "real" ln_exp nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^^ const-decl "nnreal" expt nil) (exp_continuous formula-decl nil ln_exp nil) (continuous? const-decl "bool" continuous_functions "analysis/") (exp_0 formula-decl nil ln_exp nil) (= const-decl "[T, T -> boolean]" equalities nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil) (TRUE const-decl "bool" booleans nil) (convergence_fun_of formula-decl nil continuous_functions_more "analysis/") (conv_1_div_n formula-decl nil convergence_special nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (cnv_seq_scal formula-decl nil convergence_ops "analysis/")) nil) (conv_x_to_1_div_n-1 nil 3300103323 ("" (skosimp*) (("" (case-replace "convergence(LAMBDA n: 1/(n+1)*ln(px!1), 0)") (("1" (lemma "convergence_fun_of") (("1" (assert) (("1" (inst - "0" "(LAMBDA n: 1 / (n + 1) * ln(px!1))" "exp") (("1" (expand "^^") (("1" (assert) (("1" (lemma "exp_continuous") (("1" (expand "continuous?" -1) (("1" (inst?) (("1" (assert) (("1" (case-replace "(LAMBDA n: exp((1 / (1 + n)) * ln(px!1))) = (LAMBDA (n_1: nat): exp((1 / (1 + n_1)) * ln(px!1)))") (("1" (hide -1) (("1" (rewrite "exp_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "conv_1_div_n") (("2" (lemma "cnv_seq_scal") (("2" (inst?) (("2" (inst - "ln(px!1)") (("2" (assert) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergence const-decl "bool" convergence_sequences "analysis/") (ln const-decl "real" ln_exp nil) (^^ const-decl "nnreal" expt nil) (exp_continuous formula-decl nil ln_exp nil) (exp_0 formula-decl nil ln_exp nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil) (cnv_seq_scal formula-decl nil convergence_ops "analysis/")) shostak)) (conv_x_to_n_TCC1 0 (conv_x_to_n_TCC1-1 nil 3298641456 ("" (subtype-tcc) (("" (postpone) nil nil)) nil) ((/= const-decl "boolean" notequal nil)) shostak)) (conv_x_to_n 0 (conv_x_to_n-2 nil 3301933221 ("" (skosimp*) (("" (expand "convergence") (("" (skosimp*) (("" (lemma "conv_x_to_1_div_n") (("" (inst -1 "epsilon!1") (("" (case "(EXISTS (k: posnat): abs(x!1) < epsilon!1^^(1/k))") (("1" (skosimp*) (("1" (lemma "hathat_gt_cross") (("1" (case-replace "x!1 = 0") (("1" (expand "^") (("1" (inst + "100") (("1" (skosimp*) (("1" (expand "expt") (("1" (assert) (("1" (rewrite "abs_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) (("2" (inst - "epsilon!1" "abs(x!1)" "k!1") (("2" (assert) (("2" (inst + "k!1") (("2" (skosimp*) (("2" (lemma "hathat_nat") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "abs_expt" :dir rl) (("2" (case "abs(x!1) ^ i!1 <= abs(x!1) ^ k!1") (("1" (assert) nil nil) ("2" (hide 4) (("2" (hide-all-but (-4 -5 1)) (("2" (lemma "both_sides_expt_lt1_le") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergence") (("2" (inst - "1-abs(x!1)") (("1" (skosimp*) (("1" (inst + "n!1+1") (("1" (inst - "n!1") (("1" (assert) (("1" (grind :exclude "^^") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergence const-decl "bool" convergence_sequences "analysis/") (conv_x_to_1_div_n formula-decl nil convergence_special nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (^^ const-decl "nnreal" expt nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types 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) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (hathat_gt_cross formula-decl nil expt nil) (abs_eq_0 formula-decl nil abs_lems "reals/") (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_expt_lt1_le formula-decl nil exponentiation nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (abs_expt formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (hathat_nat formula-decl nil expt nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (^ const-decl "real" exponentiation nil) (nat_expt application-judgement "nat" exponentiation nil) (abs_0 formula-decl nil abs_lems "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (x!1 skolem-const-decl "real" convergence_special nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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)) nil) (conv_x_to_n-1 nil 3301930198 ("" (skosimp*) (("" (expand "convergence") (("" (skosimp*) (("" (lemma "conv_x_to_1_div_n") (("" (inst -1 "epsilon!1") (("" (case "(EXISTS (k: posnat): abs(x!1) < epsilon!1^^(1/k))") (("1" (skosimp*) (("1" (lemma "hathat_lem1") (("1" (inst - "epsilon!1" "abs(x!1)" "k!1") (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergence") (("2" (inst - "1-abs(x!1)") (("1" (skosimp*) (("1" (inst + "n!1+1") (("1" (inst - "n!1") (("1" (assert) (("1" (grind :exclude "^^") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (expt_abs_gt_TCC1 0 (expt_abs_gt_TCC1-1 nil 3302013574 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (expt_abs_gt_TCC2 0 (expt_abs_gt_TCC2-1 nil 3302013574 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (expt_abs_gt 0 (expt_abs_gt-1 nil 3302013658 ("" (induct "n") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (expand "^") (("2" (expand "expt" 1) (("2" (inst?) (("2" (assert) (("2" (expand "abs" 1 1) (("2" (lift-if) (("2" (ground) (("1" (rewrite "expt_of_abs") (("1" (name-replace "EE" "expt(x!1, j!1)") (("1" (grind) (("1" (case-replace "-x!1 >= x!1") (("1" (mult-ineq -1 -3) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_expt application-judgement "nnreal" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt_of_abs formula-decl nil exponentiation nil) (ge_times_ge_any1 formula-decl nil extra_real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers 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 "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (conv_x_to_n_div_fact 0 (conv_x_to_n_div_fact-5 nil 3413217310 ("" (stop-rewrite "abs_nat") (("" (skosimp*) (("" (case "EXISTS (k: nat): k > abs(x!1)") (("1" (skosimp*) (("1" (case "convergence(LAMBDA n: abs(x!1) ^ n / factorial(n), 0)") (("1" (lemma "abs_convergence") (("1" (inst - "(LAMBDA n: x!1 ^ n / factorial(n))") (("1" (assert) (("1" (expand "abs" 1) (("1" (case-replace "(LAMBDA (x: nat): abs(x!1 ^ x / factorial(x))) = (LAMBDA n: abs(x!1) ^ n / factorial(n))") (("1" (hide -1 2 3) (("1" (apply-extensionality 1 :hide? t) (("1" (real-props) (("1" (expand "abs" 1 3) (("1" (lemma "abs_expt") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (grind) nil nil) ("2" (assert) (("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (real-props) (("2" (hide -1) (("2" (rewrite "expt_abs_gt") (("2" (assert) (("2" (rewrite "abs_expt") (("1" (assert) nil nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "convergence(LAMBDA n: (abs(x!1)/k!1) ^ n, 0)") (("1" (lemma "squeezing_abs_0_gen") (("1" (inst - "(LAMBDA n: abs(x!1) ^ n / factorial(n))" "(LAMBDA n: (abs(x!1) / k!1) ^ n * k!1^k!1/factorial(k!1))") (("1" (assert) (("1" (lemma "cnv_seq_scal") (("1" (inst - "k!1 ^ k!1 / factorial(k!1)" "0" "(LAMBDA n: (abs(x!1) / k!1) ^ n)") (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (inst + "k!1") (("1" (skosimp*) (("1" (hide -1 2) (("1" (rewrite "abs_div") (("1" (expand "abs" 1 1) (("1" (expand "abs" 1 2) (("1" (lemma "factorial_ge") (("1" (inst - "k!1" "n!1") (("1" (assert) (("1" (cross-mult 1) (("1" (case-replace "x!1 = 0") (("1" (rewrite "abs_0") (("1" (expand "^") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (mult-by -1 "(abs(x!1) / k!1) ^ n!1 * k!1 ^ k!1") (("1" (case-replace "k!1 ^ (n!1 - k!1) * factorial(k!1) * ((abs(x!1) / k!1) ^ n!1 * k!1 ^ k!1) = abs(x!1) ^ n!1 * factorial(k!1) ") (("1" (assert) nil nil) ("2" (hide -1 -3 3) (("2" (rewrite "div_expt") (("2" (rewrite "expt_div" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "expt_pos") (("2" (inst?) (("1" (assert) (("1" (mult-by -1 "k!1 ^ k!1") (("1" (assert) nil nil)) nil)) nil) ("2" (prop) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) 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" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "conv_x_to_n") (("2" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "abs" 1 1) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (cross-mult -1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "floor(abs(x!1)+1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (conv_x_to_n formula-decl nil convergence_special nil) (squeezing_abs_0_gen formula-decl nil convergence_ops "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (factorial_ge formula-decl nil factorial "ints/") (nnrat_exp application-judgement "nnrat" exponentiation nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (rat_expt application-judgement "rat" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (expt_pos formula-decl nil exponentiation nil) (div_expt formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_div formula-decl nil exponentiation nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (n!1 skolem-const-decl "nat" convergence_special nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (div_mult_pos_le1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (cnv_seq_scal formula-decl nil convergence_ops "analysis/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (k!1 skolem-const-decl "nat" convergence_special nil) (abs_convergence formula-decl nil convergence_ops "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (= const-decl "[T, T -> boolean]" equalities nil) (x!1 skolem-const-decl "real" convergence_special nil) (nzreal nonempty-type-eq-decl nil reals nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (abs_0 formula-decl nil abs_lems "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat_expt application-judgement "nat" exponentiation nil) (nat_exp application-judgement "nat" exponentiation nil) (abs_expt formula-decl nil exponentiation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (abs_div formula-decl nil real_props nil) (cross_mult formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (both_sides_div_pos_ge1 formula-decl nil real_props 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) (minus_real_is_real application-judgement "real" reals nil) (expt_abs_gt formula-decl nil convergence_special nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (minus_rat_is_rat application-judgement "rat" rationals nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (sequence type-eq-decl nil sequences nil) (convergence const-decl "bool" convergence_sequences "analysis/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/") (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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) nil) (conv_x_to_n_div_fact-4 nil 3352453165 ("" (skosimp*) (("" (case "EXISTS (k: nat): k > abs(x!1)") (("1" (skosimp*) (("1" (case "convergence(LAMBDA n: abs(x!1) ^ n / factorial(n), 0)") (("1" (lemma "abs_convergence") (("1" (inst - "(LAMBDA n: x!1 ^ n / factorial(n))") (("1" (assert) (("1" (expand "abs" 1) (("1" (case-replace "(LAMBDA (x: nat): abs(x!1 ^ x / factorial(x))) = (LAMBDA n: abs(x!1) ^ n / factorial(n))") (("1" (hide -1 2 3) (("1" (apply-extensionality 1 :hide? t) (("1" (real-props) (("1" (expand "abs" 1 3) (("1" (lemma "abs_expt") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (grind) nil nil) ("2" (assert) (("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (real-props) (("2" (hide -1) (("2" (rewrite "expt_abs_gt") (("2" (assert) (("2" (rewrite "abs_expt") (("1" (assert) nil nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "convergence(LAMBDA n: (abs(x!1)/k!1) ^ n, 0)") (("1" (lemma "squeezing_abs_0_gen") (("1" (inst - "(LAMBDA n: abs(x!1) ^ n / factorial(n))" "(LAMBDA n: (abs(x!1) / k!1) ^ n * k!1^k!1/factorial(k!1))") (("1" (assert) (("1" (lemma "cnv_seq_scal") (("1" (inst - "k!1 ^ k!1 / factorial(k!1)" "0" "(LAMBDA n: (abs(x!1) / k!1) ^ n)") (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (inst + "k!1") (("1" (skosimp*) (("1" (hide -1 2) (("1" (rewrite "abs_div") (("1" (expand "abs" 1 1) (("1" (expand "abs" 1 2) (("1" (lemma "factorial_ge") (("1" (inst - "k!1" "n!1") (("1" (assert) (("1" (cross-mult 1) (("1" (case-replace "x!1 = 0") (("1" (rewrite "abs_0") (("1" (expand "^") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (mult-by -1 "(abs(x!1) / k!1) ^ n!1 * k!1 ^ k!1") (("1" (case-replace "k!1 ^ (n!1 - k!1) * factorial(k!1) * ((abs(x!1) / k!1) ^ n!1 * k!1 ^ k!1) = abs(x!1) ^ n!1 * factorial(k!1) ") (("1" (assert) nil nil) ("2" (hide -1 -3 3) (("2" (rewrite "div_expt") (("2" (rewrite "expt_div" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "expt_pos") (("2" (inst?) (("1" (assert) (("1" (mult-by -1 "k!1 ^ k!1") (("1" (assert) nil nil)) nil)) nil) ("2" (prop) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) 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" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "conv_x_to_n") (("2" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "abs" 1 1) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (cross-mult -1) (("1" (assert) nil nil)) nil) ("2" (cross-mult 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "floor(abs(x!1)+1)") (("2" (assert) nil nil)) nil)) nil)) nil) ((squeezing_abs_0_gen formula-decl nil convergence_ops "analysis/") (cnv_seq_scal formula-decl nil convergence_ops "analysis/") (abs_convergence formula-decl nil convergence_ops "analysis/") (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (convergence const-decl "bool" convergence_sequences "analysis/")) nil) (conv_x_to_n_div_fact-3 nil 3302012408 ("" (skosimp*) (("" (case "EXISTS (k: nat): k > abs(x!1)") (("1" (skosimp*) (("1" (case "convergence(LAMBDA n: abs(x!1) ^ n / factorial(n), 0)") (("1" (lemma "abs_convergence") (("1" (inst - "(LAMBDA n: x!1 ^ n / factorial(n))") (("1" (assert) (("1" (expand "abs" 1) (("1" (case-replace "(LAMBDA (x: nat): abs(x!1 ^ x / factorial(x))) = (LAMBDA n: abs(x!1) ^ n / factorial(n))") (("1" (hide -1 2 3) (("1" (apply-extensionality 1 :hide? t) (("1" (real-props) (("1" (expand "abs" 1 3) (("1" (lemma "abs_expt") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (grind) nil nil) ("2" (assert) (("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (real-props) (("2" (hide -1) (("2" (rewrite "expt_abs_gt") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "convergence(LAMBDA n: (abs(x!1)/k!1) ^ n, 0)") (("1" (lemma "squeezing_abs_0_gen") (("1" (inst - "(LAMBDA n: abs(x!1) ^ n / factorial(n))" "(LAMBDA n: (abs(x!1) / k!1) ^ n * k!1^k!1/factorial(k!1))") (("1" (assert) (("1" (lemma "cnv_seq_scal") (("1" (inst - "k!1 ^ k!1 / factorial(k!1)" "0" "(LAMBDA n: (abs(x!1) / k!1) ^ n)") (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (inst + "k!1") (("1" (skosimp*) (("1" (hide -1 2) (("1" (rewrite "abs_div") (("1" (expand "abs" 1 1) (("1" (expand "abs" 1 2) (("1" (lemma "factorial_ge") (("1" (inst - "k!1" "n!1") (("1" (assert) (("1" (cross-mult 1) (("1" (case-replace "x!1 = 0") (("1" (rewrite "abs_0") (("1" (expand "^") (("1" (expand --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.128Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
