(derivatives_lamnil 3301761309"" (lemma "deriv_domain" ) (("" (propax) nil nil )) nil )nil derivatives_lam nil )) shostak))nil 3301761489"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil derivatives_lam nil )) shostak))nil 3304425174"" (expand "derivable?" )"" (lemma "derivable_id" )"" (expand "I" )"" (skeep)"" (expand "derivable?" -1) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam 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 nil )"(bijective?[T, T])" identity nil )"bool" derivatives nil ))nil 3304425582"" (skosimp*)"" (lemma "const_derivable_fun" )"" (inst?)"" (expand "const_fun" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam 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 nil ))nil 3304429143"" (skosimp :preds? t)"" (lemma "sum_derivable_fun" )"" (inst - "f!1" "g!1" )"" (expand "+ " ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil derivatives nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil ))nil 3304429240"" (skosimp*)"" (lemma "prod_derivable_fun" )"" (inst - "f!1" "g!1" )"" (expand "*" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam 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 nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )"bool" derivatives nil )nil booleans nil ))nil 3305042267 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) shostak))nil 3305042471"" (skosimp*)"" (case-replace "n!1=0" )"1" (expand "^" )"1" (expand "expt" )"1" (rewrite "derivable_const_lam" ) nil nil )) nil ))nil )"2" (lemma "deriv_x_to_n" )"2" (inst - "n!1" "1" )"1" (assert )"1" (flatten)"1" "(LAMBDA (t): t ^ n!1) = (LAMBDA (x: T): 1 * x ^ n!1)" )"1" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"real" exponentiation nil )nil derivatives_lam nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"nat" derivatives_lam nil )nil integers nil )nil integers nil )nil number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam nil )nil derivatives nil ))nil 3304699767"" (skosimp :preds? t)"" (lemma "scal_derivable_fun" )"" (inst - "a!1" "f!1" )"" (expand "*" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil derivatives nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil ))nil 3472317982"" (skosimp :preds? t)"" (lemma "scal_derivable_fun" )"" (inst - "a!1" "f!1" )"" (expand "*" )"" "(LAMBDA (x: T): a!1 * f!1(x)) = (LAMBDA (t): f!1(t) * a!1)" )"" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil ))nil ))nil ))nil )nil derivatives nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil number_fields nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil )nil 3304431294"" (skosimp :preds? t)"" (lemma "derivable_scal1_lam" )"" (inst -1 "a!1" "f!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )"bool" derivatives nil )nil derivatives nil ))nil 3442593099"" (skosimp*)"" (lemma "neg_derivable_fun" )"" (inst - "g!1" )"" (expand "-" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam 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 nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )"bool" derivatives nil )nil booleans nil ))nil )nil 3304429291"" (skosimp :preds? t)"" (expand "derivable?" )"" (lemma "derivable_opp" )"" (inst -1 "g!1" )"" (expand "-" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )nil derivatives nil )) shostak))nil 3304429323"" (skosimp :preds? t)"" (lemma "diff_derivable_fun" )"" (inst - "f!1" "g!1" )"" (expand "-" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil derivatives nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil 3304429366"" (expand "sq" )"" (rewrite "derivable_mult_lam" )"" (rewrite "derivable_id_lam" ) nil nil )) nil ))nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil )nil derivatives_lam nil )"nonneg_real" sq "reals/" )"real" reals nil ))nil 3304431982"" (skosimp :preds? t)"" (lemma "div_derivable_fun" )"" (inst - "f!1" "k!1" )"" (expand "/" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil derivatives nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil )"boolean" notequal nil )nil reals nil )nil derivatives nil ))nil 3304432031"" (skosimp :preds? t)"" (lemma "derivable_div" )"" (inst -1 "LAMBDA(t):a!1" "k!1" )"1" (expand "/" ) (("1" (propax) nil nil )) nil )"2" (lemma "derivable_const" )"2" (expand "const_fun" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil derivatives nil )nil derivatives nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )"real" derivatives_lam nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )"boolean" notequal nil )nil reals nil )nil derivatives nil ))nil 3304432497"" (skosimp)"" (lemma "derivable_scal1_lam" )"" (inst -1 "1/b!1" "f!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil derivatives_lam nil )"real" reals nil )"real" reals nil )nil derivatives nil )"bool" derivatives nil )nil booleans nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam nil )nil reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nzreal" nil ))nil 3304424118"" (rewrite "derivable_id_lam" ) nil nil )nil derivatives_lam nil )) shostak))nil 3304429116"" (expand "D" )"" (lemma "deriv_id_fun" )"" (expand "I" )"" (expand "const_fun" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil derivatives nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil ))nil 3304424144"" (skosimp) (("" (rewrite "derivable_const_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3304430079"" (skosimp)"" (expand "D" )"" (lemma "deriv_const_fun" )"" (inst -1 "a!1" )"" (expand "const_fun" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam 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 nil ))nil 3304424494"" (skosimp) (("" (rewrite "derivable_add_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil ))nil 3304430121"" (skosimp :preds? t)"" (expand * "derivable?" "D" )"" (lemma "deriv_sum_fun" )"" (inst -1 "f!1" "g!1" )"" (expand "+" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil 3304424503"" (skosimp) (("" (rewrite "derivable_mult_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil ))nil 3304430162"" (skosimp :preds? t)"" (expand * "derivable?" "D" )"" (lemma "deriv_prod_fun" )"" (inst -1 "f!1" "g!1" )"" (expand "*" )"" (expand "+" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil 3305042277 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) shostak))nil 3305042285"" (skosimp) (("" (rewrite "derivable_pow_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals 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 integers nil )"bool" reals nil )nil integers nil ))nil 3305042306 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) shostak))nil 3305042697"" (skeep)"" (expand "D" )"" (lemma "deriv_x_to_n" )"" (inst -1 "m" "1" )"" (beta) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam 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 nil )"real" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil ))nil 3304431213"" (skosimp) (("" (rewrite "derivable_scal1_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil ))nil ))nil 3304431129"" (skosimp :preds? t)"" (expand * "derivable?" "D" )"" (lemma "deriv_scal_fun" )"" (inst -1 "a!1" "f!1" )"" (expand "*" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil ))nil 3304431448"" (skosimp) (("" (rewrite "derivable_scal2_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil ))nil ))nil 3304431330"" (skosimp :preds? t)"" (lemma "deriv_scal1_lam" )"" (inst -1 "a!1" "f!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil derivatives_lam nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil 3304424526"" (skosimp) (("" (rewrite "derivable_neg_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil ))nil 3442592991"" (skosimp :preds? t)"" (expand * "derivable?" "D" )"" (lemma "deriv_neg_fun" )"" (inst -1 "g!1" )"" (expand "-" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil )nil 3304430224"" (skosimp :preds? t)"" (expand * "derivable?" "D" )"" (lemma "deriv_opp_fun" )"" (inst -1 "g!1" )"" (expand "-" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )nil derivatives nil )) shostak))nil 3304424618"" (skosimp) (("" (rewrite "derivable_sub_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil ))nil 3304430250"" (skosimp :preds? t)"" (expand * "derivable?" "D" )"" (lemma "deriv_diff_fun" )"" (inst -1 "f!1" "g!1" )"" (expand "-" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil ))nil 3304424624"" (rewrite "derivable_sq_lam" ) nil nil )nil derivatives_lam nil )) shostak))nil 3304430266"" (expand "sq" )"" (rewrite "deriv_mult_lam" )"1" (rewrite "deriv_id_lam" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "derivable_id_lam" ) nil nil ))nil ))nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil )"real" reals nil )"real" reals nil )nil derivatives_lam nil )nil derivatives_lam nil )"nonneg_real" sq "reals/" ))nil 3304431524"" (skosimp :preds? t) (("" (rewrite "derivable_div_lam" ) nil nil ))nil )nil derivatives_lam nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil )"boolean" notequal nil )nil reals nil )nil derivatives nil ))nil 3304432155"" (skosimp :preds? t)"" (expand * "derivable?" "D" )"" (lemma "deriv_div_fun" )"" (inst -1 "f!1" "k!1" )"1" (expand "/" )"1" (expand "sq" )"1" (expand "*" )"1" (assert )"1" (expand "-" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"real" reals nil )"nonneg_real" sq "reals/" )"real" reals nil )"nzreal" nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )nil derivatives nil )"boolean" notequal nil )nil reals nil )nil derivatives nil ))nil 3304431707"" (skosimp :preds? t)"" (rewrite "derivable_scald1_lam" ) nil nil )) nil )nil derivatives_lam nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )"boolean" notequal nil )nil reals nil )nil derivatives nil ))nil 3304432324"" (skosimp :preds? t)"" (expand * "derivable?" "D" )"" (lemma "deriv_scaldiv_fun" )"" (inst -1 "a!1" "k!1" )"1" (expand "/" )"1" (expand "-" )"1" (expand "*" )"1" (expand "sq" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"[T -> real]" real_fun_ops "reals/" )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil )"real" reals nil )"nzreal" nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )"bool" derivatives nil )"boolean" notequal nil )nil reals nil )nil derivatives nil ))nil 3304432644"" (skosimp) (("" (rewrite "derivable_scald2_lam" ) nil nil )) nil )nil derivatives_lam nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[real -> boolean]" derivatives_lam nil )nil derivatives_lam nil )nil booleans nil )"bool" derivatives nil )nil derivatives nil ))nil 3304432554"" (skosimp)"" (lemma "deriv_scal1_lam" )"" (inst -1 "1/b!1" "f!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil derivatives_lam nil )"real" reals nil )"real" reals nil )nil derivatives nil )"bool" derivatives nil )nil booleans nil )nil derivatives_lam nil )"[real -> boolean]" derivatives_lam nil )nil reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nzreal" nil ))quality 100%
¤ 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.0.25Bemerkung:
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
