|
(table_of_integrals
(IMP_fundamental_theorem_TCC1 0
(IMP_fundamental_theorem_TCC1-1 nil 3610702399
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil table_of_integrals nil)) nil))
(IMP_fundamental_theorem_TCC2 0
(IMP_fundamental_theorem_TCC2-1 nil 3610702399
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil table_of_integrals nil)) nil))
(antideriv_x_to_n_TCC1 0
(antideriv_x_to_n_TCC1-1 nil 3298216573 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) shostak))
(antideriv_x_to_n_TCC2 0
(antideriv_x_to_n_TCC2-1 nil 3298216574 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil))
shostak))
(antideriv_x_to_n 0
(antideriv_x_to_n-2 nil 3298217808
("" (skosimp*)
(("" (assert)
(("" (expand "antiderivative?")
(("" (lemma "deriv_x_to_n[T]")
(("1" (inst - "n!1+1" "c!1/(n!1+1)")
(("1" (assert)
(("1" (flatten)
(("1" (assert)
(("1" (replace -2)
(("1" (apply-extensionality 1 :hide? t)
(("1" (factor 1 l)
(("1" (name-replace "NP1" "(1 + n!1)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil))
nil)
("3" (lemma "deriv_domain") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(T formal-nonempty-subtype-decl nil table_of_integrals nil)
(T_pred const-decl "[real -> boolean]" table_of_integrals 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)
(deriv_x_to_n formula-decl nil derivatives nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(posint nonempty-type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(not_one_element formula-decl nil table_of_integrals nil)
(deriv_domain formula-decl nil indefinite_integral nil)
(antiderivative? const-decl "bool" indefinite_integral nil))
nil)
(antideriv_x_to_n-1 nil 3298216903
("" (skosimp*)
(("" (assert)
(("" (expand "antiderivative?")
(("" (lemma "deriv_x_to_n[T]")
(("1" (inst - "n!1+1" "a!1/(n!1+1)")
(("1" (assert)
(("1" (flatten)
(("1" (assert)
(("1" (replace -2)
(("1" (apply-extensionality 1 :hide? t)
(("1" (factor 1 l)
(("1" (name-replace "NP1" "(1 + n!1)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (lemma "not_one_element") (("2" (inst?) nil nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_x_to_n formula-decl nil derivatives nil)) shostak))
(integral_x_to_n 0
(integral_x_to_n-1 nil 3298217828
("" (skosimp*)
(("" (assert)
(("" (lemma "fundamental3[T]")
(("" (inst?)
(("" (inst - "(LAMBDA x: (c!1/(n!1+1))*x^(n!1+1))")
(("" (assert)
(("" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (lemma "deriv_x_to_n[T]")
(("1" (inst?)
(("1" (assert) (("1" (flatten) nil nil)) nil))
nil)
("2" (lemma "not_one_element")
(("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain")
(("3" (propax) nil nil)) nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "deriv_x_to_n[T]")
(("1" (assert)
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1" (assert)
(("1"
(replace -2)
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(factor 1 l)
(("1"
(name-replace "NP1" "(1 + n!1)")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element")
(("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain")
(("3" (propax) nil nil)) nil))
nil))
nil)
("4" (hide 2)
(("4" (lemma "derivable_cont_fun[T]")
(("1" (inst?)
(("1" (assert)
(("1" (hide 2)
(("1" (lemma "deriv_x_to_n[T]")
(("1" (inst?) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element")
(("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(>= const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(derivable_cont_fun formula-decl nil derivatives nil)
(posint nonempty-type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(deriv_domain formula-decl nil indefinite_integral nil)
(not_one_element formula-decl nil table_of_integrals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(deriv_x_to_n formula-decl nil derivatives nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(fundamental3 formula-decl nil fundamental_theorem 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]" table_of_integrals nil)
(T formal-nonempty-subtype-decl nil table_of_integrals nil))
shostak))
(integral_linear_TCC1 0
(integral_linear_TCC1-1 nil 3611912085 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(integral_linear 0
(integral_linear-1 nil 3611921758
("" (skosimp*)
(("" (lemma "Integral_sum")
(("" (inst -1 "a!1" "b!1" "LAMBDA x: mm!1 * x" "LAMBDA x: bb!1")
(("" (lemma "integral_x_to_n")
(("" (inst -1 "a!1" "b!1" "1" "mm!1")
(("" (lemma "Integral_const_fun")
(("" (inst -1 "bb!1" "a!1" "b!1")
(("" (expand "const_fun")
(("" (flatten)
(("" (expand "^")
(("" (expand "expt")
(("" (expand "expt")
(("" (expand "expt")
(("" (flatten)
((""
(replace -2)
((""
(replace -4)
((""
(prop)
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil table_of_integrals nil)
(T_pred const-decl "[real -> boolean]" table_of_integrals 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)
(Integral_sum formula-decl nil integral nil)
(integral_x_to_n formula-decl nil table_of_integrals nil)
(Integral_const_fun formula-decl nil integral nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(^ const-decl "real" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt def-decl "real" exponentiation nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(integral_quadratic_TCC1 0
(integral_quadratic_TCC1-1 nil 3612514704 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(integral_quadratic_TCC2 0
(integral_quadratic_TCC2-1 nil 3612514704 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(integral_quadratic_TCC3 0
(integral_quadratic_TCC3-1 nil 3612514704 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(integral_quadratic 0
(integral_quadratic-1 nil 3612514730
("" (skosimp*)
(("" (lemma "Integral_sum")
((""
(inst -1 " a!1" "b!1" "LAMBDA x: A!1 * x ^ 2"
"LAMBDA x: B!1 * x + C!1")
(("" (lemma "integral_x_to_n")
(("" (inst -1 "a!1" "b!1" "2" "A!1")
(("" (lemma "integral_linear")
(("" (inst -1 "a!1" "b!1" "B!1" "C!1")
(("" (prop)
(("1" (assert) nil nil)
("2" (assert)
(("2" (flatten)
(("2" (assert)
(("2" (replace -4)
(("2" (replace -6) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil) ("4" (assert) nil nil)
("5" (assert) nil nil) ("6" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil table_of_integrals nil)
(T_pred const-decl "[real -> boolean]" table_of_integrals 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)
(Integral_sum formula-decl nil integral nil)
(integral_x_to_n formula-decl nil table_of_integrals nil)
(integral_linear formula-decl nil table_of_integrals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(>= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil)))
¤ Dauer der Verarbeitung: 0.28 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.
|
