| products/sources/formale sprachen/PVS/series/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: power_series_conv.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(power_series_conv
(Inf_sum_TCC1 0 (Inf_sum_TCC1-1 nil 3298729967 ("" (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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (conv_powerseries? const-decl "bool" power_series_conv nil) (T_pred const-decl "[real -> boolean]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (powerseries const-decl "sequence[real]" power_series nil) (series const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (Inf_sum_TCC2 0 (Inf_sum_TCC2-1 nil 3298729967 ("" (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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (conv_powerseries? const-decl "bool" power_series_conv nil) (T_pred const-decl "[real -> boolean]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (powerseries const-decl "sequence[real]" power_series nil) (series const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (end_powerseries_conv 0 (end_powerseries_conv-1 nil 3298368454 ("" (skosimp*) (("" (lemma "end_series_conv") (("" (expand "conv_powerseries?") (("" (expand "powerseries") (("" (split +) (("1" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((end_series_conv formula-decl nil series nil) (powerseries const-decl "sequence[real]" power_series nil) (powerseries const-decl "sequence[real]" power_series 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]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (powerseq const-decl "sequence[real]" power_series nil) (sequence type-eq-decl nil sequences 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) (conv_powerseries? const-decl "bool" power_series_conv nil) (conv_powerseries? const-decl "bool" power_series_conv nil)) shostak)) (Inf_inf_TCC1 0 (Inf_inf_TCC1-1 nil 3298731432 ("" (skosimp*) (("" (expand "conv_series?") (("" (expand "conv_powerseries?") (("" (inst?) (("" (expand "powerseries") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((conv_series? const-decl "bool" series 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]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (powerseries const-decl "sequence[real]" power_series nil) (conv_powerseries? const-decl "bool" power_series_conv nil)) shostak)) (Inf_inf 0 (Inf_inf-1 nil 3298730864 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (expand "Inf_sum") (("1" (expand "powerseries") (("1" (expand "inf_sum") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "conv_powerseries?") (("2" (expand "conv_series?") (("2" (expand "powerseries") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) 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]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (inf_sum const-decl "real" series nil) (Inf_sum const-decl "real" power_series_conv nil) (conv_powerseries? const-decl "bool" power_series_conv 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) (conv_series? const-decl "bool" series nil) (powerseq const-decl "sequence[real]" power_series nil) (a!1 skolem-const-decl "sequence[real]" power_series_conv nil) (powerseries const-decl "sequence[real]" power_series nil)) shostak)) (Inf_inf_m_TCC1 0 (Inf_inf_m_TCC1-1 nil 3298731432 ("" (skosimp*) (("" (expand "conv_series?") (("" (expand "conv_powerseries?") (("" (expand "powerseries") (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((conv_series? const-decl "bool" series nil) (powerseries const-decl "sequence[real]" power_series 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]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (conv_powerseries? const-decl "bool" power_series_conv nil)) shostak)) (Inf_inf_m 0 (Inf_inf_m-1 nil 3298731378 ("" (skosimp*) (("" (expand "Inf_sum") (("" (apply-extensionality 1 :hide? t) (("1" (expand "inf_sum") (("1" (expand "powerseries") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "conv_powerseries?") (("2" (expand "powerseries") (("2" (expand "conv_series?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "conv_powerseries?") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((Inf_sum const-decl "real" power_series_conv nil) (conv_powerseries? const-decl "bool" power_series_conv nil) (m!1 skolem-const-decl "nat" power_series_conv nil) (a!1 skolem-const-decl "sequence[real]" power_series_conv nil) (powerseries const-decl "sequence[real]" power_series nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (sequence type-eq-decl nil sequences 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) (powerseq const-decl "sequence[real]" power_series nil) (conv_series? const-decl "bool" series nil) (limit const-decl "real" convergence_sequences "analysis/") (inf_sum const-decl "real" series nil) (T formal-subtype-decl nil power_series_conv nil) (T_pred const-decl "[real -> boolean]" power_series_conv 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)) (powerseries_abs_conv 0 (powerseries_abs_conv-1 nil 3297171631 ("" (skosimp*) (("" (case-replace "EXISTS (y:T): abs(y) > abs(x!1)") (("1" (skosimp*) (("1" (lemma "powerseries_conv_point") (("1" (expand "absolutely_convergent_series?") (("1" (inst?) (("1" (assert) (("1" (inst -1 "y!1") (("1" (assert) (("1" (inst -2 "y!1") nil nil)) nil) ("2" (assert) (("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (case "x!1 >= 0") (("1" (lemma "open") (("1" (inst -1 "x!1") (("1" (skosimp*) (("1" (inst + "x!1 + delta!1/2") (("1" (hide -1) (("1" (grind) nil nil)) nil) ("2" (inst?) (("2" (assert) (("2" (hide 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "open") (("2" (inst -1 "x!1") (("2" (skosimp*) (("2" (inst + "x!1 - delta!1/2") (("1" (hide -1) (("1" (grind) nil nil)) nil) ("2" (inst?) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals 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) (powerseries_conv_point formula-decl nil power_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-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) (/= const-decl "boolean" notequal nil) (y!1 skolem-const-decl "T" power_series_conv nil) (nonzero_real nonempty-type-eq-decl nil reals 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) (absolutely_convergent_series? const-decl "boolean" power_series nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "T" power_series_conv nil) (delta!1 skolem-const-decl "posreal" power_series_conv nil) (posreal 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 "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (open formula-decl nil power_series_conv nil) (delta!1 skolem-const-decl "posreal" power_series_conv nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (simple_TCC1 0 (simple_TCC1-1 nil 3297159301 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (simple_0_conv 0 (simple_0_conv-1 nil 3297159301 ("" (expand "simple") (("" (flatten) (("" (lemma "tail_series_conv2") (("" (inst -1 "1" "_") (("" (inst?) (("" (assert) (("" (hide 2) (("" (expand "series") (("" (expand "^") (("" (expand "expt") (("" (assert) (("" (expand "convergent?") (("" (inst 1 "0") (("" (expand "convergence") (("" (skosimp*) (("" (inst 1 "100") (("" (skosimp*) (("" (assert) (("" (case-replace "(LAMBDA (n_1962: nat): 0 * expt(0, n_1962) / factorial(1 + n_1962)) = (LAMBDA n: 0)") (("1" (rewrite "sigma_const") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (zero_hat formula-decl nil exponent_props "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (series const-decl "sequence[real]" series nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (convergence const-decl "bool" convergence_sequences "analysis/") (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (sigma_const formula-decl nil sigma "reals/") (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nat_expt application-judgement "nat" exponentiation nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sequence type-eq-decl nil sequences nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (tail_series_conv2 formula-decl nil series nil) (simple const-decl "sequence[real]" power_series_conv nil) (nat_exp application-judgement "nat" exponentiation nil)) nil)) (simple_conv 0 (simple_conv-1 nil 3297159301 ("" (skosimp*) (("" (case-replace "x!1 = 0") (("1" (rewrite "simple_0_conv") nil nil) ("2" (lemma "ratio_test_gen") (("2" (inst?) (("2" (assert) (("2" (hide 3) (("2" (split +) (("1" (skosimp*) (("1" (expand "simple") (("1" (rewrite "div_eq_zero") (("1" (assert) (("1" (expand "^") (("1" (lemma "expt_nonzero_aux") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "1/2") (("2" (assert) (("2" (inst + "floor(abs(2*x!1))") (("2" (skosimp*) (("2" (case-replace "simple(x!1)(1 + n!1) / simple(x!1)(n!1) = x!1/(1+n!1)") (("1" (hide -1) (("1" (typepred "floor(abs(2 * x!1))") (("1" (hide -1) (("1" (case "n!1 > abs(2 * x!1) - 1") (("1" (hide -2 -3 -4) (("1" (rewrite "abs_div") (("1" (expand "abs" 1 2) (("1" (lemma "both_sides_div_pos_le1") (("1" (inst -1 "1+n!1" "abs(x!1)" "1/2*(1+n!1)") (("1" (flatten) (("1" (hide -1) (("1" (case-replace "1 / 2 * (1 + n!1) / (1 + n!1) = 1/2") (("1" (split -2) (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (lemma "both_sides_times_pos_le1") (("2" (inst -1 "2" "abs(x!1)" "1 / 2 * (1 + n!1)") (("2" (flatten) (("2" (hide -2) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (case-replace "1 / 2 * (1 + n!1) * 2 = 1+n!1") (("1" (hide -1) (("1" (rewrite "abs_mult") (("1" (expand "abs" -1 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 2) (("2" (name-replace "NN" "(1 + n!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "simple") (("2" (case "(forall (a: real),(b,c,d: nzreal): (a/b)/(c/d) = (a/c)/(b/d))") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "(x!1 ^ (1 + n!1)) / x!1 ^ n!1 = x!1") (("1" (case-replace "(factorial(1 + n!1) / factorial(n!1)) = 1 + n!1") (("1" (hide 2) (("1" (expand "factorial" 1 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "^") (("2" (expand "expt" 1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "^") (("2" (lemma "expt_nonzero_aux") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (simple_0_conv formula-decl nil power_series_conv nil) (real_div_nzreal_is_real application-judgement "real" 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) (simple const-decl "sequence[real]" power_series_conv nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals 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) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_times_real_is_real application-judgement "real" reals 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) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs_div formula-decl nil real_props nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (both_sides_div_pos_le1 formula-decl nil 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) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_mult formula-decl nil real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (posint nonempty-type-eq-decl nil integers nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!1 skolem-const-decl "T" power_series_conv nil) (n!1 skolem-const-decl "nat" power_series_conv nil) (expt def-decl "real" exponentiation nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_eq_zero formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/") (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_nonzero_aux formula-decl nil exponentiation nil) (ratio_test_gen formula-decl nil series nil)) nil)) (m1_conv 0 (m1_conv-1 nil 3321109289 ("" (skosimp*) (("" (expand "powerseries") (("" (expand "powerseq") (("" (lemma "geometric_conv") (("" (expand "geometric") (("" (inst - "-x!1") (("" (rewrite "abs_neg") (("" (assert) (("" (case-replace "(LAMBDA (k: nat): (-1) ^ k * x!1 ^ k) = (LAMBDA n: (-x!1) ^ n)") (("" (hide -1 2) (("" (apply-extensionality 1 :hide? t) (("" (lemma "mult_expt") (("" (inst?) (("1" (assert) nil nil) ("2" (flatten) (("2" (replace -1) (("2" (typepred "x!2") (("2" (case-replace "x!2 = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((powerseries const-decl "sequence[real]" power_series nil) (geometric_conv formula-decl nil series nil) (minus_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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (T_pred const-decl "[real -> boolean]" power_series_conv nil) (T formal-subtype-decl nil power_series_conv nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_expt formula-decl nil exponentiation nil) (NOT const-decl "[bool -> bool]" booleans nil) (zero_hat formula-decl nil exponent_props "reals/") (expt_x0 formula-decl nil exponentiation nil) (minus_even_is_even application-judgement "even_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat_exp application-judgement "nat" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (x!1 skolem-const-decl "T" power_series_conv nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (abs_neg formula-decl nil abs_lems "reals/") (geometric const-decl "sequence[real]" series nil) (powerseq const-decl "sequence[real]" power_series nil)) nil))) ¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
