(deriv_signnil 3471617303"" (lemma "deriv_domain_nzreal" ) (("" (propax) nil nil )) nil )nil deriv_domain nil )) nil ))nil 3471617303"" (expand "not_one_element?" )"" (skosimp*) (("" (inst + "x!1/2" ) (("" (assert ) nil nil )) nil ))nil ))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 )"nzreal" nil )"bool" deriv_domain_def nil ))nil ))nil 3471093961"" (skosimp*)"" (expand "derivable?" )"" (expand "convergent?" )"" (inst + "0" )"" (expand "convergence" )"" (expand "fullset" )"" (expand "convergence" )"" (prop)"1" (expand "adh" )"1" (skosimp*)"1" (case "x!1 > 0" )"1" (inst + "e!1/2" )"1" (grind) nil nil ) ("2" (grind) nil nil ))nil )"2" (inst + "-e!1/2" )"1" (grind) nil nil ) ("2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (case "x!1 > 0" )"1" (expand "NQ" )"1" (expand "sign" )"1" (assert )"1" (inst + "x!1/2" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "-x!1/2" )"1" (skosimp*) (("1" (grind) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" derivatives_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"set" sets nil )"nzreal" real_typesnil )"nzreal" nil )"[numfield -> numfield]" number_fields nil )"posreal" nil )"posreal" deriv_sign nil )nil real_types nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"nzreal" deriv_sign nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"{y: posreal | y >= x}" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )nil reals nil )"boolean" notequal nil )"bool" reals nil )nil booleans nil )"setof[real]" convergence_functions nil )"Sign" sign "reals/" )"(total_order?[real])" nil )"even_int" integersnil )"odd_int" integers nil )"R" restrict nil )"real" derivatives_def nil )"real" reals nil )"int" integers nil )"even_int" integersnil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" convergence_functions nil )"real" reals nil )"bool" lim_of_functions nil )"bool" lim_of_functions nil ))nil 3471617730"" (expand "derivable?" )"" (skosimp*)"" (lemma "sign_derivable" ) (("" (inst?) nil nil )) nil )) nil ))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 )nil deriv_sign nil )"bool" derivatives nil ))nil 3472228554"" (lemma "sign_derivable_fun" ) (("" (propax) nil nil )) nil )nil deriv_sign nil )) nil ))nil 3472228558"" (expand "restrict" )"" (expand "deriv" )"" (apply-extensionality 1 :hide? t)"1" (expand "const_fun" )"1" (lemma "deriv_def" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (expand "convergence" )"1" (expand "fullset" )"1" (expand "NQ" )"1" (expand "convergence" )"1" (split +)"1" (expand "adh" )"1" "deriv_domain_nzreal" )"1" expand "deriv_domain?" )"1" "1" "1" "1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "min(epsilon!1,abs(x!1/2))" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "sign_derivable" )"2" (inst?)"2" (expand "restrict" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> real]" derivatives nil )nil deriv_sign nil )"set" sets nil )"real" reals nil )"int" integers nil )"real" reals nil )"bool" convergence_functions nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{y: posreal | y >= x}" nil )"nzreal" real_typesnil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(total_order?[real])" nil )"even_int" integersnil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nzreal" nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )"setof[real]" convergence_functions nil )"real" reals nil )"bool" deriv_domain_def nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"setof[nzreal]" derivatives_def nil )nil defined_types nil )"nzreal" deriv_sign nil )"{u: nzreal | u + x!1 /= 0}" deriv_sign nil )nil deriv_domain nil )"real" derivatives_def nil )"bool" lim_of_functions nil )nil derivatives_def nil )"deriv_fun" deriv_sign nil )"Sign" sign "reals/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" derivatives_def nil )nil booleans nil )"real" derivatives_def nil )"[T -> real]" real_fun_ops "reals/" )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 )"R" restrict nil ))quality 100%
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
