Quelle trig_props.prf
Sprache: Lisp
(trig_propsnil 3299592135"" (expand "connected?" ) (("" (propax) nil nil )) nil )"bool" deriv_domain_def "analysis/" ))nil 3299592135"" (expand "not_one_element?" )"" (skosimp*)"" (assert ) (("" (inst + "x!1+1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" deriv_domain_def "analysis/" ))nil 3299592135"" (skosimp*) (("" (inst + "1" ) (("" (skosimp*) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil 3299592135 ("" (skosimp*) nil nil )nil shostak))nil 3471704739"" (expand "deriv_domain?" )"" (skosimp*) (("" (inst + e!1/2) (("" (grind) nil nil )) nil ))nil ))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{y: posreal | y >= x}" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"bool" deriv_domain_def "analysis/" )"real" reals nil ))nil ))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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power_series_deriv nil )"real" series nil )"sequence[real]" power_series nil )"real" trig_fun nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" trig_fun nil )nil trig_fun nil ))nil ))nil 3249311628"" (lemma "sin_derivable" ) (("" (propax) nil nil )) nil )nil trig_props nil )) nil ))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" )"" "series(powerseq(derivseq[real](sin_coef),x!1)) = series(powerseq(cos_coef, x!1))" )"" "" expand "series" )"" "" "powerseq(derivseq[real](sin_coef), x!1) = powerseq(cos_coef, x!1)" )"" "" rewrite "apow_rew" )"" rewrite "apow_rew" )"" expand "apowerseq" )"" expand "derivseq" )"" "" "" "1" expand "sin_coef" )"1" expand "cos_coef" )"1" expand "factorial" )"1" expand "factorial" )"1" expand "even?" )"1" expand "altsign" )"1" expand "even?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sin_coef" )"2" "2" "1" expand "cos_coef" )"1" "even_plus1" )"1" "x!3" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "altsign" )"2" expand "cos_coef" )"2" "even_plus1" )"2" "x!3" )"2" assert )"2" expand "altsign" )"2" expand "factorial" "2" expand "factorial" "2" assert )"2" "FF" "factorial(x!3)" )"2" "M1" "(-1) ^ (x!3 / 2)" )"1" "X23" "x!1 ^ x!3 " )"1" assert )"1" nil nil ))nil ))nil )"2" expand "even?" )"2" "2" replace "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 reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power_series_deriv nil )nil trig_fun nil )"real" series nil )"real" trig_fun nil )"real" trig_fun nil )"sequence[real]" power_series_derivseq nil )"sequence[real]" power_series nil )"sequence[real]" series nil )"[T, T -> boolean]" equalities nil )nil power_series nil )"sequence[real]" power_series nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )"real" exponentiation nil )"posint" nil )"real" reals nil )"{i: int | i = -1 OR i = 1}" trig_fun nil )"real" exponentiation nil )"(total_order?[real])" nil )"int" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"nzrat" rationalsnil )"nzrat" rationalsnil )"bool" integers nil )"posnat" factorial "ints/" )"rat" exponentiation nil )"nonneg_rat" nil )nil rationals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )nil integers nil )"rat" rationals nil )"posint" nil )nil real_props nil )nil reals nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil integers nil )"bool" reals nil )nil integers nil )"posint" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil naturalnumbers nil )"rat" rationals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"sequence[real]" power_series nil )"real" power_series_conv nil )"real" trig_fun nil )"real" trig_fun nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil ))nil )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" )"" "series(powerseq(derivseq[real](sin_coef),x!1)) = series(powerseq(cos_coef, x!1))" )"" "" expand "series" )"" "" "powerseq(derivseq[real](sin_coef), x!1) = powerseq(cos_coef, x!1)" )"" "" expand "powerseq" )"" expand "derivseq" )"" "" "" "1" expand "sin_coef" )"1" expand "cos_coef" )"1" expand "factorial" )"1" expand "factorial" )"1" expand "even?" )"1" expand "altsign" )"1" expand "even?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sin_coef" )"2" "2" "1" expand "cos_coef" )"1" "even_plus1" )"1" "x!3" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "altsign" )"2" expand "cos_coef" )"2" "even_plus1" )"2" "x!3" )"2" assert )"2" expand "altsign" )"2" expand "factorial" "2" expand "factorial" "2" assert )"2" "FF" "factorial(x!3)" )"2" "M1" "(-1) ^ (x!3 / 2)" )"1" "X23" "x!1 ^ x!3 " )"1" assert )"1" nil nil ))nil ))nil )"2" expand "even?" )"2" "2" replace "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 power_series_deriv nil )nil trig_fun nil )"real" trig_fun nil )"real" trig_fun nil )"sequence[real]" power_series_derivseq nil )"sequence[real]" power_series nil )"{i: int | i = -1 OR i = 1}" trig_fun nil )"real" sigma "reals/" )"real" trig_fun nil )"real" trig_fun nil ))nil ))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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power_series_deriv nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"real" trig_fun nil )"real" series nil )"sequence[real]" power_series nil )"real" trig_fun nil )nil trig_fun nil ))nil ))nil 3249311628"" (rewrite "cos_derivable" ) nil nil )nil trig_props nil )) nil ))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" )"" "series(powerseq(derivseq[real](cos_coef),x!1)) = -series(powerseq(sin_coef, x!1))" )"1" "1" (rewrite "limit_neg" ) nil nil ))nil )"2" "2" expand "series" )"2" "2" "powerseq(derivseq[real](cos_coef), x!1) = -powerseq(sin_coef, x!1)" )"1" assert )"1" expand "-" )"1" "sigma_scal" )"1" "LAMBDA (x: nat): powerseq(sin_coef, x!1)(x)" "-1" "x!2" "0" )"1" assert )"1" replace -1)"1" "(LAMBDA (x: nat): powerseq(sin_coef, x!1)(x)) =powerseq(sin_coef, x!1)" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "apow_rew" )"2" rewrite "apow_rew" )"2" expand "apowerseq" )"2" expand "derivseq" )"2" expand "-" )"2" "2" "2" "1" expand "cos_coef" )"1" expand "sin_coef" )"1" expand "even?" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "cos_coef" )"2" "2" expand "sin_coef" )"2" "even_plus1" )"2" "x!3" )"2" assert )"2" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" "altsign(1 + x!3) = -altsign(x!3)" )"1" "1" "FF" "factorial(x!3)" )"1" "AA" "altsign(x!3)" )"1" "X23" "x!1 ^ x!3 " )"1" "1" "XP1" "(1 + x!3)" )"1" replace "1" "factorial(XP1) = XP1*factorial(x!3)" )"1" "F1" "factorial(x!3)" )"1" nil nil ))nil )"2" "2" replace "2" expand "factorial" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "altsign" )"2" expand "even?" )"2" "2" replace "2" "x!3 - 1 = 2 * j!1 - 2" )"1" "2 * j!1 / 2 = j!1" )"1" "(2 * j!1 -2)/ 2 = j!1-1" )"1" "1" "expt_plus" )"1" "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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power_series_deriv nil )nil trig_fun nil )"real" reals nil )"real" series nil )"real" trig_fun nil )"real" trig_fun nil )"[T -> real]" real_fun_ops "reals/" )"sequence[real]" power_series_derivseq nil )"sequence[real]" power_series nil )"sequence[real]" series nil )"[T, T -> boolean]" equalities nil )"bool" convergence_sequences "analysis/" )nil convergence_ops "analysis/" )"odd_int" integers nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )nil sigma "reals/" )nil power_series nil )"sequence[real]" power_series nil )"rat" rationals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integersnil )nil exponentiation nil )nil exponentiation nil )"nzrat" rationals nil )"int" exponentiation nil )"nzrat" rationalsnil )"int" integers nil )"nzreal" exponentiation nil )nil reals nil )"odd_int" integersnil )"rat" rationals nil )"even_int" integersnil )"rat" exponentiation nil )"posrat" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )"rat" rationals nil )"posint" nil )nil integers nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )"int" integers nil )"int" integers nil )"{i: int | i = -1 OR i = 1}" trig_fun nil )"posint" nil )nil naturalnumbers nil )"bool" integers nil )"real" reals nil )"posint" nil )"real" exponentiation nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"sequence[real]" power_series nil )"real" power_series_conv nil )"real" trig_fun nil )"real" trig_fun nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil ))nil )nil 3298209019"" (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" )"" "series(powerseq(derivseq[real](cos_coef),x!1)) = -series(powerseq(sin_coef, x!1))" )"1" "1" rewrite "limit_neg" )"1" "1" "sin_conv" )"1" expand "conv_powerseries?" )"1" "1" expand "powerseries" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" "2" "powerseq(derivseq[real](cos_coef), x!1) = -powerseq(sin_coef, x!1)" )"1" assert )"1" expand "-" )"1" "sigma_scal" )"1" "LAMBDA (x: nat): powerseq(sin_coef, x!1)(x)" "-1" "x!2" "0" )"1" assert )"1" replace -1)"1" "(LAMBDA (x: nat): powerseq(sin_coef, x!1)(x)) =powerseq(sin_coef, x!1)" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "powerseq" )"2" expand "derivseq" )"2" expand "-" )"2" "2" "2" "1" expand "cos_coef" )"1" expand "sin_coef" )"1" expand "even?" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "cos_coef" )"2" "2" expand "sin_coef" )"2" "even_plus1" )"2" "x!3" )"2" assert )"2" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" "altsign(1 + x!3) = -altsign(x!3)" )"1" "1" "FF" "factorial(x!3)" )"1" "AA" "altsign(x!3)" )"1" "X23" "x!1 ^ x!3 " )"1" "1" "XP1" "(1 + x!3)" )"1" replace "1" "factorial(XP1) = XP1*factorial(x!3)" )"1" "F1" "factorial(x!3)" )"1" nil nil ))nil )"2" "2" replace "2" expand "factorial" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "altsign" )"2" expand "even?" )"2" "2" replace "2" "x!3 - 1 = 2 * j!1 - 2" )"1" "2 * j!1 / 2 = j!1" )"1" "(2 * j!1 -2)/ 2 = j!1-1" )"1" "1" "expt_plus" )"1" "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 power_series_deriv nil )nil trig_fun nil )"real" trig_fun nil )"real" trig_fun nil )"sequence[real]" power_series_derivseq nil )"sequence[real]" power_series nil )nil convergence_ops "analysis/" )nil sigma "reals/" )"{i: int | i = -1 OR i = 1}" trig_fun nil )"real" sigma "reals/" )"real" trig_fun nil )"real" trig_fun nil ))nil )nil 3249311628"" (skosimp*)"" (lemma "deriv_inf_series" )"" (inst -1 "cos_coef" )"" (split -1)"1" (assert )"1" (expand "cos" )"1" (expand "inf_sum" )"1" (expand "powerseries" )"1" (replace -1 * rl)"1" (hide -1)"1" (assert )"1" (expand "sin" )"1" (expand "deriv_powerseq" )"1" (expand "inf_sum" )"1" "limit_series_shift" )"1" "1" "1" )"1" "1" replace -1)"1" "1" assert )"1" expand "sigma" )"1" "limit_neg" )"1" "1" replace -1 * rl)"1" "1" "series(LAMBDA n: cos_coef(1 + n) * x!1 ^ n + n * cos_coef(1 + n) * x!1 ^ n) = -series(powerseq(sin_coef, x!1))" )"1" "1" "-series(powerseq(sin_coef, x!1)) = series(-powerseq(sin_coef, x!1))" )"1" "1" rewrite "congruence" )"1" "1" "1" expand "-" )"1" expand "powerseq" )"1" expand "sin_coef" )"1" expand "cos_coef" )"1" "1" "1" "1" "1" "even_plus1" )"1" "x!2" )"1" assert )nil nil ))nil ))nil ))nil )"2" "Y" "x!2" )"2" "X" "x!1" )"2" assert )nil nil ))nil ))nil )"3" "Y" "x!2" )"3" "X" "x!1" )"3" "factorial(1 + Y) = factorial(Y)* (1+Y)" )"1" "1" "FF" "factorial(Y)" )"1" "altsign(1+Y) = - altsign(Y)" )"1" "AA" "altsign(Y)" )"1" "EE" "X^Y" )"1" "-AA / (FF * (1 + Y)) * EE + EE * (-AA / (FF * (1 + Y))) * Y = -AA * EE * (1 / (FF * (1 + Y)) + Y/ (FF * (1 + Y)))" )"1" "1" "(1 / (FF * (1 + Y)) + Y / (FF * (1 + Y))) = (1 + Y)/ (FF * (1 + Y))" )"1" "1" "DD" "(1+Y)" )"1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" expand "altsign" )"2" "2" "2" expand "^" )"2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "factorial" "2" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "even_plus1" )"4" "x!2" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "-" )"2" expand "powerseq" )"2" expand "series" )"2" "sigma_scal" )"2" "2" "-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sin_conv" )"2" "2" expand "powerseries" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "deriv_powerseries_conv" )"2" "2" assert )"2" "1" (inst?) nil nil )"2" assert )"2" "2" "2" expand "powerseries" )"2" "cos_conv" )"2" "2" expand "powerseries" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (rewrite "cos_conv" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" trig_fun nil )"real" trig_fun nil )"real" sigma "reals/" )"sequence[real]" power_series nil )"real" trig_fun nil )nil sigma "reals/" )"{i: int | i = -1 OR i = 1}" trig_fun nil )nil trig_fun nil )nil convergence_ops "analysis/" )nil trig_fun nil )nil series nil )"real" trig_fun nil ))nil ))nil 3249311628"" (lemma "cos_derivable" )"" (lemma "sin_derivable" )"" (expand "derivable?" )"" (skosimp*)"" (inst?)"" (inst?)"" (lemma "sum_derivable[real]" )"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (assert )"1" (hide 2)"1" (lemma "prod_derivable[real]" )"1" (inst -1 "sin" "sin" "x!1" )"1" (assert )"1" (lemma "prod_derivable[real]" )"1" "cos" "cos" "x!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_props nil )nil deriv_domain "analysis/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" trig_fun nil )"real" trig_fun nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives_def "analysis/" )nil booleans nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil derivatives_def "analysis/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" derivatives "analysis/" )nil trig_props nil ))nil ))nil 3445341842"" (expand "const_fun" )"" (lemma "cos_derivable" )"" (lemma "sin_derivable" )"" (case "derivable?[real](cos * cos)" )"1" (case "derivable?[real](sin * sin)" )"1" "derivable?[real](sin * sin + cos * cos)" )"1" (case "deriv(sin*sin+cos*cos) = const_fun(0)" )"1" (lemma "null_derivative[real]" )"1" (inst -1 "sin*sin+cos*cos" )"1" (flatten)"1" (hide -1)"1" (split -1)"1" (hide -2)"1" (hide -2)"1" case "(sin * sin + cos * cos)(0) = 1" )"1" expand "constant?" )"1" "1" "x!1" "0" )"1" replace -1)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" "sin_0" )"2" "cos_0" )"2" expand "+ " )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide 2)"2" case "deriv(sin * sin + cos * cos)(x!1) = const_fun(0)(x!1)" )"1" "1" expand "deriv" -1)"1" replace -1)"1" expand "const_fun" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!1+1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (expand "connected?" ) (("3" (propax) nil nil ))nil ))nil )"2" (hide 2)"2" (lemma "deriv_sum[real]" )"1" (apply-extensionality 1 :hide? t)"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" "1" assert )"1" expand "deriv" 1)"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "sin" "sin" "x!1" )"1" assert )"1" expand "derivable?" "1" expand "derivable?" "1" "1" "1" assert )"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "cos" "cos" "x!1" )"1" assert )"1" replace "1" "1" "deriv_cos" )"1" "1" expand "deriv" "1" replace "1" "1" "deriv_sin" )"1" "1" expand "deriv" "1" replace "1" "1" expand "const_fun" )"1" 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 )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!1+1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide 2)"2" (lemma "sum_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (expand "derivable?" -2)"1" (expand "derivable?" -3)"1" (inst?)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_props nil )"real" trig_fun nil )"[T -> real]" real_fun_ops "reals/" )"bool" derivatives "analysis/" )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil derivatives_def "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil deriv_domain "analysis/" )nil derivatives_def "analysis/" )nil trig_props nil )"real" reals nil )nil trig_props nil )"bool" deriv_domain_def "analysis/" )nil derivatives_def "analysis/" )nil derivative_props "analysis/" )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil trig_fun nil )"real" reals nil )"real" reals nil )nil trig_fun nil )"bool" real_fun_preds "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" derivatives "analysis/" )nil derivatives "analysis/" )"[T, T -> boolean]" equalities nil )"(convergent?)" "analysis/" )"deriv_fun" derivatives"analysis/" )nil derivatives_def "analysis/" )"real" trig_fun nil )nil trig_props nil )"[T -> real]" real_fun_ops "reals/" ))nil )nil 3445341805"" (expand "const_fun" )"" (lemma "cos_derivable" )"" (lemma "sin_derivable" )"" (case "derivable?[real](cos * cos)" )"1" (case "derivable?[real](sin * sin)" )"1" "derivable?[real](sin * sin + cos * cos)" )"1" (case "deriv(sin*sin+cos*cos) = const_fun(0)" )"1" (lemma "null_derivative[real]" )"1" (inst -1 "sin*sin+cos*cos" )"1" (flatten)"1" (hide -1)"1" (split -1)"1" (hide -2)"1" (hide -2)"1" case "(sin * sin + cos * cos)(0) = 1" )"1" expand "constant?" )"1" "1" "x!1" "0" )"1" replace -1)"1" (propax) nil )))))))))"2" "2" "sin_0" )"2" "cos_0" )"2" expand "+ " )"2" expand "*" )"2" assert )nil )))))))))))))))))"2" (skosimp*)"2" (hide 2)"2" case "deriv(sin * sin + cos * cos)(x!1) = const_fun(0)(x!1)" )"1" "1" expand "deriv" -1)"1" replace -1)"1" expand "const_fun" )"1" (propax) nil )))))))))"2" replace -1)"2" (propax) nil )))))))))))))))))"2" (hide -1 2)"2" (skosimp*)"2" (inst + "x!1+1" )"2" (assert ) nil )))))))))"2" (hide 2)"2" (lemma "deriv_sum[real]" )"1" (apply-extensionality 1 :hide? t)"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" "1" assert )"1" expand "deriv" 1)"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "sin" "sin" "x!1" )"1" assert )"1" expand "derivable?" "1" expand "derivable" "1" "1" "1" assert )"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "cos" "cos" "x!1" )"1" assert )"1" replace "1" "1" "deriv_cos" )"1" "1" expand "deriv" "1" replace "1" "1" "deriv_sin" )"1" "1" expand "deriv" "1" replace "1" "1" expand "const_fun" )"1" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" )"2" (assert ) nil )))))))))))"3" (propax) nil )))"2" (hide 2)"2" (lemma "sum_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (expand "derivable?" -2)"1" (expand "derivable?" -3)"1" (inst?)"1" "1" (assert ) nil )))))))))))))))"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" )"2" (assert ) nil )))))))))))))"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" (inst?)"1" (assert ) nil )))))))))))))))"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil )))))))))))))"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (inst?) (("1" (assert ) nil )))))))))))"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" )"2" (assert ) nil ))))))))))))))))))nil )nil nil )nil 3445341423";;; Proof sin2_cos2-1 for formula trig_props.sin2_cos2" expand "const_fun" )";;; Proof sin2_cos2-1 for formula trig_props.sin2_cos2" "cos_derivable" )";;; Proof sin2_cos2-1 for formula trig_props.sin2_cos2" "sin_derivable" )";;; Proof sin2_cos2-1 for formula trig_props.sin2_cos2" case "derivable?[real](cos * cos)" )"1" (case "derivable?[real](sin * sin)" )"1" "derivable[real](sin * sin + cos * cos)" )"1" (case "deriv(sin*sin+cos*cos) = const_fun(0)" )"1" (lemma "null_derivative[real]" )"1" (inst -1 "sin*sin+cos*cos" )"1" (flatten)"1" (hide -1)"1" (split -1)"1" (hide -2)"1" (hide -2)"1" case "(sin * sin + cos * cos)(0) = 1" )"1" expand "constant?" )"1" "1" "x!1" "0" )"1" replace -1)"1" (propax) nil )))))))))"2" "2" "sin_0" )"2" "cos_0" )"2" expand "+ " )"2" expand "*" )"2" assert )nil )))))))))))))))))"2" (skosimp*)"2" (hide 2)"2" case "deriv(sin * sin + cos * cos)(x!1) = const_fun(0)(x!1)" )"1" "1" expand "deriv" -1)"1" replace -1)"1" expand "const_fun" )"1" (propax) nil )))))))))"2" replace -1)"2" (propax) nil )))))))))))))))))"2" (hide -1 2)"2" (skosimp*)"2" (inst + "x!1+1" )"2" (assert ) nil )))))))))"2" (hide 2)"2" (lemma "deriv_sum[real]" )"1" (apply-extensionality 1 :hide? t)"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" "1" assert )"1" expand "deriv" 1)"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "sin" "sin" "x!1" )"1" assert )"1" expand "derivable?" "1" expand "derivable" "1" "1" "1" assert )"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "cos" "cos" "x!1" )"1" assert )"1" replace "1" "1" "deriv_cos" )"1" "1" expand "deriv" "1" replace "1" "1" "deriv_sin" )"1" "1" expand "deriv" "1" replace "1" "1" expand "const_fun" )"1" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" )"2" (assert ) nil )))))))))))"3" (propax) nil )))"2" (hide 2)"2" (lemma "sum_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (expand "derivable?" -2)"1" (expand "derivable?" -3)"1" (inst?)"1" "1" (assert ) nil )))))))))))))))"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" )"2" (assert ) nil )))))))))))))"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" (inst?)"1" (assert ) nil )))))))))))))))"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil )))))))))))))"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (inst?) (("1" (assert ) nil )))))))))))"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" )"2" (assert ) nil ))))))))))))))))))";;; developed with shostak decision procedures") nil nil )nil 3249311628"" (expand "const_fun" )"" (lemma "cos_derivable" )"" (lemma "sin_derivable" )"" (case "derivable[real](cos * cos)" )"1" (case "derivable[real](sin * sin)" )"1" "derivable[real](sin * sin + cos * cos)" )"1" (case "deriv(sin*sin+cos*cos) = const_fun(0)" )"1" (lemma "null_derivative[real]" )"1" (inst -1 "sin*sin+cos*cos" )"1" (flatten)"1" (hide -1)"1" (split -1)"1" (hide -2)"1" (hide -2)"1" case "(sin * sin + cos * cos)(0) = 1" )"1" expand "constant?" )"1" "1" "x!1" "0" )"1" replace -1)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" "sin_0" )"2" "cos_0" )"2" expand "+ " )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide 2)"2" case "deriv(sin * sin + cos * cos)(x!1) = const_fun(0)(x!1)" )"1" "1" expand "deriv" -1)"1" replace -1)"1" expand "const_fun" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "deriv_sum[real]" )"1" (apply-extensionality 1 :hide? t)"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" "1" assert )"1" expand "deriv" 1)"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "sin" "sin" "x!1" )"1" assert )"1" expand "derivable?" "1" expand "derivable" "1" "1" "1" assert )"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "cos" "cos" "x!1" )"1" assert )"1" replace "1" "1" "deriv_cos" )"1" "1" expand "deriv" "1" replace "1" "1" "deriv_sin" )"1" "1" expand "deriv" "1" replace "1" "1" expand "const_fun" )"1" 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 )"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide 2)"2" (lemma "sum_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst -1 "sin*sin" "cos*cos" "x!1" )"1" (expand "derivable?" -2)"1" (expand "derivable?" -3)"1" (inst?)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_fun nil )nil derivatives_def "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives_def "analysis/" )nil derivatives_def "analysis/" )nil derivative_props "analysis/" )nil trig_fun nil )nil trig_fun nil )"bool" real_fun_preds "reals/" )nil derivatives "analysis/" )"[T -> real]" derivatives "analysis/" )nil derivatives_def "analysis/" )"real" trig_fun nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3445341870"" (skosimp*)"" (lemma "cos_derivable" )"" (lemma "sin_derivable" )"" (case "derivable?[real](cos * cos)" )"1" (case "derivable?[real](sin * sin)" )"1" "derivable?[real](sin * sin + cos * cos)" )"1" (case "deriv(sin*sin+cos*cos) = const_fun(0)" )"1" (lemma "null_derivative[real]" )"1" (inst -1 "sin*sin+cos*cos" )"1" (flatten)"1" (hide -1)"1" (split -1)"1" (hide -2)"1" case "(sin * sin + cos * cos)(0) = 1" )"1" expand "constant?" )"1" "x!1" "0" )"1" replace -1)"1" assert )"1" "1" expand "*" )"1" assert )"1" expand "+" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sin_0" )"2" "cos_0" )"2" expand "+ " )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide 2)"2" "deriv(sin * sin + cos * cos)(x!2) = const_fun(0)(x!2)" )"1" "1" expand "deriv" -1)"1" replace -1)"1" expand "const_fun" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "connected?" ) (("3" (propax) nil nil ))nil ))nil )"2" (hide 2)"2" (lemma "deriv_sum[real]" )"1" (apply-extensionality 1 :hide? t)"1" (inst -1 "sin*sin" "cos*cos" "x!2" )"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" "1" assert )"1" expand "deriv" 1)"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "sin" "sin" "x!2" )"1" assert )"1" expand "derivable?" "1" expand "derivable?" "1" "1" "1" assert )"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "cos" "cos" "x!2" )"1" assert )"1" replace "1" "1" "deriv_cos" )"1" "1" expand "deriv" "1" replace "1" "1" "deriv_sin" )"1" "1" expand "deriv" "1" replace "1" "1" expand "const_fun" )"1" 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 )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!2+1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide 2)"2" (lemma "sum_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst -1 "sin*sin" "cos*cos" "x!2" )"1" (expand "derivable?" -2)"1" (expand "derivable?" -3)"1" (inst?)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "deriv_domain_real" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_props nil )"real" trig_fun nil )"[T -> real]" real_fun_ops "reals/" )"bool" derivatives "analysis/" )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil derivatives_def "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil deriv_domain "analysis/" )nil derivatives_def "analysis/" )nil trig_props nil )"real" reals nil )nil trig_props nil )"bool" deriv_domain_def "analysis/" )nil derivatives_def "analysis/" )nil derivative_props "analysis/" )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"real" reals nil )"real" reals nil )"bool" real_fun_preds "reals/" )nil trig_fun nil )nil trig_fun nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"deriv_fun" derivatives"analysis/" )"(convergent?)" "analysis/" )"[T, T -> boolean]" equalities nil )nil derivatives "analysis/" )"[T -> real]" derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives_def "analysis/" )"real" trig_fun nil )nil trig_props nil ))nil )nil 3249311628"" (skosimp*)"" (lemma "cos_derivable" )"" (lemma "sin_derivable" )"" (case "derivable[real](cos * cos)" )"1" (case "derivable[real](sin * sin)" )"1" "derivable[real](sin * sin + cos * cos)" )"1" (case "deriv(sin*sin+cos*cos) = const_fun(0)" )"1" (lemma "null_derivative[real]" )"1" (inst -1 "sin*sin+cos*cos" )"1" (flatten)"1" (hide -1)"1" (split -1)"1" (hide -2)"1" case "(sin * sin + cos * cos)(0) = 1" )"1" expand "constant?" )"1" "x!1" "0" )"1" replace -1)"1" assert )"1" "1" expand "*" )"1" assert )"1" expand "+" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sin_0" )"2" "cos_0" )"2" expand "+ " )"2" expand "*" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide 2)"2" "deriv(sin * sin + cos * cos)(x!2) = const_fun(0)(x!2)" )"1" "1" expand "deriv" -1)"1" replace -1)"1" expand "const_fun" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst 1 "x!2+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "deriv_sum[real]" )"1" (apply-extensionality 1 :hide? t)"1" (inst -1 "sin*sin" "cos*cos" "x!2" )"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" "1" assert )"1" expand "deriv" 1)"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "sin" "sin" "x!2" )"1" assert )"1" expand "derivable?" "1" expand "derivable" "1" "1" "1" assert )"1" replace -1)"1" "1" "deriv_prod[real]" )"1" "cos" "cos" "x!2" )"1" assert )"1" replace "1" "1" "deriv_cos" )"1" "1" expand "deriv" "1" replace "1" "1" "deriv_sin" )"1" "1" expand "deriv" "1" replace "1" "1" expand "const_fun" )"1" 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 )"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide 2)"2" (lemma "sum_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst -1 "sin*sin" "cos*cos" "x!2" )"1" (expand "derivable?" -2)"1" (expand "derivable?" -3)"1" (inst?)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (expand "derivable?" -4)"1" (inst?)"1" (inst?) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "prod_derivable[real]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" (inst?)"1" (expand "derivable?" -3)"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst-cp + "0" )"2" (inst + "1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_fun nil )nil derivatives_def "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives_def "analysis/" )nil derivatives_def "analysis/" )nil derivative_props "analysis/" )"bool" real_fun_preds "reals/" )nil trig_fun nil )nil trig_fun nil )nil derivatives "analysis/" )"[T -> real]" derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives_def "analysis/" )"real" trig_fun nil ))nil ))nil 3249311628"" (skosimp*)"" (lemma "sin_cos_one" )"" (inst?)"" (case "sin(x!1) * sin(x!1) <= 1" )"1" (hide -2)"1" (lemma "sqrt_1_le" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (assert )"2" (hide 2)"2" (case "cos(x!1) * cos(x!1) >= 0" )"1" (assert ) nil nil )"2" (hide -1 2)"2" (assert )"2" (rewrite "abs_square" :dir rl)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_props nil )"real" trig_fun nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil booleans nil )nil real_props nil )"(total_order?[real])" nil )nil real_props nil )"(total_order?[real])" nil )"real" trig_fun nil )"bool" reals nil )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.158Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-05)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
