|
(integration_by_parts
(IMP_fundamental_theorem_TCC1 0
(IMP_fundamental_theorem_TCC1-1 nil 3603208137
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil integration_by_parts nil)) nil))
(IMP_fundamental_theorem_TCC2 0
(IMP_fundamental_theorem_TCC2-1 nil 3603208137
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil integration_by_parts nil)) nil))
(integ_parts_prep_TCC1 0
(integ_parts_prep_TCC1-1 nil 3603197586
("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
((deriv_domain 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]" integration_by_parts nil)
(T formal-nonempty-subtype-decl nil integration_by_parts nil))
nil))
(integ_parts_prep 0
(integ_parts_prep-2 nil 3603197701
("" (skosimp*)
(("" (name "F" "(LAMBDA (x: T): v!1(x) * deriv[T](u!1)(x))")
(("" (replace -1)
(("" (case "continuous?(F)")
(("1" (lemma "cont_fun_Integrable?[T]")
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "prod_fun_continuous[T]")
(("2" (inst -1 "v!1" "deriv(u!1)")
(("1" (expand "*") (("1" (assert) nil nil)) nil)
("2" (lemma "derivable_cont_fun[T]")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(T formal-nonempty-subtype-decl nil integration_by_parts nil)
(T_pred const-decl "[real -> boolean]" integration_by_parts 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)
(real_times_real_is_real application-judgement "real" reals nil)
(continuous? const-decl "bool" continuous_functions nil)
(connected_domain formula-decl nil integration_by_parts nil)
(not_one_element formula-decl nil integration_by_parts nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(connected? const-decl "bool" deriv_domain_def nil)
(cont_fun_Integrable? formula-decl nil integral nil)
(prod_fun_continuous judgement-tcc nil continuous_functions nil)
(derivable_cont_fun formula-decl nil derivatives nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(v!1 skolem-const-decl "[T -> real]" integration_by_parts nil)
(u!1 skolem-const-decl "[T -> real]" integration_by_parts nil))
nil)
(integ_parts_prep-1 nil 3603197589
("" (skosimp*)
(("" (name "F" "(LAMBDA (x: T): u!1(x) * deriv[T](v!1)(x))")
(("" (replace -1)
(("" (case "continuous?(F)")
(("1" (lemma "cont_fun_Integrable?[T]")
(("1" (inst?) (("1" (assert) nil)))
("2" (lemma "not_one_element") (("2" (propax) nil)))
("3" (lemma "connected_domain")
(("3" (expand "connected?") (("3" (propax) nil)))))))
("2" (hide 2)
(("2" (lemma "prod_fun_continuous[T]")
(("2" (inst -1 "u!1" "deriv(v!1)")
(("1" (expand "*") (("1" (assert) nil)))
("2" (lemma "derivable_cont_fun[T]")
(("2" (inst?) (("2" (assert) nil))))))))))))))))))
nil)
nil nil))
(integ_parts_TCC1 0
(integ_parts_TCC1-1 nil 3393862614
("" (skosimp*)
(("" (lemma "integ_parts_prep")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((integ_parts_prep formula-decl nil integration_by_parts nil)
(real_times_real_is_real application-judgement "real" reals nil)
(T formal-nonempty-subtype-decl nil integration_by_parts nil)
(T_pred const-decl "[real -> boolean]" integration_by_parts 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))
(integ_parts_TCC2 0
(integ_parts_TCC2-1 nil 3393862614
("" (skosimp*)
(("" (name "F" "(LAMBDA (x: T): v!1(x) * deriv[T](u!1)(x))")
(("" (replace -1)
(("" (case "continuous?(F)")
(("1" (lemma "cont_fun_Integrable?[T]")
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil)
("3" (lemma "connected_domain")
(("3" (hide 2)
(("3" (expand "connected?") (("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "prod_fun_continuous[T]")
(("2" (inst -1 "v!1" "deriv(u!1)")
(("1" (expand "*") (("1" (assert) nil nil)) nil)
("2" (lemma "derivable_cont_fun[T]")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(T formal-nonempty-subtype-decl nil integration_by_parts nil)
(T_pred const-decl "[real -> boolean]" integration_by_parts 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)
(real_times_real_is_real application-judgement "real" reals nil)
(continuous? const-decl "bool" continuous_functions nil)
(connected_domain formula-decl nil integration_by_parts nil)
(not_one_element formula-decl nil integration_by_parts nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(connected? const-decl "bool" deriv_domain_def nil)
(cont_fun_Integrable? formula-decl nil integral nil)
(prod_fun_continuous judgement-tcc nil continuous_functions nil)
(derivable_cont_fun formula-decl nil derivatives nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions nil)
(v!1 skolem-const-decl "[T -> real]" integration_by_parts nil)
(u!1 skolem-const-decl "[T -> real]" integration_by_parts nil))
nil))
(integ_parts 0
(integ_parts-4 nil 3477655234
("" (skosimp*)
(("" (lemma "deriv_prod_fun[T]")
(("" (inst -1 "u!1" "v!1")
(("" (lemma "prod_derivable_fun[T]")
(("" (inst?)
(("" (assert)
(("" (assert)
(("" (case "continuous?(deriv(u!1)*v!1)")
(("1" (case "continuous?(deriv(v!1)*u!1)")
(("1" (case "continuous?(deriv(u!1 * v!1))")
(("1"
(case "Integral(a!1,b!1,deriv(u!1 * v!1)) = Integral(a!1,b!1,deriv(u!1) * v!1 + deriv(v!1) * u!1)")
(("1" (lemma "fundamental3b")
(("1" (inst -1 "u!1 * v!1" "a!1" "b!1")
(("1" (assert)
(("1"
(flatten)
(("1"
(replace -2)
(("1"
(hide -2)
(("1"
(assert)
(("1"
(lemma "Integral_sum[T]")
(("1"
(inst
-1
"a!1"
"b!1"
"deriv(u!1) * v!1"
"deriv(v!1) * u!1")
(("1"
(split -1)
(("1"
(flatten)
(("1"
(case-replace
"(LAMBDA (x: T): (deriv(u!1) * v!1)(x) + (deriv(v!1) * u!1)(x)) = deriv(u!1) * v!1 + deriv(v!1) * u!1")
(("1"
(replace -3)
(("1"
(hide -1 -3)
(("1"
(case-replace
"(LAMBDA (x_1: T): u!1(x_1) * deriv(v!1)(x_1)) = u!1 * deriv(v!1)")
(("1"
(case-replace
"(LAMBDA (x_2: T): v!1(x_2) * deriv(u!1)(x_2)) = v!1 * deriv(u!1)")
(("1"
(expand "*")
(("1"
(assert)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"*")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "*")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide 2)
(("2"
(expand "*")
(("2"
(expand "+ ")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"cont_Integrable?[T]")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(lemma
"cont_Integrable?[T]")
(("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (assert) nil nil)) nil)
("3" (hide 2)
(("3" (lemma "cont_Integrable?[T]")
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (lemma "not_one_element")
(("2" (propax) nil nil)) nil)
("3" (assert)
(("3"
(lemma "connected_domain")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("4" (lemma "not_one_element")
(("4" (propax) nil nil)) nil)
("5" (lemma "connected_domain")
(("5" (propax) nil nil)) nil)
("6" (hide 2)
(("6" (lemma "cont_Integrable?[T]")
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (lemma "not_one_element")
(("2" (propax) nil nil)) nil)
("3" (lemma "connected_domain")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "sum_cont_fun[T]")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "prod_cont_fun[T]")
(("2" (inst?)
(("2" (assert)
(("2" (lemma "derivable_cont[T]")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "prod_cont_fun[T]")
(("2" (inst?)
(("2" (assert)
(("2" (lemma "derivable_cont[T]")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integration_by_parts nil)
(T_pred const-decl "[real -> boolean]" integration_by_parts 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_prod_fun formula-decl nil derivatives nil)
(prod_derivable_fun formula-decl nil derivatives nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(continuous? const-decl "bool" continuous_functions nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv const-decl "[T -> real]" derivatives nil)
(derivable_cont judgement-tcc nil derivatives nil)
(prod_cont_fun formula-decl nil continuous_functions nil)
(connected_domain formula-decl nil integration_by_parts nil)
(not_one_element formula-decl nil integration_by_parts nil)
(fundamental3b formula-decl nil fundamental_theorem nil)
(cont_Integrable? formula-decl nil integral nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Integral_sum formula-decl nil integral nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(connected? const-decl "bool" deriv_domain_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Integrable? const-decl "bool" integral_def nil)
(Integrable_funs type-eq-decl nil integral_def nil)
(Integral const-decl "real" integral_def nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(sum_cont_fun formula-decl nil continuous_functions nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil))
nil)
(integ_parts-3 nil 3445337156
(";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(skosimp*)
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(lemma "deriv_prod_fun[T]")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(inst -1 "u!1" "v!1")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(lemma "prod_derivable_fun[T]")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(inst?)
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(assert)
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(lemma "derivable_cont_fun")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(inst - "u!1*v!1")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(assert)
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(lemma "derivable_cont_fun")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(inst - "u!1")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(assert)
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(lemma "derivable_cont_fun")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(inst - "v!1")
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(assert)
((";;; Proof integ_parts-2 for formula integration_by_parts.integ_parts"
(case "continuous?(deriv(u!1)*v!1)")
(("1"
(case
"continuous?(deriv(v!1)*u!1)")
(("1"
(case
"continuous?(deriv(u!1 * v!1))")
(("1"
(case
"Integral(a!1,b!1,deriv(u!1 * v!1)) = Integral(a!1,b!1,deriv(u!1) * v!1 + deriv(v!1) * u!1)")
(("1"
(lemma "fundamental3b")
(("1"
(inst
-1
"u!1 * v!1"
"a!1"
"b!1")
(("1"
(assert)
(("1"
(flatten)
(("1"
(replace -2)
(("1"
(hide -2)
(("1"
(assert)
(("1"
(lemma
"Integral_sum[T]")
(("1"
(inst
-1
"a!1"
"b!1"
"deriv(u!1) * v!1"
"deriv(v!1) * u!1")
(("1"
(split -1)
(("1"
(flatten)
(("1"
(case-replace
"(LAMBDA (x: T): (deriv(u!1) * v!1)(x) + (deriv(v!1) * u!1)(x)) = deriv(u!1) * v!1 + deriv(v!1) * u!1")
(("1"
(replace
-3)
(("1"
(hide
-1
-3)
(("1"
(case-replace
"(LAMBDA (x_1: T): u!1(x_1) * deriv(v!1)(x_1)) = u!1 * deriv(v!1)")
(("1"
(case-replace
"(LAMBDA (x_2: T): v!1(x_2) * deriv(u!1)(x_2)) = v!1 * deriv(u!1)")
(("1"
(expand
"*")
(("1"
(assert)
nil)))
("2"
(hide
2)
(("2"
(expand
"*")
(("2"
(propax)
nil)))))))
("2"
(hide
2)
(("2"
(expand
"*")
(("2"
(propax)
nil)))))))))))
("2"
(assert)
(("2"
(hide
2)
(("2"
(expand
"*")
(("2"
(expand
"+ ")
(("2"
(propax)
nil)))))))))))))
("2"
(hide 2)
(("2"
(lemma
"cont_Integrable?[T]")
(("2"
(inst?)
(("2"
(assert)
nil)))))))
("3"
(hide 2)
(("3"
(lemma
"cont_Integrable?[T]")
(("3"
(inst?)
(("3"
(assert)
nil)))))))))))))))))))))))))))
("2"
(hide 2)
(("2" (assert) nil)))
("3"
(hide 2)
(("3"
(lemma
"cont_Integrable?[T]")
(("1"
(inst?)
(("1" (assert) nil)))
("2"
(lemma "not_one_element")
(("2" (propax) nil)))
("3"
(assert)
(("3"
(lemma
"connected_domain")
(("3"
(propax)
nil)))))))))
("4"
(lemma "not_one_element")
(("4" (propax) nil)))
("5"
(lemma "connected_domain")
(("5" (propax) nil)))
("6"
(hide 2)
(("6"
(lemma
"cont_Integrable?[T]")
(("1"
(inst?)
(("1" (assert) nil)))
("2"
(lemma "not_one_element")
(("2" (propax) nil)))
("3"
(lemma
"connected_domain")
(("3"
(propax)
nil)))))))))
("2"
(hide 2)
(("2"
(replace -7)
(("2"
(lemma "sum_cont_fun[T]")
(("2"
(inst?)
(("2"
(assert)
nil)))))))))))
("2"
(hide 2)
(("2"
(lemma "prod_cont_fun[T]")
(("2"
(inst?)
(("2" (assert) nil)))))))))
("2"
(hide 2)
(("2"
(lemma "prod_cont_fun[T]")
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))
";;; developed with shostak decision procedures")
nil nil)
(integ_parts-2 nil 3393933493
("" (skosimp*)
(("" (lemma "deriv_prod_fun[T]")
(("" (inst -1 "u!1" "v!1")
(("" (lemma "prod_derivable_fun[T]")
(("" (inst?)
(("" (assert)
(("" (lemma "derivable_cont_fun")
(("" (inst - "u!1*v!1")
(("" (assert)
(("" (lemma "derivable_cont_fun")
(("" (inst - "u!1")
(("" (assert)
(("" (lemma "derivable_cont_fun")
(("" (inst - "v!1")
((""
(assert)
((""
(case "continuous?(deriv(u!1)*v!1)")
(("1"
(case
"continuous?(deriv(v!1)*u!1)")
(("1"
(case "(deriv(u!1 * v!1))")
(("1"
(case
"Integral(a!1,b!1,deriv(u!1 * v!1)) = Integral(a!1,b!1,deriv(u!1) * v!1 + deriv(v!1) * u!1)")
(("1"
(lemma "fundamental3b")
(("1"
(inst
-1
"u!1 * v!1"
"a!1"
"b!1")
(("1"
(assert)
(("1"
(flatten)
(("1"
(replace -2)
(("1"
(hide -2)
(("1"
(assert)
(("1"
(lemma
"Integral_sum[T]")
(("1"
(inst
-1
"a!1"
"b!1"
"deriv(u!1) * v!1"
"deriv(v!1) * u!1")
(("1"
(split -1)
(("1"
(flatten)
(("1"
(case-replace
"(LAMBDA (x: T): (deriv(u!1) * v!1)(x) + (deriv(v!1) * u!1)(x)) = deriv(u!1) * v!1 + deriv(v!1) * u!1")
(("1"
(replace
-3)
(("1"
(hide
-1
-3)
(("1"
(case-replace
"(LAMBDA (x_1: T): u!1(x_1) * deriv(v!1)(x_1)) = u!1 * deriv(v!1)")
(("1"
(case-replace
"(LAMBDA (x_2: T): v!1(x_2) * deriv(u!1)(x_2)) = v!1 * deriv(u!1)")
(("1"
(expand
"*")
(("1"
(assert)
nil
nil))
nil)
("2"
(hide
2)
(("2"
(expand
"*")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(expand
"*")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide
2)
(("2"
(expand
"*")
(("2"
(expand
"+ ")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"cont_Integrable?[T]")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(lemma
"cont_Integrable?[T]")
(("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2" (assert) nil nil))
nil)
("3"
(hide 2)
(("3"
(lemma
"cont_Integrable?[T]")
(("1"
(inst?)
(("1" (assert) nil nil))
nil)
("2"
(lemma "not_one_element")
(("2" (propax) nil nil))
nil)
("3"
(assert)
(("3"
(lemma
"connected_domain")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(lemma "not_one_element")
(("4" (propax) nil nil))
nil)
("5"
(lemma "connected_domain")
(("5" (propax) nil nil))
nil)
("6"
(hide 2)
(("6"
(lemma
"cont_Integrable?[T]")
(("1"
(inst?)
(("1" (assert) nil nil))
nil)
("2"
(lemma "not_one_element")
(("2" (propax) nil nil))
nil)
("3"
(lemma
"connected_domain")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(replace -7)
(("2"
(lemma "sum_cont_fun[T]")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma "prod_cont_fun[T]")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma "prod_cont_fun[T]")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_prod_fun formula-decl nil derivatives nil)
(prod_derivable_fun formula-decl nil derivatives nil)
(deriv const-decl "[T -> real]" derivatives nil)
(prod_cont_fun formula-decl nil continuous_functions nil)
(fundamental3b formula-decl nil fundamental_theorem nil)
(cont_Integrable? formula-decl nil integral nil)
(Integral_sum formula-decl nil integral nil)
(Integrable? const-decl "bool" integral_def nil)
(Integrable_funs type-eq-decl nil integral_def nil)
(Integral const-decl "real" integral_def nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(sum_cont_fun formula-decl nil continuous_functions nil)
(derivable_cont_fun formula-decl nil derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil)
(integ_parts-1 nil 3393863589
("" (skosimp*)
(("" (lemma "deriv_prod_fun[T]")
(("" (inst -1 "u!1" "v!1")
((""
(case "Integral(a!1,b!1,deriv(u!1 * v!1)) = Integral(a!1,b!1,deriv(u!1) * v!1 + deriv(v!1) * u!1)")
(("1" (hide -2)
(("1" (lemma "fundamental5")
(("1" (inst -1 "u!1 * v!1" "a!1" "b!1")
(("1" (assert)
(("1" (split -1)
(("1" (flatten)
(("1" (replace -2)
(("1" (hide -2)
(("1" (lemma "Integral_sum[T]")
(("1"
(inst -1 "a!1" "b!1" "deriv(u!1) * v!1"
"deriv(v!1) * u!1")
(("1"
(split -1)
(("1"
(flatten)
(("1"
(case-replace
"(LAMBDA (x: T): (deriv(u!1) * v!1)(x) + (deriv(v!1) * u!1)(x)) = deriv(u!1) * v!1 + deriv(v!1) * u!1")
(("1"
(replace -3)
(("1"
(hide -1 -3)
(("1"
(case-replace
"(LAMBDA (x_1: T): u!1(x_1) * deriv(v!1)(x_1)) = u!1 * deriv(v!1)")
(("1"
(case-replace
"(LAMBDA (x_2: T): v!1(x_2) * deriv(u!1)(x_2)) = v!1 * deriv(u!1)")
(("1"
(expand "*")
(("1" (assert) nil nil))
nil)
("2"
(hide 2)
(("2"
(expand "*")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "*")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide 2)
(("2"
(expand "*")
(("2"
(expand "+ ")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma "derivable_cont_fun[T]")
(("2"
(inst -1 "v!1")
(("2"
(assert)
(("2" (postpone) nil nil))
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "prod_derivable_fun")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil)
("3" (hide 2) (("3" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (assert) nil nil)) nil)
("3" (hide 2) (("3" (postpone) nil nil)) nil)
("4" (lemma "not_one_element") (("4" (propax) nil nil)) nil)
("5" (lemma "connected_domain") (("5" (propax) nil nil))
nil)
("6" (hide 2) (("6" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil)
nil shostak)))
¤ Dauer der Verarbeitung: 0.67 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.
|
