SSL derivatives_def.prf
Sprache: unbekannt
|
|
(derivatives_def
(derivable_continuous 0
(derivable_continuous-1 nil 3253536989
("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*) (("" (forward-chain "deriv_continuous") nil nil))
nil))
nil))
nil)
nil nil))
(sum_derivable 0
(sum_derivable-1 nil 3253536989
("" (auto-rewrite "derivable?" "sum_NQ" "deriv_TCC")
(("" (skosimp)
(("" (assert)
(("" (use "sum_fun_convergent[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
nil nil))
(neg_derivable 0
(neg_derivable-1 nil 3442586144
("" (auto-rewrite "derivable?" "neg_NQ" "deriv_TCC")
(("" (skosimp)
(("" (assert)
(("" (use "neg_fun_convergent[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
nil nil))
(diff_derivable 0
(diff_derivable-1 nil 3253536989
("" (auto-rewrite "derivable?" "diff_NQ" "deriv_TCC")
(("" (skosimp)
(("" (assert)
(("" (use "diff_fun_convergent[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
nil nil))
(prod_derivable 0
(prod_derivable-1 nil 3253536989
("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (use "cnv_seq_prod_NQ")
(("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil)
nil nil))
(scal_derivable 0
(scal_derivable-1 nil 3253536989
("" (auto-rewrite "derivable?" "scal_NQ" "deriv_TCC")
(("" (skosimp)
(("" (assert)
(("" (use "scal_fun_convergent[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
nil nil))
(const_derivable 0
(const_derivable-1 nil 3253536989
("" (skolem!)
(("" (auto-rewrite "derivable?" "const_NQ" "deriv_TCC")
(("" (assert)
(("" (lemma "const_fun_convergent[(A(x!1))]")
(("" (inst - "0" "0") nil nil)) nil))
nil))
nil))
nil)
((const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil))
nil))
(inv_derivable 0
(inv_derivable-1 nil 3253536989
("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (use "cnv_seq_inv_NQ")
(("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil)
nil nil))
(div_derivable 0
(div_derivable-1 nil 3253536989
("" (skosimp)
(("" (rewrite "div_function[T]")
(("" (rewrite "prod_derivable")
(("" (rewrite "inv_derivable") nil nil)) nil))
nil))
nil)
((div_function formula-decl nil real_fun_ops "reals/")
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals 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)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(inv_derivable formula-decl nil derivatives_def nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(prod_derivable formula-decl nil derivatives_def nil))
nil))
(identity_derivable 0
(identity_derivable-1 nil 3253536989
("" (skolem!)
(("" (auto-rewrite "derivable?" "identity_NQ" "deriv_TCC")
(("" (assert)
(("" (use "const_fun_convergent[(A(x!1))]" ("b" "1" "c" "0"))
nil nil))
nil))
nil))
nil)
((id_fun_continuous name-judgement "continuous_fun"
continuous_functions nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil))
nil))
(deriv_sum_TCC1 0
(deriv_sum_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "sum_derivable") nil nil)) nil)
((sum_derivable formula-decl nil 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)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil))
nil))
(deriv_sum 0
(deriv_sum-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "sum_derivable" "derivable?" "deriv"
"sum_NQ" "lim_sum_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
nil nil))
(deriv_neg_TCC1 0
(deriv_neg_TCC1-1 nil 3442582979
("" (lemma "neg_derivable") (("" (propax) nil nil)) nil)
((neg_derivable formula-decl nil derivatives_def nil)) shostak))
(deriv_neg 0
(deriv_neg-2 nil 3442586421
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "neg_derivable" "derivable?" "deriv"
"neg_NQ" "lim_neg_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
nil nil)
(deriv_neg-1 nil 3442586370
(";;; Proof for formula derivatives_def.deriv_opposite" (skosimp)
((";;; Proof for formula derivatives_def.deriv_opposite"
(auto-rewrite "deriv_TCC" "opposite_derivable" "derivable?"
"deriv" "opposite_NQ" "lim_opposite_fun[(A(x!1))]")
((";;; Proof for formula derivatives_def.deriv_opposite" (assert)
nil))))
"")
nil nil))
(deriv_diff_TCC1 0
(deriv_diff_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "diff_derivable") nil nil)) nil)
((diff_derivable formula-decl nil 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)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil))
nil))
(deriv_diff 0
(deriv_diff-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "diff_derivable" "derivable?" "deriv"
"diff_NQ" "lim_diff_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
nil nil))
(deriv_prod_TCC1 0
(deriv_prod_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "prod_derivable") nil nil)) nil)
((prod_derivable formula-decl nil 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)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil))
nil))
(deriv_prod 0
(deriv_prod-1 nil 3253536989
("" (skosimp)
(("" (use "prod_derivable")
(("" (assert)
((""
(auto-rewrite "deriv" "deriv_TCC" "derivable?"
("lim_fun_def[(A(x!1))]"
"lim_fun_lemma[(A(x!1))]"))
(("" (assert)
((""
(use "cnv_seq_prod_NQ"
("l1" "lim(NQ(f1!1, x!1), 0)" "l2"
"lim(NQ(f2!1, x!1), 0)"))
(("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(deriv_const_TCC1 0
(deriv_const_TCC1-1 nil 3253536989
("" (lemma "const_derivable") (("" (propax) nil nil)) nil)
((const_derivable formula-decl nil derivatives_def nil)) nil))
(deriv_const 0
(deriv_const-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "const_derivable" "derivable?" "deriv"
"const_NQ")
(("" (assert)
(("" (use "lim_const_fun[(A(x!1))]" ("b" "0" "c" "0")) nil
nil))
nil))
nil))
nil)
((const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil))
nil))
(deriv_scal_TCC1 0
(deriv_scal_TCC1-1 nil 3253536989
("" (lemma "scal_derivable") (("" (propax) nil nil)) nil)
((scal_derivable formula-decl nil derivatives_def nil)) nil))
(deriv_scal 0
(deriv_scal-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "scal_derivable" "derivable?" "deriv"
"scal_NQ" "lim_scal_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
nil nil))
(deriv_inv_TCC1 0
(deriv_inv_TCC1-1 nil 3253536989
("" (lemma "inv_derivable") (("" (propax) nil nil)) nil)
((inv_derivable formula-decl nil derivatives_def nil)) nil))
(deriv_inv 0
(deriv_inv-1 nil 3253536989
("" (skosimp)
(("" (forward-chain "inv_derivable")
(("" (assert)
((""
(auto-rewrite "deriv" "deriv_TCC" "derivable?"
("lim_fun_def[(A(x!1))]"
"lim_fun_lemma[(A(x!1))]"))
(("" (assert)
(("" (use "cnv_seq_inv_NQ" ("l1" "lim(NQ(g!1, x!1), 0)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(deriv_div_TCC1 0
(deriv_div_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "div_derivable") nil nil)) nil)
((div_derivable formula-decl nil 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)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil))
nil))
(deriv_div 0
(deriv_div-1 nil 3253536989
(""
(grind :defs nil :rewrites
("inv_derivable" "deriv_inv" "deriv_prod" "div_function[T]" "/"))
nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(inv_derivable formula-decl nil derivatives_def nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_inv formula-decl nil derivatives_def nil)
(deriv_prod formula-decl nil derivatives_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" derivatives_def 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)
(div_function formula-decl nil real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
nil))
(deriv_identity_TCC1 0
(deriv_identity_TCC1-1 nil 3253536989
("" (lemma "identity_derivable") (("" (propax) nil nil)) nil)
((identity_derivable formula-decl nil derivatives_def nil)) nil))
(deriv_identity 0
(deriv_identity-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "identity_derivable" "derivable?"
"deriv" "identity_NQ")
(("" (use "lim_const_fun[(A(x!1))]" ("b" "1" "c" "0"))
(("" (assert) nil nil)) nil))
nil))
nil)
((id_fun_continuous name-judgement "continuous_fun"
continuous_functions nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil))
nil)))
[ zur Elbe Produktseite wechseln0.11Quellennavigators
Analyse erneut starten
]
|
2026-03-28
|
