| products/sources/formale sprachen/PVS/vect_analysis/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: vect_chain_rule.prf Sprache: Unknown
|
(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.82 Sekunden (vorverarbeitet) ] |