|
(table_of_integrals
(IMP_fundamental_theorem_TCC1 0
(IMP_fundamental_theorem_TCC1-1 nil 3623168299
("" (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 3623168299
("" (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
("" (auto-rewrite "xis_lem")
(("" (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" (lemma "deriv_domain") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((antiderivative? const-decl "bool" indefinite_integral nil)
(deriv_domain formula-decl nil indefinite_integral nil)
(not_one_element formula-decl nil table_of_integrals 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)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint nonempty-type-eq-decl nil integers nil)
(^ const-decl "real" exponentiation nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(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)
(real_times_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_div_nzreal_is_real application-judgement "real" reals 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
("" (auto-rewrite "xis_lem")
(("" (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 "deriv_domain")
(("2" (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 "deriv_domain")
(("2" (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 "deriv_domain")
(("2" (propax) 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)
(fundamental3 formula-decl nil fundamental_theorem nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields 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)
(real_plus_real_is_real application-judgement "real" reals nil)
(deriv_domain formula-decl nil indefinite_integral nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint nonempty-type-eq-decl nil integers nil)
(derivable_cont_fun formula-decl nil derivatives 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 "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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(integral_linear_TCC1 0
(integral_linear_TCC1-1 nil 3611494920
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(integral_linear 0
(integral_linear-1 nil 3611494930
("" (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))
shostak))
(integral_quadratic_TCC1 0
(integral_quadratic_TCC1-1 nil 3612513846 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(integral_quadratic_TCC2 0
(integral_quadratic_TCC2-1 nil 3612513846
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(integral_quadratic_TCC3 0
(integral_quadratic_TCC3-1 nil 3612513846
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(integral_quadratic 0
(integral_quadratic-1 nil 3612513873
("" (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))
shostak)))
¤ Dauer der Verarbeitung: 0.38 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
