(vect_chain_rulenil 3472221152"" (lemma "deriv_domain1" )"" (expand "deriv_domain?" ) (("" (propax) nil nil )) nil )) nil )nil vect_chain_rule nil )) nil ))nil 3472221152"" (lemma "not_one_element1" ) (("" (propax) nil nil )) nil )nil vect_chain_rule nil )) nil ))nil 3472221152"" (lemma "deriv_domain2" ) (("" (skosimp*) nil nil )) nil )nil vect_chain_rule nil )) nil ))nil 3472221152"" (skosimp*)"" (lemma "not_one_element2" )"" (expand "not_one_element?" ) (("" (inst?) nil nil )) nil ))nil ))nil )nil vect_chain_rule nil )) nil ))nil 3472381455"" (skosimp*)"" (expand "derivable_rv?" )"" (flatten)"" (split +)"1" (hide -3)"1" (lemma "composition_derivable[T1,T2]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" "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" "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" "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" "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 )"bool" deriv_real_vect2 nil )nil vect_chain_rule nil )"[real -> boolean]" vect_chain_rule nil )nil vect_chain_rule nil )"[real -> boolean]" vect_chain_rule nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil chain_rule "analysis/" )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil booleans nil )"T3" function_props nil )nil vectors_2D_def "vectors/" )"bool" derivatives "analysis/" )nil vect_chain_rule nil )nil vect_chain_rule nil )nil vect_chain_rule nil )nil vect_chain_rule nil ))nil )nil 3472221158"" (skosimp*)"" (expand "differentiable_rv?" )"" (flatten)"" (split +)"1" (hide -3)"1" (lemma "composition_derivable[T1,T2]" )"1" (expand "derivable?" 1)"1" (skosimp*)"1" "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" "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" "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" "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 )nil chain_rule "analysis/" )nil vectors_2D_def "vectors/" )"bool" derivatives "analysis/" ))nil ))nil 3313840193"" (lemma "deriv_domain2" ) (("" (propax) nil nil )) nil )nil vect_chain_rule nil )) nil ))nil 3313840193"" (lemma "not_one_element2" ) (("" (propax) nil nil )) nil )nil vect_chain_rule nil )) nil ))nil 3472221178"" (skosimp*)"" (lemma "composition_derivable_vfun" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil vect_chain_rule nil )"bool" deriv_real_vect2 nil )nil vectors_2D_def "vectors/" )"bool" derivatives "analysis/" )nil booleans nil )nil vect_chain_rule nil )"[real -> boolean]" vect_chain_rule nil )nil vect_chain_rule nil )"[real -> boolean]" vect_chain_rule nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))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" "1" expand "o " )"1" replace -1)"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" expand "derivable?" -2)"2" (inst?) nil nil ))nil ))nil )"3" "3" expand "derivable_rv?" )"3" "3" expand "derivable?" -)"3" "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" "1" expand "o " )"1" replace -1)"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" expand "derivable?" -2)"2" (inst?) nil nil ))nil ))nil )"3" "3" expand "derivable_rv?" )"3" "3" expand "derivable?" -)"3" "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 )"[T -> Vect2]" vect_fun_ops_rv nil )"[T -> real]" derivatives "analysis/" )"[T -> Vect2]" deriv_real_vect2 nil )nil chain_rule "analysis/" )"real" reals nil )nil vect_chain_rule nil )nil vect_chain_rule nil )nil vect_chain_rule nil )nil vect_chain_rule nil )"bool" derivatives_def "analysis/" )"{f | derivable?(f)}" vect_chain_rule nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"Vect2" deriv_real_vect2 nil )"T3" function_props nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" derivatives_def "analysis/" )nil vect_chain_rule nil )"bool" deriv_real_vect2 nil )nil vectors_2D_def "vectors/" )nil vect_chain_rule nil )"[real -> boolean]" vect_chain_rule nil )"bool" derivatives "analysis/" )nil vect_chain_rule nil )"[real -> boolean]" vect_chain_rule nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil )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" "1" expand "o " )"1" replace -1)"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" expand "derivable?" -2)"2" (inst?) nil nil ))nil ))nil )"3" "3" expand "differentiable_rv?" )"3" "3" expand "derivable?" -)"3" "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" "1" expand "o " )"1" replace -1)"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" expand "derivable?" -2)"2" (inst?) nil nil ))nil ))nil )"3" "3" expand "differentiable_rv?" )"3" "3" expand "derivable?" -)"3" "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 )"[T -> real]" derivatives "analysis/" )nil chain_rule "analysis/" )"bool" derivatives_def "analysis/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" derivatives_def "analysis/" )nil vectors_2D_def "vectors/" )"bool" derivatives "analysis/" ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.28 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
