|
(trig_props
(IMP_power_series_deriv_TCC1 0
(IMP_power_series_deriv_TCC1-1 nil 3299592135
("" (expand "connected?") (("" (propax) nil nil)) nil)
((connected? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(IMP_power_series_deriv_TCC2 0
(IMP_power_series_deriv_TCC2-1 nil 3299592135
("" (expand "not_one_element?")
(("" (skosimp*)
(("" (assert) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((real_plus_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 -> numfield]" number_fields nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(IMP_power_series_deriv_TCC3 0
(IMP_power_series_deriv_TCC3-1 nil 3299592135
("" (skosimp*) (("" (inst + "1") (("" (skosimp*) 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals 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))
shostak))
(IMP_power_series_deriv_TCC4 0
(IMP_power_series_deriv_TCC4-1 nil 3299592135 ("" (skosimp*) nil nil)
nil shostak))
(sin_derivable_TCC1 0
(sin_derivable_TCC1-1 nil 3471704739
("" (expand "deriv_domain?")
(("" (skosimp*) (("" (inst + e!1/2) (("" (grind) nil nil)) nil))
nil))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(/ 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)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(sin_derivable 0
(sin_derivable-1 nil 3249311628
("" (lemma "sin_conv")
(("" (lemma "powerseries_derivable[real]")
(("" (expand "sin")
(("" (expand "inf_sum")
(("" (inst?)
(("" (assert)
(("" (expand "powerseries") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
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)
(powerseries_derivable formula-decl nil power_series_deriv nil)
(inf_sum const-decl "real" series nil)
(powerseries const-decl "sequence[real]" power_series nil)
(sin_coef const-decl "real" trig_fun 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)
(sin const-decl "real" trig_fun nil)
(sin_conv formula-decl nil trig_fun nil))
nil))
(deriv_sin_TCC1 0
(deriv_sin_TCC1-1 nil 3249311628
("" (lemma "sin_derivable") (("" (propax) nil nil)) nil)
((sin_derivable formula-decl nil trig_props nil)) nil))
(deriv_sin 0
(deriv_sin-2 nil 3352090315
("" (skosimp*)
(("" (lemma "deriv_Inf_sum[real]")
(("" (inst -1 "sin_coef")
(("" (rewrite "sin_conv")
(("" (expand "sin")
(("" (assert)
(("" (expand "Inf_sum")
(("" (expand "inf_sum")
(("" (expand "powerseries")
(("" (replace -1)
(("" (hide -1)
(("" (expand "cos")
(("" (expand "inf_sum")
((""
(case-replace
"series(powerseq(derivseq[real](sin_coef),x!1)) = series(powerseq(cos_coef, x!1))")
((""
(hide 2)
((""
(expand "series")
((""
(apply-extensionality 1 :hide? t)
((""
(case-replace
"powerseq(derivseq[real](sin_coef), x!1) = powerseq(cos_coef, x!1)")
((""
(hide 2)
((""
(rewrite "apow_rew")
((""
(rewrite "apow_rew")
((""
(expand "apowerseq")
((""
(expand "derivseq")
((""
(apply-extensionality
1
:hide?
t)
((""
(lift-if)
((""
(ground)
(("1"
(expand
"sin_coef")
(("1"
(expand
"cos_coef")
(("1"
(expand
"factorial")
(("1"
(expand
"factorial")
(("1"
(expand
"even?")
(("1"
(expand
"altsign")
(("1"
(expand
"even?")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"sin_coef")
(("2"
(lift-if)
(("2"
(ground)
(("1"
(expand
"cos_coef")
(("1"
(lemma
"even_plus1")
(("1"
(inst
-
"x!3")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"altsign")
(("2"
(expand
"cos_coef")
(("2"
(lemma
"even_plus1")
(("2"
(inst
-
"x!3")
(("2"
(assert)
(("2"
(expand
"altsign")
(("2"
(expand
"factorial"
2
1)
(("2"
(expand
"factorial"
2
3)
(("2"
(assert)
(("2"
(name-replace
"FF"
"factorial(x!3)")
(("2"
(name-replace
"M1"
"(-1) ^ (x!3 / 2)")
(("1"
(name-replace
"X23"
"x!1 ^ x!3 ")
(("1"
(assert)
(("1"
(field
2)
nil
nil))
nil))
nil)
("2"
(expand
"even?")
(("2"
(skosimp*)
(("2"
(replace
-1)
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(deriv_Inf_sum formula-decl nil power_series_deriv nil)
(sin_conv formula-decl nil trig_fun nil)
(inf_sum const-decl "real" series nil)
(cos const-decl "real" trig_fun nil)
(cos_coef const-decl "real" trig_fun nil)
(derivseq const-decl "sequence[real]" power_series_derivseq nil)
(powerseq const-decl "sequence[real]" power_series nil)
(series const-decl "sequence[real]" series nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(apow_rew formula-decl nil power_series nil)
(apowerseq const-decl "sequence[real]" power_series nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(altsign const-decl "{i: int | i = -1 OR i = 1}" trig_fun nil)
(expt def-decl "real" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_expt application-judgement "int" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation 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)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(even? const-decl "bool" integers nil)
(factorial def-decl "posnat" factorial "ints/")
(rat_exp application-judgement "rat" exponentiation nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(rat nonempty-type-eq-decl nil rationals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posint nonempty-type-eq-decl nil integers nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(both_sides_times1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers 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)
(even_plus1 formula-decl nil naturalnumbers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(powerseries const-decl "sequence[real]" power_series nil)
(Inf_sum const-decl "real" power_series_conv nil)
(sin const-decl "real" trig_fun nil)
(sin_coef const-decl "real" trig_fun 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))
nil)
(deriv_sin-1 nil 3249311628
("" (skosimp*)
(("" (lemma "deriv_Inf_sum[real]")
(("" (inst -1 "sin_coef")
(("" (rewrite "sin_conv")
(("" (expand "sin")
(("" (assert)
(("" (expand "Inf_sum")
(("" (expand "inf_sum")
(("" (expand "powerseries")
(("" (replace -1)
(("" (hide -1)
(("" (expand "cos")
(("" (expand "inf_sum")
((""
(case-replace
"series(powerseq(derivseq[real](sin_coef),x!1)) = series(powerseq(cos_coef, x!1))")
((""
(hide 2)
((""
(expand "series")
((""
(apply-extensionality 1 :hide? t)
((""
(case-replace
"powerseq(derivseq[real](sin_coef), x!1) = powerseq(cos_coef, x!1)")
((""
(hide 2)
((""
(expand "powerseq")
((""
(expand "derivseq")
((""
(apply-extensionality
1
:hide?
t)
((""
(lift-if)
((""
(ground)
(("1"
(expand "sin_coef")
(("1"
(expand
"cos_coef")
(("1"
(expand
"factorial")
(("1"
(expand
"factorial")
(("1"
(expand
"even?")
(("1"
(expand
"altsign")
(("1"
(expand
"even?")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "sin_coef")
(("2"
(lift-if)
(("2"
(ground)
(("1"
(expand
"cos_coef")
(("1"
(lemma
"even_plus1")
(("1"
(inst
-
"x!3")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"altsign")
(("2"
(expand
"cos_coef")
(("2"
(lemma
"even_plus1")
(("2"
(inst
-
"x!3")
(("2"
(assert)
(("2"
(expand
"altsign")
(("2"
(expand
"factorial"
2
1)
(("2"
(expand
"factorial"
2
3)
(("2"
(assert)
(("2"
(name-replace
"FF"
"factorial(x!3)")
(("2"
(name-replace
"M1"
"(-1) ^ (x!3 / 2)")
(("1"
(name-replace
"X23"
"x!1 ^ x!3 ")
(("1"
(assert)
(("1"
(field
2)
nil
nil))
nil))
nil)
("2"
(expand
"even?")
(("2"
(skosimp*)
(("2"
(replace
-1)
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_Inf_sum formula-decl nil power_series_deriv nil)
(sin_conv formula-decl nil trig_fun nil)
(cos const-decl "real" trig_fun nil)
(cos_coef const-decl "real" trig_fun nil)
(derivseq const-decl "sequence[real]" power_series_derivseq nil)
(powerseq const-decl "sequence[real]" power_series nil)
(altsign const-decl "{i: int | i = -1 OR i = 1}" trig_fun nil)
(sigma def-decl "real" sigma "reals/")
(sin const-decl "real" trig_fun nil)
(sin_coef const-decl "real" trig_fun nil))
nil))
(cos_derivable 0
(cos_derivable-1 nil 3249311628
("" (lemma "cos_conv")
(("" (lemma "powerseries_derivable[real]")
(("1" (expand "cos")
(("1" (inst?)
(("1" (assert)
(("1" (expand "inf_sum")
(("1" (assert)
(("1" (expand "powerseries") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst + "x!1 + 1") (("2" (assert) nil nil)) nil)) nil))
nil))
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)
(powerseries_derivable formula-decl nil power_series_deriv 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)
(cos_coef const-decl "real" trig_fun nil)
(inf_sum const-decl "real" series nil)
(powerseries const-decl "sequence[real]" power_series nil)
(cos const-decl "real" trig_fun nil)
(cos_conv formula-decl nil trig_fun nil))
nil))
(deriv_cos_TCC1 0
(deriv_cos_TCC1-1 nil 3249311628
("" (rewrite "cos_derivable") nil nil)
((cos_derivable formula-decl nil trig_props nil)) nil))
(deriv_cos 0
(deriv_cos-3 nil 3352090481
("" (skosimp*)
(("" (lemma "deriv_Inf_sum[real]")
(("" (inst -1 "cos_coef")
(("" (rewrite "cos_conv")
(("" (expand "cos")
(("" (assert)
(("" (expand "Inf_sum")
(("" (expand "inf_sum")
(("" (expand "powerseries")
(("" (replace -1)
(("" (hide -1)
(("" (expand "sin")
(("" (expand "inf_sum")
((""
(case-replace
"series(powerseq(derivseq[real](cos_coef),x!1)) = -series(powerseq(sin_coef, x!1))")
(("1"
(hide -1)
(("1" (rewrite "limit_neg") nil nil))
nil)
("2"
(hide 2)
(("2"
(expand "series")
(("2"
(apply-extensionality 1 :hide? t)
(("2"
(case-replace
"powerseq(derivseq[real](cos_coef), x!1) = -powerseq(sin_coef, x!1)")
(("1"
(assert)
(("1"
(expand "-")
(("1"
(lemma "sigma_scal")
(("1"
(inst
-
"LAMBDA (x: nat): powerseq(sin_coef, x!1)(x)"
"-1"
"x!2"
"0")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(case-replace
"(LAMBDA (x: nat): powerseq(sin_coef, x!1)(x)) =powerseq(sin_coef, x!1)")
(("1"
(assert)
nil
nil)
("2"
(hide 2)
(("2"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "apow_rew")
(("2"
(rewrite "apow_rew")
(("2"
(expand "apowerseq")
(("2"
(expand "derivseq")
(("2"
(expand "-")
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(lift-if)
(("2"
(ground)
(("1"
(expand
"cos_coef")
(("1"
(expand
"sin_coef")
(("1"
(expand
"even?")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"cos_coef")
(("2"
(lift-if)
(("2"
(expand
"sin_coef")
(("2"
(lemma
"even_plus1")
(("2"
(inst
-
"x!3")
(("2"
(assert)
(("2"
(prop)
(("1"
(lift-if)
(("1"
(assert)
nil
nil))
nil)
("2"
(lift-if)
(("2"
(assert)
(("2"
(case-replace
"altsign(1 + x!3) = -altsign(x!3)")
(("1"
(hide
-1)
(("1"
(name
"FF"
"factorial(x!3)")
(("1"
(name-replace
"AA"
"altsign(x!3)")
(("1"
(name-replace
"X23"
"x!1 ^ x!3 ")
(("1"
(factor
1
l)
(("1"
(name
"XP1"
"(1 + x!3)")
(("1"
(replace
-1)
(("1"
(case-replace
"factorial(XP1) = XP1*factorial(x!3)")
(("1"
(name-replace
"F1"
"factorial(x!3)")
(("1"
(field
1)
nil
nil))
nil)
("2"
(hide
2)
(("2"
(replace
-1
*
rl)
(("2"
(expand
"factorial"
1
1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(hide
-1)
(("2"
(expand
"altsign")
(("2"
(expand
"even?")
(("2"
(skosimp*)
(("2"
(replace
-1)
(("2"
(case-replace
"x!3 - 1 = 2 * j!1 - 2")
(("1"
(case-replace
"2 * j!1 / 2 = j!1")
(("1"
(case-replace
"(2 * j!1 -2)/ 2 = j!1-1")
(("1"
(hide-all-but
1)
(("1"
(lemma
"expt_plus")
(("1"
(inst
-
"j!1-1"
"1"
"-1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(deriv_Inf_sum formula-decl nil power_series_deriv nil)
(cos_conv formula-decl nil trig_fun nil)
(minus_real_is_real application-judgement "real" reals nil)
(inf_sum const-decl "real" series nil)
(sin const-decl "real" trig_fun nil)
(sin_coef const-decl "real" trig_fun nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(derivseq const-decl "sequence[real]" power_series_derivseq nil)
(powerseq const-decl "sequence[real]" power_series nil)
(series const-decl "sequence[real]" series nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(convergent? const-decl "bool" convergence_sequences "analysis/")
(limit_neg formula-decl nil convergence_ops "analysis/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sigma_scal formula-decl nil sigma "reals/")
(apow_rew formula-decl nil power_series nil)
(apowerseq const-decl "sequence[real]" power_series nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(even_minus_even_is_even application-judgement "even_int" integers
nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_x1 formula-decl nil exponentiation nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(int_exp application-judgement "int" exponentiation nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(rat_exp application-judgement "rat" exponentiation 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 1.78 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.
|
