|
(deriv_sign
(IMP_derivatives_TCC1 0
(IMP_derivatives_TCC1-1 nil 3471617303
("" (lemma "deriv_domain_nzreal") (("" (propax) nil nil)) nil)
((deriv_domain_nzreal formula-decl nil deriv_domain nil)) nil))
(IMP_derivatives_TCC2 0
(IMP_derivatives_TCC2-1 nil 3471617303
("" (expand "not_one_element?")
(("" (skosimp*) (("" (inst + "x!1/2") (("" (assert) nil nil)) nil))
nil))
nil)
((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(not_one_element? const-decl "bool" deriv_domain_def nil))
nil))
(sign_derivable 0
(sign_derivable-1 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"
(skosimp*)
(("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)
((derivable? const-decl "bool" derivatives_def 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)
(fullset const-decl "set" sets nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(e!1 skolem-const-decl "posreal" deriv_sign nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(x!1 skolem-const-decl "nzreal" deriv_sign nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(adh const-decl "setof[real]" convergence_functions nil)
(sign const-decl "Sign" sign "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(restrict const-decl "R" restrict nil)
(NQ const-decl "real" derivatives_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(convergence const-decl "bool" convergence_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil))
shostak))
(sign_derivable_fun 0
(sign_derivable_fun-1 nil 3471617730
("" (expand "derivable?")
(("" (skosimp*)
(("" (lemma "sign_derivable") (("" (inst?) nil nil)) nil)) nil))
nil)
((nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sign_derivable formula-decl nil deriv_sign nil)
(derivable? const-decl "bool" derivatives nil))
shostak))
(deriv_sign_TCC1 0
(deriv_sign_TCC1-1 nil 3472228554
("" (lemma "sign_derivable_fun") (("" (propax) nil nil)) nil)
((sign_derivable_fun formula-decl nil deriv_sign nil)) nil))
(deriv_sign 0
(deriv_sign-1 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"
(lemma "deriv_domain_nzreal")
(("1"
(expand "deriv_domain?")
(("1"
(skosimp*)
(("1"
(inst - e!1 x!1)
(("1"
(skosimp*)
(("1"
(inst?)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2"
(inst + "min(epsilon!1,abs(x!1/2))")
(("2"
(skosimp*)
(("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)
((deriv const-decl "[T -> real]" derivatives nil)
(sign_derivable formula-decl nil deriv_sign nil)
(fullset const-decl "set" sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_functions nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(adh const-decl "setof[real]" convergence_functions nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(x!1 skolem-const-decl "nzreal" deriv_sign nil)
(y!1 skolem-const-decl "{u: nzreal | u + x!1 /= 0}" deriv_sign nil)
(deriv_domain_nzreal formula-decl nil deriv_domain nil)
(NQ const-decl "real" derivatives_def nil)
(convergence const-decl "bool" lim_of_functions nil)
(deriv_def formula-decl nil derivatives_def nil)
(derivable_const application-judgement "deriv_fun" deriv_sign nil)
(sign const-decl "Sign" sign "reals/")
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers 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)
(derivable? const-decl "bool" derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(deriv const-decl "real" derivatives_def nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(restrict const-decl "R" restrict nil))
shostak)))
¤ Dauer der Verarbeitung: 0.19 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.
|
