|
(restrict2_deriv
(deriv_domain_T1 0
(deriv_domain_T1-1 nil 3472400421
(";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(expand "deriv_domain?")
((";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(skosimp*)
((";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(lemma "connected_domain")
((";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(lemma "connected_deriv_domain[T1]")
((";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(replace -2)
((";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(lemma not_one_element)
((";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(replace -1)
((";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(hide -1)
((";;; Proof deriv_domain-2 for formula taylors.deriv_domain"
(inst?) nil))))))))))))))))
";;; developed with shostak decision procedures")
nil nil))
(f_TCC1 0
(f_TCC1-2 nil 3471602995
("" (lemma "deriv_domain_T2") (("" (propax) nil nil)) nil)
((deriv_domain_T2 formula-decl nil restrict2_deriv nil)) nil)
(f_TCC1-1 nil 3267250906
("" (lemma "deriv_domain2") (("" (propax) nil nil)) nil) nil nil))
(f_TCC2 0
(f_TCC2-1 nil 3267250906
("" (lemma "not_one_element_T2") (("" (propax) nil nil)) nil)
((not_one_element_T2 formula-decl nil restrict2_deriv nil)) nil))
(sub_dom 0
(sub_dom-1 nil 3267250906
("" (lemma "sub_domain") (("" (grind) nil nil)) nil)
((T2 formal-subtype-decl nil restrict2_deriv nil)
(T2_pred const-decl "[real -> boolean]" restrict2_deriv nil)
(T1 formal-subtype-decl nil restrict2_deriv nil)
(T1_pred const-decl "[real -> boolean]" restrict2_deriv 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sub_domain formula-decl nil restrict2_deriv nil))
nil))
(restrict2_derivable_TCC1 0
(restrict2_derivable_TCC1-1 nil 3267250906
("" (lemma "deriv_domain_T1") (("" (propax) nil nil)) nil)
((deriv_domain_T1 formula-decl nil restrict2_deriv nil)) nil))
(restrict2_derivable_TCC2 0
(restrict2_derivable_TCC2-1 nil 3267250906
("" (lemma "not_one_element_T1") (("" (propax) nil nil)) nil)
((not_one_element_T1 formula-decl nil restrict2_deriv nil)) nil))
(restrict2_derivable 0
(restrict2_derivable-1 nil 3267250906
("" (skosimp*)
(("" (typepred "f!1")
(("" (expand "derivable?")
(("" (skosimp*)
(("" (expand "restrict2")
(("" (inst?)
(("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (inst + "l!1")
(("" (expand "convergence")
(("" (expand "NQ")
(("" (expand "convergence")
(("" (prop)
(("1"
(rewrite "deriv_TCC")
(("1"
(lemma "not_one_element_T1")
(("1"
(expand "not_one_element?")
(("1" (propax) nil nil))
nil))
nil)
("2"
(lemma "deriv_domain_T1")
(("2"
(expand "deriv_domain?")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst - "epsilon!1")
(("2"
(skosimp*)
(("2"
(inst + "delta!1")
(("2"
(skosimp*)
(("2"
(inst?)
(("1" (assert) nil nil)
("2"
(hide 2)
(("2"
(expand "A")
(("2"
(expand "adh")
(("2"
(typepred "x!2")
(("2"
(expand "A")
(("2"
(assert)
(("2"
(typepred
"x!1")
(("2"
(lemma
"sub_dom")
(("2"
(inst?)
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)
((deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(T2 formal-subtype-decl nil restrict2_deriv nil)
(T2_pred const-decl "[real -> boolean]" restrict2_deriv 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-subtype-decl nil restrict2_deriv nil)
(T1_pred const-decl "[real -> boolean]" restrict2_deriv nil)
(convergent? const-decl "bool" lim_of_functions nil)
(NQ const-decl "real" derivatives_def nil)
(deriv_domain_T1 formula-decl nil restrict2_deriv nil)
(not_one_element_T1 formula-decl nil restrict2_deriv nil)
(deriv_TCC formula-decl nil derivatives_def nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(not_one_element? 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 "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(x!1 skolem-const-decl "T1" restrict2_deriv nil)
(x!2 skolem-const-decl "(A(x!1))" restrict2_deriv 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sub_dom judgement-tcc nil restrict2_deriv nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(adh const-decl "setof[real]" convergence_functions nil)
(convergence const-decl "bool" convergence_functions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" lim_of_functions nil)
(derivable? const-decl "bool" derivatives_def nil)
(restrict2 const-decl "[T1 -> real]" restrict2_deriv nil))
nil))
(restrict2_deriv_TCC1 0
(restrict2_deriv_TCC1-1 nil 3267250906
("" (lemma "restrict2_derivable") (("" (propax) nil nil)) nil)
((restrict2_derivable formula-decl nil restrict2_deriv nil)) nil))
(restrict2_deriv 0
(restrict2_deriv-1 nil 3267250906
("" (skosimp*)
(("" (typepred "f!1")
(("" (lemma "restrict2_derivable" ("f" "f!1"))
((""
(lemma "deriv_comp_fun[T1,T2]"
("ff" "LAMBDA (x:T1): x" "gg" "f!1"))
(("1" (lemma "identity_derivable_fun[T1]")
(("1" (lemma "deriv_id_fun[T1]")
(("1" (expand "I")
(("1" (replace -1)
(("1" (expand "o")
(("1" (expand "*")
(("1" (expand "restrict2")
(("1" (expand "deriv" 1)
(("1" (hide -1 -2)
(("1"
(lemma "extensionality_postulate"
("f"
"deriv(LAMBDA (x_1: T1): f!1(x_1))"
"g"
"(LAMBDA (x_1: T1): deriv(f!1)(x_1))"))
(("1"
(flatten -1)
(("1"
(hide -1)
(("1"
(split -1)
(("1"
(inst - "a!1")
(("1"
(expand "deriv" -1)
(("1"
(replace -1 1)
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "identity_derivable_fun[T1]")
(("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)
("3" (hide-all-but 1)
(("3" (lemma "not_one_element_T2")
(("3" (expand "not_one_element?")
(("3" (propax) nil nil)) nil))
nil))
nil)
("4" (lemma "deriv_domain_T2") (("4" (propax) nil nil)) nil)
("5" (lemma "not_one_element_T1")
(("5" (expand "not_one_element?") (("5" (propax) nil nil))
nil))
nil)
("6" (lemma "deriv_domain_T1") (("6" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(T2 formal-subtype-decl nil restrict2_deriv nil)
(T2_pred const-decl "[real -> boolean]" restrict2_deriv 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-subtype-decl nil restrict2_deriv nil)
(T1_pred const-decl "[real -> boolean]" restrict2_deriv nil)
(deriv_comp_fun formula-decl nil chain_rule nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(deriv_id_fun formula-decl nil derivatives nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv const-decl "[T -> real]" derivatives nil)
(extensionality_postulate formula-decl nil functions nil)
(restrict2 const-decl "[T1 -> real]" restrict2_deriv nil)
(O const-decl "T3" function_props nil)
(I const-decl "(bijective?[T, T])" identity nil)
(identity_derivable_fun formula-decl nil derivatives nil)
(not_one_element_T2 formula-decl nil restrict2_deriv nil)
(deriv_domain_T2 formula-decl nil restrict2_deriv nil)
(not_one_element_T1 formula-decl nil restrict2_deriv nil)
(deriv_domain_T1 formula-decl nil restrict2_deriv nil)
(restrict2_derivable formula-decl nil restrict2_deriv nil))
nil)))
¤ Dauer der Verarbeitung: 0.20 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.
|
