|
(power_series
(hat_02n 0
(hat_02n-1 nil 3352090131
("" (induct "pn" 1)
(("1" (grind) nil nil) ("2" (assert) nil nil)
("3" (skosimp*)
(("3" (expand "^")
(("3" (expand "expt" 1) (("3" (assert) nil nil)) nil)) nil))
nil))
nil)
((expt def-decl "real" exponentiation nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(nat_expt application-judgement "nat" exponentiation nil)
(expt_x0 formula-decl nil exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(> const-decl "bool" reals nil)
(IMPLIES 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))
(powerseq_TCC1 0
(powerseq_TCC1-1 nil 3249311616 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(powerseries_bounded 0
(powerseries_bounded-1 nil 3297508094
("" (skosimp*)
(("" (expand "powerseries")
(("" (lemma "conv_series_terms_to_0")
(("" (inst?)
(("" (assert)
(("" (hide -2)
(("" (lemma "convergence_cauchy")
(("" (inst - "powerseq(a!1, x!1)")
(("" (flatten)
(("" (hide -2)
(("" (split -1)
(("1" (hide -2)
(("1" (lemma "cauchy_bounded")
(("1" (inst?)
(("1"
(assert)
(("1"
(expand "bounded?")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "convergent?")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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)
(powerseq const-decl "sequence[real]" power_series nil)
(convergent? const-decl "bool" convergence_sequences "analysis/")
(bounded? const-decl "bool" real_fun_preds "reals/")
(cauchy_bounded formula-decl nil convergence_sequences "analysis/")
(convergence_cauchy formula-decl nil convergence_sequences
"analysis/")
(conv_series_terms_to_0 formula-decl nil series nil))
shostak))
(powerseries_conv_point 0
(powerseries_conv_point-1 nil 3249311616
("" (skosimp*)
(("" (lemma "conv_series_terms_to_0")
(("" (expand "powerseries")
(("" (inst?)
(("" (assert)
(("" (hide -2)
(("" (expand "convergence")
(("" (expand "absolutely_convergent_series?")
(("" (inst -1 "1")
(("" (skosimp*)
(("" (lemma "comparison_test_gen")
(("" (inst?)
(("" (assert)
(("" (inst -1 "geometric(abs(x!1/x1!1))")
((""
(assert)
((""
(hide 2)
((""
(split +)
(("1"
(lemma "geometric_series")
(("1"
(expand "convergent?")
(("1"
(inst?)
(("1"
(assert)
(("1"
(split -1)
(("1"
(hide -2)
(("1" (inst?) nil nil))
nil)
("2"
(hide -1 2)
(("2"
(rewrite "abs_abs")
(("2"
(rewrite "abs_div")
(("2"
(lemma
"div_mult_pos_lt1")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(inst 1 "n!1")
(("2"
(skosimp*)
(("2"
(expand "powerseq")
(("2"
(expand "abs" 1 2)
(("2"
(rewrite "abs_abs")
(("2"
(expand "geometric")
(("2"
(inst?)
(("2"
(assert)
(("2"
(case-replace
"abs(a!1(n!2) * x!1 ^ n!2) = abs(a!1(n!2) * x1!1 ^ n!2) * abs(x!1/x1!1)^n!2")
(("1"
(hide -1)
(("1"
(mult-by
-2
"abs(x!1 / x1!1) ^ n!2")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(case-replace
"abs(x!1 / x1!1) ^ n!2 = abs((x!1 / x1!1) ^ n!2)")
(("1"
(rewrite
"abs_mult"
:dir
rl)
(("1"
(assert)
(("1"
(hide
-1
2)
(("1"
(expand
"^")
(("1"
(rewrite
"expt_of_div")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(hide
-2
-3)
(("2"
(name-replace
"BBB"
"(x!1 / x1!1)")
(("2"
(rewrite
"abs_hat_nat")
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))
nil))
nil))
nil)
((conv_series_terms_to_0 formula-decl nil 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)
(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)
(powerseq const-decl "sequence[real]" power_series nil)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(absolutely_convergent_series? const-decl "boolean" power_series
nil)
(abs const-decl "sequence[real]" series 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)
(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)
(geometric const-decl "sequence[real]" series nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_hat_nat formula-decl nil exponentiation nil)
(abs_mult formula-decl nil real_props nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_of_div formula-decl nil exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(x!1 skolem-const-decl "real" power_series nil)
(x1!1 skolem-const-decl "nonzero_real" power_series nil)
(n!2 skolem-const-decl "nat" power_series nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(geometric_series formula-decl nil series nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(abs_abs formula-decl nil real_props nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(abs_div formula-decl nil real_props nil)
(convergent? const-decl "bool" convergence_sequences "analysis/")
(comparison_test_gen formula-decl nil series nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(convergence const-decl "bool" convergence_sequences "analysis/")
(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)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(powerseries const-decl "sequence[real]" power_series nil))
nil))
(powerseries_conv 0
(powerseries_conv-1 nil 3249311616
("" (skosimp*)
(("" (lemma "powerseries_conv_point")
(("" (inst?)
(("1" (expand "powerseries")
(("1" (inst -1 "y!1")
(("1" (assert)
(("1" (expand "absolutely_convergent_series?")
(("1" (lemma "convergent_abs")
(("1" (inst -1 "powerseq(a!1,y!1)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((powerseries_conv_point formula-decl nil power_series nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(powerseries const-decl "sequence[real]" power_series nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(convergent_abs formula-decl nil series nil)
(powerseq const-decl "sequence[real]" power_series nil)
(absolutely_convergent_series? const-decl "boolean" power_series
nil)
(nonzero_real nonempty-type-eq-decl nil reals 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)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal 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)
(x!1 skolem-const-decl "real" power_series nil))
nil))
(powerseries_diverg 0
(powerseries_diverg-1 nil 3249311616
("" (skosimp*)
(("" (expand "divergent_series?")
(("" (lemma "powerseries_conv_point")
(("" (inst?)
(("" (inst?)
(("1" (assert)
(("1" (expand "powerseries")
(("1" (expand "absolutely_convergent_series?")
(("1" (hide -3)
(("1" (lemma "convergent_abs")
(("1" (inst -1 "powerseq(a!1, x1!1)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide -2 2)
(("2" (typepred "x1!1") (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((divergent_series? const-decl "boolean" 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)
(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)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(abs_nat formula-decl nil abs_lems "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_ge_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)
(absolutely_convergent_series? const-decl "boolean" power_series
nil)
(convergent_abs formula-decl nil series nil)
(powerseq const-decl "sequence[real]" power_series nil)
(powerseries const-decl "sequence[real]" power_series nil)
(x!1 skolem-const-decl "real" power_series nil)
(powerseries_conv_point formula-decl nil power_series nil))
nil))
(zero_powerseries_conv 0
(zero_powerseries_conv-1 nil 3249311616
("" (skosimp*)
(("" (expand "powerseries")
(("" (expand "powerseq")
(("" (lemma "tail_series_conv2")
(("" (inst?)
(("" (inst -1 "1")
(("" (assert)
(("" (hide 2)
(("" (lemma "zero_series_conv")
((""
(case-replace
"(LAMBDA n: 0) = (LAMBDA n: a!1(1 + n) * 0 ^ (1 + n))")
(("" (hide -1 2)
(("" (apply-extensionality 1 :hide? t)
(("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((powerseries const-decl "sequence[real]" power_series nil)
(tail_series_conv2 formula-decl nil series nil)
(zero_series_conv formula-decl nil series nil)
(hat_02n formula-decl nil power_series nil)
(nat_exp application-judgement "nat" exponentiation nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(numfield nonempty-type-eq-decl nil number_fields 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)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(powerseq const-decl "sequence[real]" power_series nil))
nil))
(powerseries_three_cases 0
(powerseries_three_cases-1 nil 3249311616
("" (skosimp*)
(("" (expand "series_convergent_only_at_0")
(("" (expand "series_convergent_within")
(("" (expand "divergent_series?")
(("" (split 2)
(("1" (hide 2 3)
(("1" (lemma "zero_powerseries_conv")
(("1" (inst?)
(("1" (expand "powerseries") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (case "abs(x!1) < abs(x!2)")
(("1" (lemma "powerseries_conv")
(("1" (inst -1 "a!1" "x!2" "x!1")
(("1" (expand "powerseries")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (lemma "real_complete")
(("2"
(inst -1
"{x: real | convergent?(series(powerseq(a!1, x)))}")
(("1" (split -1)
(("1" (skosimp*)
(("1" (name-replace "LUB" "y!1")
(("1" (lemma "real_lower_complete")
(("1"
(inst -1
"{x: real | convergent?(series(powerseq(a!1, x)))}")
(("1"
(split -1)
(("1"
(skosimp*)
(("1"
(name-replace "GLB" "x!3")
(("1"
(case "LUB >= 0")
(("1"
(case "GLB <= 0")
(("1"
(case "abs(GLB) = abs(LUB)")
(("1"
(inst 4 "abs(LUB)")
(("1"
(split 4)
(("1"
(skosimp*)
(("1"
(case "x!4 >= 0")
(("1"
(expand
"least_upper_bound?")
(("1"
(flatten)
(("1"
(inst -8 "x!4")
(("1"
(split -8)
(("1"
(hide
-4
-7
-8
-9
1
4)
(("1"
(grind)
nil
nil))
nil)
("2"
(expand
"upper_bound?")
(("2"
(skosimp*)
(("2"
(typepred
"s!1")
(("2"
(lemma
"powerseries_conv")
(("2"
(inst
-1
"a!1"
"s!1"
"x!4")
(("2"
(assert)
(("2"
(expand
"powerseries")
(("2"
(hide
-1
-4
-7
-8
-9
3
6)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"greatest_lower_bound?")
(("2"
(flatten)
(("2"
(inst -6 "x!4")
(("2"
(split -6)
(("1"
(hide
-6
-7
-8
2
5)
(("1"
(grind)
nil
nil))
nil)
("2"
(expand
"lower_bound?")
(("2"
(skosimp*)
(("2"
(typepred
"s!1")
(("2"
(lemma
"powerseries_conv")
(("2"
(inst
-1
"a!1"
"s!1"
"x!4")
(("2"
(assert)
(("2"
(expand
"powerseries")
(("2"
(hide
-1
-6
-7
-8
4
7)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"series_divergent_outside")
(("2"
(expand "abs" 1 1)
(("2"
(skosimp*)
(("2"
(lift-if)
(("2"
(split -1)
(("1"
(flatten)
(("1"
(expand
"greatest_lower_bound?")
(("1"
(flatten)
(("1"
(expand
"lower_bound?")
(("1"
(inst
-6
"x!4")
(("1"
(hide
-7
-8
-9
1
4)
(("1"
(grind)
nil
nil))
nil)
("2"
(expand
"divergent_series?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(expand
"divergent_series?")
(("2"
(expand
"least_upper_bound?")
(("2"
(flatten)
(("2"
(hide
-6
-8)
(("2"
(expand
"upper_bound?")
(("2"
(inst
-6
"x!4")
(("2"
(hide
-2
-7
3)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "abs" 1)
(("2"
(assert)
(("2"
(case-replace
"LUB = 0")
(("1"
(expand
"least_upper_bound?")
(("1"
(flatten)
(("1"
(expand
"upper_bound?")
(("1"
(inst
-6
"x!2")
(("1"
(assert)
(("1"
(expand
"greatest_lower_bound?")
(("1"
(flatten)
(("1"
(expand
"lower_bound?")
(("1"
(inst
-5
"x!2")
(("1"
(expand
"abs"
-2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide 5)
(("2"
(case
"abs(GLB) > abs(LUB)")
(("1"
(name
"WW"
"abs(LUB) + (abs(GLB) - abs(LUB))/2")
(("1"
(case
"convergent?(powerseries(a!1)(WW))")
(("1"
(expand
"least_upper_bound?")
(("1"
(flatten)
(("1"
(expand
"upper_bound?")
(("1"
(inst
-7
"WW")
(("1"
(hide
-1
-6
-8
-9
4)
(("1"
(grind)
nil
nil))
nil)
("2"
(expand
"powerseries")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"greatest_lower_bound?")
(("2"
(flatten)
(("2"
(expand
"lower_bound?")
(("2"
(inst
-6
"-WW")
(("2"
(split -6)
(("1"
(hide
-6
-7
-8
1
5)
(("1"
(grind)
nil
nil))
nil)
("2"
(skosimp*)
(("2"
(typepred
"s!1")
(("2"
(lemma
"powerseries_conv")
(("2"
(inst
-1
"a!1"
"s!1"
"WW")
(("2"
(expand
"powerseries")
(("2"
(assert)
(("2"
(hide
-1
-6
-7
-8
3
7)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name
"WW"
"abs(GLB) + (abs(LUB) - abs(GLB))/2")
(("2"
(case
"convergent?(powerseries(a!1)(-WW))")
(("1"
(expand
"greatest_lower_bound?")
(("1"
(flatten)
(("1"
(hide -6)
(("1"
(expand
"lower_bound?")
(("1"
(expand
"powerseries")
(("1"
(inst
-5
"-WW")
(("1"
(hide
-1
-6
-7
5)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"least_upper_bound?")
(("2"
(flatten)
(("2"
(inst -6 "WW")
(("2"
(split -6)
(("1"
(hide
-5
-6
-7
1
6)
(("1"
(grind)
nil
nil))
nil)
("2"
(expand
"upper_bound?")
(("2"
(skosimp*)
(("2"
(typepred
"s!1")
(("2"
(lemma
"powerseries_conv")
(("2"
(inst
-1
"a!1"
"s!1"
"-WW")
(("2"
(assert)
(("2"
(expand
"powerseries")
(("2"
(hide
-1
-5
-6
-7
3
8)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -4 4 5)
(("2"
(lemma
"zero_powerseries_conv")
(("2"
(inst?)
(("2"
(expand
"greatest_lower_bound?")
(("2"
(flatten)
(("2"
(expand
"lower_bound?")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.44 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
