|
(vect_chain_rule
(composition_derivable_vfun_TCC1 0
(composition_derivable_vfun_TCC1-1 nil 3472221152
("" (lemma "deriv_domain1")
(("" (expand "deriv_domain?") (("" (propax) nil nil)) nil)) nil)
((deriv_domain1 formula-decl nil vect_chain_rule nil)) nil))
(composition_derivable_vfun_TCC2 0
(composition_derivable_vfun_TCC2-1 nil 3472221152
("" (lemma "not_one_element1") (("" (propax) nil nil)) nil)
((not_one_element1 formula-decl nil vect_chain_rule nil)) nil))
(composition_derivable_vfun_TCC3 0
(composition_derivable_vfun_TCC3-1 nil 3472221152
("" (lemma "deriv_domain2") (("" (skosimp*) nil nil)) nil)
((deriv_domain2 formula-decl nil vect_chain_rule nil)) nil))
(composition_derivable_vfun_TCC4 0
(composition_derivable_vfun_TCC4-1 nil 3472221152
("" (skosimp*)
(("" (lemma "not_one_element2")
(("" (expand "not_one_element?") (("" (inst?) nil nil)) nil))
nil))
nil)
((not_one_element2 formula-decl nil vect_chain_rule nil)) nil))
(composition_derivable_vfun 0
(composition_derivable_vfun-2 nil 3472381455
("" (skosimp*)
(("" (expand "derivable_rv?")
(("" (flatten)
(("" (split +)
(("1" (hide -3)
(("1" (lemma "composition_derivable[T1,T2]")
(("1" (expand "derivable?" 1)
(("1" (skosimp*)
(("1"
(inst - "f!1" "(LAMBDA (a: T2): g!1(a)`x)" "x!1")
(("1" (expand "o ")
(("1" (assert)
(("1" (hide 2)
(("1" (expand derivable? -)
(("1" (inst?)
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element2") (("2" (propax) nil nil))
nil)
("3" (lemma "deriv_domain2")
(("3" (expand "deriv_domain?") (("3" (propax) nil nil))
nil))
nil)
("4" (lemma "not_one_element1") (("4" (propax) nil nil))
nil)
("5" (lemma "deriv_domain1")
(("5" (expand "deriv_domain?") (("5" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide -2)
(("2" (lemma "composition_derivable[T1,T2]")
(("1" (expand "derivable?" 1)
(("1" (skosimp*)
(("1"
(inst - "f!1" "(LAMBDA (a: T2): g!1(a)`y)" "x!1")
(("1" (expand "o ")
(("1" (assert)
(("1" (hide 2)
(("1" (expand derivable? -)
(("1" (inst?)
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element2") (("2" (propax) nil nil))
nil)
("3" (lemma "deriv_domain2")
(("3" (expand "deriv_domain?") (("3" (propax) nil nil))
nil))
nil)
("4" (lemma "not_one_element1") (("4" (propax) nil nil))
nil)
("5" (lemma "deriv_domain1")
(("5" (expand "deriv_domain?") (("5" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(T2 formal-subtype-decl nil vect_chain_rule nil)
(T2_pred const-decl "[real -> boolean]" vect_chain_rule nil)
(T1 formal-subtype-decl nil vect_chain_rule nil)
(T1_pred const-decl "[real -> boolean]" vect_chain_rule 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)
(composition_derivable formula-decl nil chain_rule "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(O const-decl "T3" function_props nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(derivable? const-decl "bool" derivatives "analysis/")
(not_one_element2 formula-decl nil vect_chain_rule nil)
(deriv_domain2 formula-decl nil vect_chain_rule nil)
(not_one_element1 formula-decl nil vect_chain_rule nil)
(deriv_domain1 formula-decl nil vect_chain_rule nil))
nil)
(composition_derivable_vfun-1 nil 3472221158
("" (skosimp*)
(("" (expand "differentiable_rv?")
(("" (flatten)
(("" (split +)
(("1" (hide -3)
(("1" (lemma "composition_derivable[T1,T2]")
(("1" (expand "derivable?" 1)
(("1" (skosimp*)
(("1"
(inst - "f!1" "(LAMBDA (a: T2): g!1(a)`x)" "x!1")
(("1" (expand "o ")
(("1" (assert)
(("1" (hide 2)
(("1" (expand derivable? -)
(("1" (inst?)
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element2") (("2" (propax) nil nil))
nil)
("3" (lemma "deriv_domain2") (("3" (propax) nil nil))
nil)
("4" (lemma "not_one_element1") (("4" (propax) nil nil))
nil)
("5" (lemma "deriv_domain1") (("5" (propax) nil nil))
nil))
nil))
nil)
("2" (hide -2)
(("2" (lemma "composition_derivable[T1,T2]")
(("1" (expand "derivable?" 1)
(("1" (skosimp*)
(("1"
(inst - "f!1" "(LAMBDA (a: T2): g!1(a)`y)" "x!1")
(("1" (expand "o ")
(("1" (assert)
(("1" (hide 2)
(("1" (expand derivable? -)
(("1" (inst?)
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element2") (("2" (propax) nil nil))
nil)
("3" (lemma "deriv_domain2") (("3" (propax) nil nil))
nil)
("4" (lemma "not_one_element1") (("4" (propax) nil nil))
nil)
("5" (lemma "deriv_domain1") (("5" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((composition_derivable formula-decl nil chain_rule "analysis/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(derivable? const-decl "bool" derivatives "analysis/"))
nil))
(gg_TCC1 0
(gg_TCC1-1 nil 3313840193
("" (lemma "deriv_domain2") (("" (propax) nil nil)) nil)
((deriv_domain2 formula-decl nil vect_chain_rule nil)) nil))
(gg_TCC2 0
(gg_TCC2-1 nil 3313840193
("" (lemma "not_one_element2") (("" (propax) nil nil)) nil)
((not_one_element2 formula-decl nil vect_chain_rule nil)) nil))
(deriv_comp_vfun_TCC1 0
(deriv_comp_vfun_TCC1-1 nil 3472221178
("" (skosimp*)
(("" (lemma "composition_derivable_vfun")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((composition_derivable_vfun formula-decl nil vect_chain_rule nil)
(derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(derivable? const-decl "bool" derivatives "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-subtype-decl nil vect_chain_rule nil)
(T2_pred const-decl "[real -> boolean]" vect_chain_rule nil)
(T1 formal-subtype-decl nil vect_chain_rule nil)
(T1_pred const-decl "[real -> boolean]" vect_chain_rule 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))
nil))
(deriv_comp_vfun 0
(deriv_comp_vfun-2 nil 3472381511
("" (skolem-typepred)
(("" (expand "*" 1)
(("" (lemma "composition_derivable_vfun")
(("" (inst?)
(("" (assert)
(("" (expand "deriv")
(("" (apply-extensionality 1 :hide? t)
(("1" (expand "deriv_rv")
(("1" (expand "o ")
(("1" (expand "*")
(("1" (split +)
(("1" (lemma "deriv_composition[T1,T2]")
(("1" (inst?)
(("1" (assert)
(("1"
(split -1)
(("1"
(expand "o ")
(("1"
(replace -1)
(("1"
(hide -1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "derivable?" -2)
(("2" (inst?) nil nil))
nil))
nil)
("3"
(hide 2)
(("3"
(expand "derivable_rv?")
(("3"
(flatten)
(("3"
(expand "derivable?" -)
(("3"
(inst -4 "ff!1(x!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element2")
(("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain2")
(("3" (propax) nil nil)) nil)
("4" (lemma "not_one_element1")
(("4" (propax) nil nil)) nil)
("5" (lemma "deriv_domain1")
(("5" (propax) nil nil)) nil))
nil)
("2" (lemma "deriv_composition[T1,T2]")
(("1" (inst?)
(("1" (assert)
(("1"
(split -1)
(("1"
(expand "o ")
(("1"
(replace -1)
(("1"
(hide -1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "derivable?" -2)
(("2" (inst?) nil nil))
nil))
nil)
("3"
(hide 2)
(("3"
(expand "derivable_rv?")
(("3"
(flatten)
(("3"
(expand "derivable?" -)
(("3"
(inst -5 "ff!1(x!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element2")
(("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain2")
(("3" (propax) nil nil)) nil)
("4" (lemma "not_one_element1")
(("4" (propax) nil nil)) nil)
("5" (lemma "deriv_domain1")
(("5" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element1")
(("2" (skosimp*) nil nil)) nil)
("3" (skosimp*)
(("3" (lemma "deriv_domain1")
(("3" (expand "deriv_domain?")
(("3" (inst?) nil nil)) nil))
nil))
nil)
("4" (expand "derivable?" -2) (("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((* const-decl "[T -> Vect2]" vect_fun_ops_rv nil)
(deriv const-decl "[T -> real]" derivatives "analysis/")
(deriv const-decl "[T -> Vect2]" deriv_real_vect2 nil)
(deriv_composition formula-decl nil chain_rule "analysis/")
(real_times_real_is_real application-judgement "real" reals nil)
(not_one_element2 formula-decl nil vect_chain_rule nil)
(deriv_domain2 formula-decl nil vect_chain_rule nil)
(not_one_element1 formula-decl nil vect_chain_rule nil)
(deriv_domain1 formula-decl nil vect_chain_rule nil)
(derivable? const-decl "bool" derivatives_def "analysis/")
(ff!1 skolem-const-decl "{f | derivable?(f)}" vect_chain_rule nil)
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_rv const-decl "Vect2" deriv_real_vect2 nil)
(O const-decl "T3" function_props nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(deriv const-decl "real" derivatives_def "analysis/")
(composition_derivable_vfun formula-decl nil vect_chain_rule nil)
(derivable_rv? const-decl "bool" deriv_real_vect2 nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(T2 formal-subtype-decl nil vect_chain_rule nil)
(T2_pred const-decl "[real -> boolean]" vect_chain_rule nil)
(derivable? const-decl "bool" derivatives "analysis/")
(T1 formal-subtype-decl nil vect_chain_rule nil)
(T1_pred const-decl "[real -> boolean]" vect_chain_rule 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))
nil)
(deriv_comp_vfun-1 nil 3472221184
("" (skolem-typepred)
(("" (expand "*" 1)
(("" (lemma "composition_derivable_vfun")
(("" (inst?)
(("" (assert)
(("" (expand "deriv")
(("" (apply-extensionality 1 :hide? t)
(("1" (expand "deriv_rv")
(("1" (expand "o ")
(("1" (expand "*")
(("1" (split +)
(("1" (lemma "deriv_composition[T1,T2]")
(("1" (inst?)
(("1" (assert)
(("1"
(split -1)
(("1"
(expand "o ")
(("1"
(replace -1)
(("1"
(hide -1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "derivable?" -2)
(("2" (inst?) nil nil))
nil))
nil)
("3"
(hide 2)
(("3"
(expand "differentiable_rv?")
(("3"
(flatten)
(("3"
(expand "derivable?" -)
(("3"
(inst -4 "ff!1(x!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element2")
(("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain2")
(("3" (propax) nil nil)) nil)
("4" (lemma "not_one_element1")
(("4" (propax) nil nil)) nil)
("5" (lemma "deriv_domain1")
(("5" (propax) nil nil)) nil))
nil)
("2" (lemma "deriv_composition[T1,T2]")
(("1" (inst?)
(("1" (assert)
(("1"
(split -1)
(("1"
(expand "o ")
(("1"
(replace -1)
(("1"
(hide -1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "derivable?" -2)
(("2" (inst?) nil nil))
nil))
nil)
("3"
(hide 2)
(("3"
(expand "differentiable_rv?")
(("3"
(flatten)
(("3"
(expand "derivable?" -)
(("3"
(inst -5 "ff!1(x!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element2")
(("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain2")
(("3" (propax) nil nil)) nil)
("4" (lemma "not_one_element1")
(("4" (propax) nil nil)) nil)
("5" (lemma "deriv_domain1")
(("5" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element1")
(("2" (skosimp*) nil nil)) nil)
("3" (skosimp*)
(("3" (lemma "deriv_domain1") (("3" (inst?) nil nil))
nil))
nil)
("4" (expand "derivable?" -2) (("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv const-decl "[T -> real]" derivatives "analysis/")
(deriv_composition formula-decl nil chain_rule "analysis/")
(derivable? const-decl "bool" derivatives_def "analysis/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(deriv const-decl "real" derivatives_def "analysis/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(derivable? const-decl "bool" derivatives "analysis/"))
nil)))
¤ Dauer der Verarbeitung: 0.34 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.
|
