|
(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.43 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.
|
