|
(trig_fun
(useful_prep_TCC1 0
(useful_prep_TCC1-1 nil 3298132328 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(useful_prep 0
(useful_prep-1 nil 3298132328
("" (skosimp*)
(("" (lemma "simple_conv[real]")
(("" (expand "simple") (("" (inst?) 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)
(simple_conv formula-decl nil power_series_conv nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(simple const-decl "sequence[real]" power_series_conv nil))
nil))
(altsign_prep 0
(altsign_prep-1 nil 3298132328
("" (induct "n")
(("1" (grind) nil nil)
("2" (skosimp*)
(("2" (expand "^")
(("2" (expand "expt" 1)
(("2" (expand "expt" 2) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(expt def-decl "real" exponentiation nil)
(nat_induction formula-decl nil naturalnumbers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(altsign_TCC1 0
(altsign_TCC1-1 nil 3298132328
("" (skosimp*) (("" (rewrite "even_div2") nil nil)) nil)
((even_div2 formula-decl nil naturalnumbers 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))
nil))
(altsign_TCC2 0
(altsign_TCC2-1 nil 3298132328
("" (case "(FORALL n: integer_pred((-1)^n))")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert)
(("1" (case "(FORALL n: (-1) ^ (n) = -1 OR (-1) ^ (n) = 1)")
(("1" (inst -1 "n!1/2")
(("1" (rewrite "even_div2") nil nil)) nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (expand "^")
(("1" (expand "expt") (("1" (propax) nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (expand "^")
(("2" (expand "expt" 1)
(("2" (expand "expt" 2) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (assert) (("2" (rewrite "even_div2") nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil))
nil)
((rat_exp application-judgement "rat" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(expt def-decl "real" exponentiation nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(even_div2 formula-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(n!1 skolem-const-decl "nat" trig_fun nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil))
nil))
(altsign_TCC3 0
(altsign_TCC3-1 nil 3298132328
("" (skosimp*)
(("" (rewrite "odd_div2")
(("" (lemma "even_iff_not_odd")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((odd_div2 formula-decl nil naturalnumbers 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(even_iff_not_odd formula-decl nil naturalnumbers nil))
nil))
(altsign_TCC4 0
(altsign_TCC4-1 nil 3298132328
("" (skosimp*)
(("" (case "(n!1 - 1) / 2 >= 0")
(("1" (lemma "even_iff_not_odd")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "odd_div2")
(("1" (inst?)
(("1" (assert)
(("1" (case "integer_pred((-1) ^ ((n!1 - 1) / 2))")
(("1" (lemma "altsign_prep")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (hide 3)
(("2" (lemma "altsign_prep")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
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 "[numfield, numfield -> numfield]" number_fields 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(odd_div2 formula-decl nil naturalnumbers nil)
(altsign_prep formula-decl nil trig_fun nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rat_exp application-judgement "rat" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(even_iff_not_odd formula-decl nil naturalnumbers nil))
nil))
(abs_altsign 0
(abs_altsign-1 nil 3298132884
("" (skosimp*)
(("" (expand "altsign")
(("" (lift-if)
(("" (ground)
(("1" (rewrite "abs_hat")
(("1" (expand "abs")
(("1" (lemma "expt_1i")
(("1" (inst?)
(("1" (assert) nil nil)
("2" (expand "even?")
(("2" (skosimp*)
(("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "even?") (("2" (propax) nil nil)) nil))
nil)
("2" (lemma "odd_iff_not_even")
(("2" (inst?)
(("2" (assert)
(("2" (rewrite "abs_hat")
(("1" (expand "abs")
(("1" (rewrite "expt_1i")
(("1" (lemma "odd_div2")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (lemma "odd_div2")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rat_exp application-judgement "rat" exponentiation nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(altsign const-decl "{i: int | i = -1 OR i = 1}" trig_fun nil)
(rat_abs_is_nonneg application-judgement "{r: nonneg_rat | r >= q}"
real_defs nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(n!1 skolem-const-decl "nat" trig_fun 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)
(even? const-decl "bool" integers nil)
(expt_1i formula-decl nil exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(abs_hat formula-decl nil exponent_props "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(odd_div2 formula-decl nil naturalnumbers nil)
(odd_iff_not_even formula-decl nil naturalnumbers nil))
shostak))
(sin_conv_TCC1 0
(sin_conv_TCC1-1 nil 3298204091
("" (expand "not_one_element?")
(("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
nil))
nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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_plus_real_is_real application-judgement "real" reals nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(sin_conv_TCC2 0
(sin_conv_TCC2-1 nil 3298204091
("" (lemma "deriv_domain_real") (("" (propax) nil nil)) nil)
((deriv_domain_real formula-decl nil deriv_domain "analysis/"))
shostak))
(sin_conv_TCC3 0
(sin_conv_TCC3-1 nil 3298204091
("" (skosimp*) (("" (assert) nil nil)) nil) nil shostak))
(sin_conv 0
(sin_conv-3 nil 3352095508
("" (expand "conv_powerseries?")
(("" (skosimp*)
(("" (lemma "useful_prep")
(("" (inst?)
(("" (lemma "comparison_test")
(("" (assert)
((""
(inst -1 "powerseq(sin_coef, x!1)"
"(LAMBDA n: (abs(x!1)) ^ n / factorial(n))")
(("" (expand "powerseries")
(("" (assert)
(("" (hide -1 2)
(("" (skosimp*)
(("" (rewrite "apow_rew")
(("" (expand "apowerseq")
(("" (expand "sin_coef")
((""
(lift-if)
((""
(ground)
(("1"
(expand "abs" 1 1)
(("1" (assert) nil nil))
nil)
("2"
(rewrite "abs_mult")
(("2"
(rewrite "abs_0")
(("2" (assert) nil nil))
nil))
nil)
("3"
(rewrite "abs_mult")
(("3"
(rewrite "abs_div")
(("3"
(expand "abs" 2 2)
(("3"
(rewrite "abs_altsign")
(("3"
(rewrite "abs_hat")
(("1" (assert) nil nil)
("2"
(flatten)
(("2"
(replace -1)
(("2"
(assert)
(("2"
(rewrite "abs_0")
(("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)
((nnreal_exp application-judgement "nnreal" exponentiation 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)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(powerseries const-decl "sequence[real]" power_series nil)
(apow_rew formula-decl nil power_series nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(abs_0 formula-decl nil abs_lems "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(abs_mult formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(abs_div formula-decl nil real_props nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(abs_altsign formula-decl nil trig_fun nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(hat_02n formula-decl nil power_series nil)
(nat_exp application-judgement "nat" exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(abs_hat formula-decl nil exponent_props "reals/")
(nzreal nonempty-type-eq-decl nil reals nil)
(rat_abs_is_nonneg application-judgement "{r: nonneg_rat | r >= q}"
real_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(altsign const-decl "{i: int | i = -1 OR i = 1}" trig_fun nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(apowerseq const-decl "sequence[real]" power_series nil)
(real_times_real_is_real application-judgement "real" reals 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(^ const-decl "real" exponentiation nil)
(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)
(sin_coef const-decl "real" trig_fun 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)
(comparison_test formula-decl nil series nil)
(useful_prep formula-decl nil trig_fun nil)
(conv_powerseries? const-decl "bool" power_series_conv nil))
nil)
(sin_conv-2 nil 3320063019
("" (stop-rewrite "abs_0")
(("" (expand "conv_powerseries?")
(("" (skosimp*)
(("" (lemma "useful_prep")
(("" (inst?)
(("" (lemma "comparison_test")
(("" (assert)
((""
(inst -1 "powerseq(sin_coef, x!1)"
"(LAMBDA n: (abs(x!1)) ^ n / factorial(n))")
(("" (expand "powerseries")
(("" (assert)
(("" (hide -1 2)
(("" (skosimp*)
(("" (expand "powerseq")
(("" (expand "sin_coef")
((""
(lift-if)
((""
(ground)
(("1"
(expand "abs" 1 1)
(("1" (assert) nil nil))
nil)
("2"
(rewrite "abs_mult")
(("2"
(rewrite "abs_0")
(("2" (assert) nil nil))
nil))
nil)
("3"
(rewrite "abs_mult")
(("3"
(rewrite "abs_div")
(("3"
(expand "abs" 2 2)
(("3"
(rewrite "abs_altsign")
(("3"
(rewrite "abs_hat")
(("1" (assert) nil nil)
("2"
(flatten)
(("2"
(replace -1)
(("2"
(assert)
(("2"
(rewrite
"zero_hat")
(("2"
(rewrite "abs_0")
(("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)
((abs_hat formula-decl nil exponent_props "reals/")
(zero_hat formula-decl nil exponent_props "reals/")
(powerseq const-decl "sequence[real]" power_series nil)
(comparison_test formula-decl nil series nil))
nil)
(sin_conv-1 nil 3298132328
("" (expand "conv_powerseries?")
(("" (skosimp*)
(("" (lemma "useful_prep")
(("" (inst?)
(("" (lemma "comparison_test")
(("" (assert)
((""
(inst -1 "powerseq(sin_coef, x!1)"
"(LAMBDA n: (abs(x!1)) ^ n / factorial(n))")
(("" (expand "powerseries")
(("" (assert)
(("" (hide -1 2)
(("" (skosimp*)
(("" (expand "powerseq")
(("" (expand "sin_coef")
(("" (lift-if)
((""
(ground)
(("1"
(expand "abs" 1 1)
(("1" (assert) nil nil))
nil)
("2"
(rewrite "abs_mult")
(("2"
(rewrite "abs_0")
(("2" (assert) nil nil))
nil))
nil)
("3"
(rewrite "abs_mult")
(("3"
(rewrite "abs_div")
(("3"
(expand "abs" 2 2)
(("3"
(rewrite "abs_altsign")
(("3"
(rewrite "abs_hat")
(("1" (assert) nil nil)
("2"
(flatten)
(("2"
(replace -1)
(("2"
(assert)
(("2"
(rewrite "zero_hat")
(("2"
(rewrite "abs_0")
(("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)
((abs_hat formula-decl nil exponent_props "reals/")
(zero_hat formula-decl nil exponent_props "reals/")
(powerseq const-decl "sequence[real]" power_series nil)
(comparison_test formula-decl nil series nil))
nil))
(sin_TCC1 0
(sin_TCC1-1 nil 3298132328
("" (skosimp*)
(("" (lemma "sin_conv")
(("" (expand "conv_powerseries?")
(("" (inst?)
(("" (expand "powerseries")
(("" (expand "conv_series?") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sin_conv formula-decl nil trig_fun 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)
(conv_series? const-decl "bool" series nil)
(powerseries const-decl "sequence[real]" power_series nil)
(conv_powerseries? const-decl "bool" power_series_conv nil))
nil))
(cos_conv 0
(cos_conv-2 nil 3352095538
("" (expand "conv_powerseries?")
(("" (skosimp*)
(("" (lemma "useful_prep")
(("" (inst?)
(("" (lemma "comparison_test")
(("" (assert)
((""
(inst -1 "powerseq(cos_coef, x!1)"
"(LAMBDA n: (abs(x!1)) ^ n / factorial(n))")
(("" (expand "powerseries")
(("" (assert)
(("" (hide -1 2)
(("" (skosimp*)
(("" (rewrite "apow_rew")
(("" (expand "apowerseq")
(("" (expand "cos_coef")
((""
(lift-if)
((""
(ground)
(("1"
(rewrite "abs_div")
(("1"
(case-replace
"abs(altsign(n!1)) = 1")
(("1"
(expand "abs" 1 1)
(("1"
(rewrite "abs_hat_nat")
(("1"
(assert)
(("1"
(lift-if)
(("1"
(expand "altsign")
(("1"
(assert)
(("1"
(expand
"factorial")
(("1"
(expand
"abs"
1
1)
(("1"
(assert)
(("1"
(typepred
"x!1")
(("1"
(replace
-3)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "altsign")
(("2"
(lemma "altsign_prep")
(("2"
(inst?)
(("2"
(expand "abs")
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "abs_mult")
(("2"
(rewrite "abs_hat_nat")
(("2"
(case-replace
"abs(altsign(n!1)) = 1")
(("1"
(rewrite "abs_div")
(("1"
(rewrite "abs_altsign")
(("1"
(expand "abs" 1 1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2 3)
(("2"
(lemma "altsign_prep")
(("2"
(expand "altsign")
(("2"
(inst?)
(("1"
(expand "abs")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil)
("2"
(reveal 1)
(("2"
(assert)
(("2"
(rewrite
"abs_div")
(("2"
(assert)
(("2"
(rewrite
"abs_altsign")
(("2"
(expand
"abs"
1
1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(rewrite "abs_0")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_exp application-judgement "nnreal" exponentiation 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)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(powerseries const-decl "sequence[real]" power_series nil)
(apow_rew formula-decl nil power_series nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(factorial_0 formula-decl nil factorial "ints/")
(rat_abs_is_nonneg application-judgement "{r: nonneg_rat | r >= q}"
real_defs nil)
(abs_hat_nat formula-decl nil exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(rat_exp application-judgement "rat" exponentiation nil)
(expt_x0 formula-decl nil exponentiation nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_exp application-judgement "int" exponentiation nil)
(minus_int_is_int application-judgement "int" integers 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)
(minus_rat_is_rat application-judgement "rat" rationals nil)
(altsign_prep formula-decl nil trig_fun nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(abs_div formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(altsign const-decl "{i: int | i = -1 OR i = 1}" trig_fun nil)
(n!1 skolem-const-decl "nat" trig_fun nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(abs_altsign formula-decl nil trig_fun nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(abs_mult formula-decl nil real_props nil)
(abs_0 formula-decl nil abs_lems "reals/")
(apowerseq const-decl "sequence[real]" power_series nil)
(real_times_real_is_real application-judgement "real" reals 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(^ const-decl "real" exponentiation nil)
(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)
(cos_coef const-decl "real" trig_fun 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)
(comparison_test formula-decl nil series nil)
(useful_prep formula-decl nil trig_fun nil)
(conv_powerseries? const-decl "bool" power_series_conv nil))
nil)
(cos_conv-1 nil 3298132328
("" (expand "conv_powerseries?")
(("" (skosimp*)
(("" (lemma "useful_prep")
(("" (inst?)
(("" (lemma "comparison_test")
(("" (assert)
((""
(inst -1 "powerseq(cos_coef, x!1)"
"(LAMBDA n: (abs(x!1)) ^ n / factorial(n))")
(("" (expand "powerseries")
(("" (assert)
(("" (hide -1 2)
(("" (skosimp*)
(("" (expand "powerseq")
(("" (expand "cos_coef")
(("" (lift-if)
((""
(ground)
(("1"
(rewrite "abs_div")
(("1"
(case-replace
"abs(altsign(n!1)) = 1")
(("1"
(expand "abs" 1 1)
(("1"
(rewrite "abs_hat_nat")
(("1"
(assert)
(("1"
(lift-if)
(("1"
(expand "altsign")
(("1"
(assert)
(("1"
(expand "factorial")
(("1"
(expand "abs" 1 1)
(("1"
(assert)
(("1"
(typepred
"x!1")
(("1"
(replace -3)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "altsign")
(("2"
(lemma "altsign_prep")
(("2"
(inst?)
(("2"
(expand "abs")
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "abs_mult")
(("2"
(rewrite "abs_hat_nat")
(("2"
(case-replace
"abs(altsign(n!1)) = 1")
(("1"
(rewrite "abs_div")
(("1"
(rewrite "abs_altsign")
(("1"
(expand "abs" 1 1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2 3)
(("2"
(lemma "altsign_prep")
(("2"
(expand "altsign")
(("2"
(inst?)
(("1"
(expand "abs")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil)
("2"
(reveal 1)
(("2"
(lemma
"not_even_int")
(("2"
(inst?)
(("2"
(assert)
(("2"
(rewrite
"abs_div")
(("2"
(assert)
(("2"
(rewrite
"abs_altsign")
(("2"
(expand
"abs"
1
1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(rewrite "abs_0")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((powerseq const-decl "sequence[real]" power_series nil)
(comparison_test formula-decl nil series nil))
nil))
(cos_TCC1 0
(cos_TCC1-1 nil 3298132328
("" (skosimp*)
(("" (expand "conv_series?")
(("" (lemma "cos_conv")
(("" (expand "conv_powerseries?")
(("" (inst?)
(("" (expand "powerseries") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((conv_series? const-decl "bool" series nil)
(conv_powerseries? const-decl "bool" power_series_conv nil)
(powerseries const-decl "sequence[real]" power_series 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)
(cos_conv formula-decl nil trig_fun nil))
nil))
(tan_TCC1 0
(tan_TCC1-1 nil 3298132328 ("" (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)
(/= 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)
(tan_domain type-eq-decl nil trig_fun nil)
(series const-decl "sequence[real]" series nil)
(convergence const-decl "bool" convergence_sequences "analysis/")
(limit const-decl "real" convergence_sequences "analysis/")
(inf_sum const-decl "real" series nil)
(cos const-decl "real" trig_fun nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(sin_0 0
(sin_0-1 nil 3298132328
("" (expand "sin")
(("" (expand "inf_sum")
(("" (lemma "limit_series_shift")
(("" (inst?)
(("" (inst -1 "1")
(("" (split -1)
(("1" (assert)
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "sigma")
(("1" (expand "powerseq")
(("1" (case-replace "sin_coef(0) * 0 ^ 0 = 0")
(("1" (hide -1)
(("1" (assert)
(("1"
(case-replace
"(LAMBDA n: sin_coef(1 + n) * 0 ^ (1 + n)) = (LAMBDA n: 0)")
(("1"
(hide -1)
(("1"
(rewrite "zero_series_limit")
(("1"
(expand "sin_coef")
(("1"
(expand "sigma")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(apply-extensionality 1 :hide? t)
nil
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "sin_coef")
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "sin_conv")
(("2" (expand "conv_powerseries?")
(("2" (expand "powerseries")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inf_sum const-decl "real" 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)
(sin_coef const-decl "real" trig_fun nil)
(sigma def-decl "real" sigma "reals/")
(^ 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(hat_02n formula-decl nil power_series nil)
(sigma_0_neg formula-decl nil sigma_nat "reals/")
(zero_series_limit formula-decl nil series nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(expt def-decl "real" exponentiation nil)
(nat_exp application-judgement "nat" exponentiation nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
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)
(sin_conv formula-decl nil trig_fun nil)
(powerseries const-decl "sequence[real]" power_series nil)
(conv_powerseries? const-decl "bool" power_series_conv nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(limit_series_shift formula-decl nil series nil)
(sin const-decl "real" trig_fun nil))
nil))
(cos_0 0
(cos_0-1 nil 3298132328
("" (expand "cos")
(("" (expand "inf_sum")
(("" (lemma "limit_series_shift")
(("" (inst?)
(("" (inst -1 "1")
(("" (split -1)
(("1" (assert)
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "sigma")
(("1" (expand "powerseq")
(("1" (case-replace "cos_coef(0) * 0 ^ 0 = 1")
(("1" (hide -1)
(("1" (assert)
(("1"
(case-replace
"(LAMBDA n: cos_coef(1 + n) * 0 ^ (1 + n)) = (LAMBDA n: 0)")
(("1"
(hide -1)
(("1"
(rewrite "zero_series_limit")
(("1"
(expand "cos_coef")
(("1" (grind) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(apply-extensionality 1 :hide? t)
(("2"
(typepred "x!1")
(("2"
(expand "cos_coef")
(("2"
(case-replace
"0 ^ (1 + x!1) = 0")
(("1" (assert) nil nil)
("2"
(hide 2)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "cos_coef")
(("2"
(expand "factorial")
(("2"
(expand "^")
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.73 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.
|
