|
(integral_indef_sincos
(derivable_sin_lin_TCC1 0
(derivable_sin_lin_TCC1-1 nil 3577540870
("" (skosimp*)
(("" (lemma "deriv_domain[T]")
(("1" (propax) nil nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_indef_sincos 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_domain formula-decl nil deriv_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil))
nil))
(derivable_sin_lin_TCC2 0
(derivable_sin_lin_TCC2-1 nil 3577540870
("" (skosimp*)
(("" (lemma "not_one_element") (("" (propax) nil nil)) nil)) nil)
((not_one_element formula-decl nil integral_indef_sincos nil)) nil))
(derivable_sin_lin 0
(derivable_sin_lin-1 nil 3577540871
("" (skosimp*)
(("" (auto-rewrite-theory "derivatives_lam[T]")
(("1" (lemma "derivable_scal1_lam[T]")
(("1" (inst -1 "(k!1/a!1)" "LAMBDA(x:T):sin(a!1 * x + b!1)")
(("1" (lemma "composition_derivable_fun[T,real]")
(("1"
(inst -1 "(LAMBDA(x:T): a!1*x + b!1)"
"(LAMBDA(x:real): sin(x))")
(("1" (assert)
(("1" (expand "o")
(("1" (lemma "sin_derivable_fun")
(("1"
(case-replace "(LAMBDA (x: real): sin(x))=sin")
(("1" (apply-extensionality 1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain[T]")
(("1" (propax) nil nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(number nonempty-type-decl nil numbers 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]" integral_indef_sincos nil)
(T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil 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)
(derivable? const-decl "bool" derivatives "analysis/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(sin const-decl "real" sincos_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(a!1 skolem-const-decl "real" integral_indef_sincos nil)
(b!1 skolem-const-decl "real" integral_indef_sincos nil)
(O const-decl "T3" function_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sin_derivable_fun formula-decl nil sincos nil)
(derivable_add_lam formula-decl nil derivatives_lam "analysis/")
(derivable_id_lam formula-decl nil derivatives_lam "analysis/")
(derivable_scald2_lam formula-decl nil derivatives_lam "analysis/")
(derivable_const_lam formula-decl nil derivatives_lam "analysis/")
(composition_derivable_fun formula-decl nil chain_rule "analysis/")
(derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain formula-decl nil deriv_sincos nil))
shostak))
(derivable_cos_lin 0
(derivable_cos_lin-1 nil 3577541263
("" (skosimp*)
(("" (auto-rewrite-theory "derivatives_lam[T]")
(("1" (lemma "derivable_scal1_lam[T]")
(("1" (inst -1 "(k!1/a!1)" "LAMBDA(x:T):cos(a!1 * x + b!1)")
(("1" (lemma "composition_derivable_fun[T,real]")
(("1" (assert)
(("1" (expand "o")
(("1"
(inst -1 "(LAMBDA(x:T): a!1*x + b!1)"
"(LAMBDA(x:real): cos(x))")
(("1" (assert)
(("1" (lemma "cos_derivable_fun")
(("1"
(case-replace "(LAMBDA (x: real): cos(x))=cos")
(("1" (apply-extensionality 1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain[T]")
(("1" (propax) nil nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(number nonempty-type-decl nil numbers 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]" integral_indef_sincos nil)
(T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil 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)
(derivable? const-decl "bool" derivatives "analysis/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(cos const-decl "real" sincos_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(a!1 skolem-const-decl "real" integral_indef_sincos nil)
(b!1 skolem-const-decl "real" integral_indef_sincos nil)
(derivable_const_lam formula-decl nil derivatives_lam "analysis/")
(derivable_scald2_lam formula-decl nil derivatives_lam "analysis/")
(cos_derivable_fun formula-decl nil sincos nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(derivable_add_lam formula-decl nil derivatives_lam "analysis/")
(derivable_id_lam formula-decl nil derivatives_lam "analysis/")
(O const-decl "T3" function_props nil)
(composition_derivable_fun formula-decl nil chain_rule "analysis/")
(derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain formula-decl nil deriv_sincos nil))
shostak))
(deriv_sin_lin_TCC1 0
(deriv_sin_lin_TCC1-1 nil 3577107599
("" (skosimp*)
(("" (auto-rewrite-theory "derivatives_lam[T]")
(("1" (hide 1)
(("1" (lemma "derivable_scal1_lam[T]")
(("1" (inst -1 "k!1" "(LAMBDA (x:T): sin(b!1 + a!1 * x))")
(("1" (hide 2)
(("1" (lemma "composition_derivable_fun[T,real]")
(("1"
(inst - "(LAMBDA(x:T): a!1*x + b!1)"
"(LAMBDA(x:real): sin(x))")
(("1" (assert)
(("1" (expand "o")
(("1" (hide 2)
(("1" (lemma "sin_derivable_fun")
(("1" (assert)
(("1"
(case-replace
"(LAMBDA(x:real): sin(x))=sin")
(("1"
(apply-extensionality 1 :hide? t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 3)
(("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil))
nil)
("3" (hide 2 3)
(("3" (lemma "deriv_domain[T]")
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(number nonempty-type-decl nil numbers 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]" integral_indef_sincos nil)
(T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
(O const-decl "T3" function_props nil)
(sin_derivable_fun formula-decl nil sincos nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(derivable_add_lam formula-decl nil derivatives_lam "analysis/")
(derivable_id_lam formula-decl nil derivatives_lam "analysis/")
(derivable_const_lam formula-decl nil derivatives_lam "analysis/")
(composition_derivable_fun formula-decl nil chain_rule "analysis/")
(a!1 skolem-const-decl "real" integral_indef_sincos nil)
(b!1 skolem-const-decl "real" integral_indef_sincos nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sin const-decl "real" sincos_def nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(derivable? const-decl "bool" derivatives "analysis/")
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(deriv_domain formula-decl nil deriv_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(connected_domain formula-decl nil integral_indef_sincos nil))
nil))
(deriv_sin_lin 0
(deriv_sin_lin-1 nil 3577107639
("" (skosimp*)
(("" (auto-rewrite-theory "derivatives_lam[T]")
(("1" (case "derivable?[T](LAMBDA(x:T):sin(b!1 + a!1*x))")
(("1" (lemma "deriv_scal_fun[T]")
(("1" (inst - "k!1" "(LAMBDA(x:T):sin(b!1 + a!1 * x))")
(("1" (assert)
(("1" (expand "*")
(("1" (assert)
(("1" (apply-extensionality 2 :hide? t)
(("1" (hide -1)
(("1" (lemma "deriv_comp_fun[T,real]")
(("1"
(inst - "(LAMBDA(x:T):a!1*x + b!1)"
"(LAMBDA(x:real): sin(x))")
(("1" (expand "o")
(("1" (replace -1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(expand "*")
(("1"
(ground)
(("1"
(lemma "deriv_sin_fun")
(("1"
(case-replace
"(LAMBDA(x:real): sin(x)) = sin")
(("1"
(replace -2)
(("1" (assert) nil nil))
nil)
("2"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sincos.sin_derivable_fun")
(("2"
(case-replace
"(LAMBDA(x:real):sin(x))=sin")
(("2"
(apply-extensionality 1 :hide? t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (hide 3)
(("2" (lemma "comp_derivable_fun[T,real]")
(("2"
(inst - "(LAMBDA (x:T): b!1 + a!1 * x)"
"(LAMBDA(x:real): sin(x))")
(("2" (assert)
(("2" (hide 2)
(("2" (lemma "sin_derivable_fun")
(("2"
(case-replace "(LAMBDA (x: real): sin(x))=sin")
(("2" (apply-extensionality 1 :hide? t) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil))
nil)
("3" (hide (2 3))
(("3" (assert)
(("3" (lemma "deriv_domain[T]")
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil))
nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(number nonempty-type-decl nil numbers 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]" integral_indef_sincos nil)
(T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(comp_derivable_fun formula-decl nil chain_rule "analysis/")
(deriv_scal_fun formula-decl nil derivatives "analysis/")
(cos_range application-judgement "trig_range" sincos_def nil)
(deriv_scal1_lam formula-decl nil derivatives_lam "analysis/")
(derivable_const_lam formula-decl nil derivatives_lam "analysis/")
(derivable_id_lam formula-decl nil derivatives_lam "analysis/")
(derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
(derivable_add_lam formula-decl nil derivatives_lam "analysis/")
(deriv_id_lam formula-decl nil derivatives_lam "analysis/")
(deriv_const_lam formula-decl nil derivatives_lam "analysis/")
(deriv_add_lam formula-decl nil derivatives_lam "analysis/")
(= const-decl "[T, T -> boolean]" equalities nil)
(deriv_sin_fun formula-decl nil sincos nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(O const-decl "T3" function_props nil)
(sin_derivable_fun formula-decl nil sincos nil)
(deriv_comp_fun formula-decl nil chain_rule "analysis/")
(cos const-decl "real" sincos_def nil)
(deriv const-decl "[T -> real]" derivatives "analysis/")
(not_one_element formula-decl nil derivatives_lam "analysis/")
(deriv_domain formula-decl nil derivatives_lam "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(b!1 skolem-const-decl "real" integral_indef_sincos nil)
(a!1 skolem-const-decl "real" integral_indef_sincos nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(sin const-decl "real" sincos_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain formula-decl nil deriv_sincos nil))
shostak))
(deriv_cos_lin_TCC1 0
(deriv_cos_lin_TCC1-1 nil 3577107599
("" (skosimp*)
(("" (auto-rewrite-theory "derivatives_lam[T]")
(("1" (hide 1)
(("1" (lemma "derivable_scal1_lam[T]")
(("1" (inst - "-k!1" "(LAMBDA (x: T): cos(b!1 + a!1 * x))")
(("1" (hide 2)
(("1" (lemma "composition_derivable_fun[T,real]")
(("1"
(inst - "LAMBDA(x:T): a!1 * x + b!1"
"LAMBDA(x:real):cos(x)")
(("1" (expand "o")
(("1" (assert)
(("1" (hide 2)
(("1" (lemma "cos_derivable_fun")
(("1"
(case-replace
"(LAMBDA (x: real): cos(x))=cos")
(("1" (apply-extensionality 1 :hide? t) nil
nil))
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[T]")
(("1" (propax) nil nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(number nonempty-type-decl nil numbers 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]" integral_indef_sincos nil)
(T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
(derivable_const_lam formula-decl nil derivatives_lam "analysis/")
(derivable_id_lam formula-decl nil derivatives_lam "analysis/")
(derivable_add_lam formula-decl nil derivatives_lam "analysis/")
(cos_derivable_fun formula-decl nil sincos nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(O const-decl "T3" function_props nil)
(composition_derivable_fun formula-decl nil chain_rule "analysis/")
(a!1 skolem-const-decl "real" integral_indef_sincos nil)
(b!1 skolem-const-decl "real" integral_indef_sincos nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(cos const-decl "real" sincos_def nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(derivable? const-decl "bool" derivatives "analysis/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain formula-decl nil deriv_sincos nil))
nil))
(deriv_cos_lin 0
(deriv_cos_lin-1 nil 3577196042
("" (skosimp*)
(("" (auto-rewrite-theory "derivatives_lam[T]")
(("1" (case "derivable?[T](LAMBDA(x:T):cos(b!1 + a!1*x))")
(("1" (lemma "deriv_scal_fun[T]")
(("1" (inst - "k!1" "(LAMBDA(x:T):cos(b!1 + a!1 * x))")
(("1" (assert)
(("1" (expand "*")
(("1" (assert)
(("1" (apply-extensionality 2 :hide? t)
(("1" (hide -1)
(("1" (lemma "deriv_comp_fun[T,real]")
(("1"
(inst - "(LAMBDA(x:T):a!1*x + b!1)"
"(LAMBDA(x:real): cos(x))")
(("1" (expand "o")
(("1" (replace -1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(expand "*")
(("1"
(lemma "deriv_cos_fun")
(("1"
(case-replace
"(LAMBDA (x: real): cos(x))=cos")
(("1"
(hide -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(hide 2)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sincos.cos_derivable_fun")
(("2"
(case-replace
"(LAMBDA (x: real): cos(x))=cos")
(("2"
(apply-extensionality 1 :hide? t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide 2) (("2" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (hide 2)
(("2" (lemma "comp_derivable_fun[T,real]")
(("2"
(inst - "(LAMBDA (x:T): b!1 + a!1 * x)"
"(LAMBDA(x:real): cos(x))")
(("2" (assert)
(("2" (hide 2)
(("2" (lemma "cos_derivable_fun")
(("2"
(case-replace "(LAMBDA (x: real): cos(x))=cos")
(("2" (apply-extensionality 1 :hide? t) nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (hide 2)
(("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil))
nil))
nil)
("3" (hide 2 3)
(("3" (lemma "deriv_domain[T]")
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(number nonempty-type-decl nil numbers 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]" integral_indef_sincos nil)
(T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(comp_derivable_fun formula-decl nil chain_rule "analysis/")
(deriv_scal_fun formula-decl nil derivatives "analysis/")
(sin_range application-judgement "trig_range" sincos_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(deriv_scal1_lam formula-decl nil derivatives_lam "analysis/")
(derivable_const_lam formula-decl nil derivatives_lam "analysis/")
(derivable_id_lam formula-decl nil derivatives_lam "analysis/")
(derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
(derivable_add_lam formula-decl nil derivatives_lam "analysis/")
(deriv_id_lam formula-decl nil derivatives_lam "analysis/")
(deriv_const_lam formula-decl nil derivatives_lam "analysis/")
(deriv_add_lam formula-decl nil derivatives_lam "analysis/")
(deriv_cos_fun formula-decl nil sincos nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(Integral const-decl "real" integral_def "analysis/")
(atan_value const-decl "real" atan nil)
(pi const-decl "posreal" atan nil)
(sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
sincos_quad nil)
(atan const-decl "real_abs_lt_pi2" atan nil)
(asin const-decl "real_abs_le_pi2" asin nil)
(inverse const-decl "D" function_inverse nil)
(sin_phase const-decl "real_abs_le1" sincos_phase nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(O const-decl "T3" function_props nil)
(cos_derivable_fun formula-decl nil sincos nil)
(deriv_comp_fun formula-decl nil chain_rule "analysis/")
(sin const-decl "real" sincos_def nil)
(deriv const-decl "[T -> real]" derivatives "analysis/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(not_one_element formula-decl nil derivatives_lam "analysis/")
(deriv_domain formula-decl nil derivatives_lam "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(b!1 skolem-const-decl "real" integral_indef_sincos nil)
(a!1 skolem-const-decl "real" integral_indef_sincos nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(cos const-decl "real" sincos_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(deriv_domain formula-decl nil deriv_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(connected_domain formula-decl nil integral_indef_sincos nil))
shostak))
(cos_lin_integrable_TCC1 0
(cos_lin_integrable_TCC1-1 nil 3579946097
("" (skeep)
(("" (lemma "connected_domain") (("" (propax) nil nil)) nil)) nil)
((connected_domain formula-decl nil integral_indef_sincos nil))
nil))
(cos_lin_integrable 0
(cos_lin_integrable-1 nil 3577200751
("" (skosimp*)
(("" (expand "integrable?")
(("" (expand "antiderivative?")
(("" (lemma "derivable_sin_lin")
(("" (inst -1 "alpha!1" "theta!1" "k!1")
(("" (assert)
((""
(inst 2
"(LAMBDA (x: T): (k!1 / alpha!1) * sin(alpha!1 * x + theta!1))")
(("" (split)
(("1" (propax) nil nil)
("2" (lemma "deriv_sin_lin")
(("2" (assert)
(("2" (inst -1 "alpha!1" "theta!1" "k!1/alpha!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(integrable? const-decl "bool" indefinite_integral "analysis/")
(derivable_sin_lin formula-decl nil integral_indef_sincos nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(deriv_sin_lin formula-decl nil integral_indef_sincos nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin const-decl "real" sincos_def 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)
(T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_indef_sincos nil)
(real_plus_real_is_real application-judgement "real" reals 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)
(antiderivative? const-decl "bool" indefinite_integral
"analysis/"))
shostak))
(sin_lin_integrable 0
(sin_lin_integrable-1 nil 3577724592
("" (skosimp*)
(("" (expand "integrable?")
(("" (expand "antiderivative?")
(("" (lemma "derivable_cos_lin")
(("" (inst -1 "alpha!1" "theta!1" "-k!1")
(("" (assert)
((""
(inst 2
"(LAMBDA (x: T): -k!1 / alpha!1 * cos(alpha!1 * x + theta!1))")
(("" (split)
(("1" (propax) nil nil)
("2" (lemma "deriv_cos_lin")
(("2" (assert)
(("2" (inst -1 "alpha!1" "theta!1" "k!1/alpha!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(integrable? const-decl "bool" indefinite_integral "analysis/")
(derivable_cos_lin formula-decl nil integral_indef_sincos nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(deriv_cos_lin formula-decl nil integral_indef_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_indef_sincos nil)
(T formal-nonempty-subtype-decl nil integral_indef_sincos 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)
(cos const-decl "real" sincos_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(minus_real_is_real application-judgement "real" reals nil)
(antiderivative? const-decl "bool" indefinite_integral
"analysis/"))
shostak))
(integral_sin_TCC1 0
(integral_sin_TCC1-1 nil 3572701399
("" (skosimp*)
(("" (lemma "sin_lin_integrable")
(("" (inst - "w!1" "v!1" "theta!1") (("" (assert) nil nil)) nil))
nil))
nil)
((sin_lin_integrable formula-decl nil integral_indef_sincos nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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))
(integral_sin_TCC2 0
(integral_sin_TCC2-1 nil 3579945862
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil integral_indef_sincos nil))
nil))
(integral_sin_TCC3 0
(integral_sin_TCC3-1 nil 3579945862
("" (skeep)
(("" (lemma "not_one_element") (("" (propax) nil nil)) nil)) nil)
((not_one_element formula-decl nil integral_indef_sincos nil)) nil))
(integral_sin 0
(integral_sin-3 "" 3577809638
("" (skeep)
(("" (lemma "indef_integral_thm[T]")
(("" (inst -1 "(LAMBDA (t: T): -(v / w) * cos(theta + w * t))")
((""
(case "derivable?((LAMBDA (t: T): -(v / w) * cos(theta + w * t)))")
(("1" (assert)
(("1" (hide -1)
(("1" (skosimp*)
(("1" (inst + "c!1")
(("1" (lemma "deriv_cos_lin")
(("1" (inst -1 "w" "theta" "v/w")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "derivable_cos_lin")
(("2" (inst -1 "w" "theta" "v")
(("2" (hide -2)
(("2" (typepred "w")
(("2" (assert)
(("2" (hide -1)
(("2" (lemma "derivable_neg_lam[T]")
(("2"
(inst -1
"(LAMBDA (t: T): v / w * cos(w * t + theta))")
(("2" (hide -2) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (lemma "not_one_element") (("3" (propax) nil nil)) nil)
("4" (lemma "deriv_domain[T]")
(("1" (propax) nil nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_indef_sincos 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)
(indef_integral_thm formula-decl nil indefinite_integral
"analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(derivable_const application-judgement "deriv_fun[T]" deriv_sincos
nil)
(const_fun_continuous application-judgement "continuous_fun[T]"
continuous_lambda "analysis/")
(deriv_cos_lin formula-decl nil integral_indef_sincos nil)
(derivable_cos_lin formula-decl nil integral_indef_sincos nil)
(derivable_neg_lam formula-decl nil derivatives_lam "analysis/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(NOT const-decl "[bool -> bool]" booleans nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain formula-decl nil deriv_sincos nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(cos const-decl "real" sincos_def nil)
(nzreal nonempty-type-eq-decl nil reals 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]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil))
shostak)
(integral_sin-2 "alt" 3577553755
("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak)
(integral_sin-1 nil 3572701400
("" (skosimp*)
(("" (lemma "indef_integral_thm[T]")
(("1"
(inst -
"(LAMBDA (x: T): -(v!1 / w!1) * cos(theta!1 + w!1 * x))")
(("1" (split -1)
(("1" (skosimp*)
(("1" (inst + "c!1")
(("1" (assert)
(("1" (lemma "deriv_cos_lin")
(("1" (inst -1 "w!1" "theta!1" "-v!1/w!1")
(("1" (assert) nil nil) ("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 3)
(("2" (lemma "scal_derivable_fun[T]")
(("1"
(inst - "-(v!1 / w!1)"
"LAMBDA(x:T): cos(theta!1 + w!1 * x)")
(("1" (assert)
(("1" (expand "*")
(("1" (hide 2)
(("1" (lemma "comp_derivable_fun[T,real]")
(("1"
(inst - "LAMBDA (x: T): w!1 * x + theta!1"
"LAMBDA(x:real): cos(x)")
(("1" (assert)
(("1" (hide 2)
(("1"
(split)
(("1"
(lemma "sum_derivable_fun[T]")
(("1"
(inst
-
"LAMBDA (x: T): w!1 * x"
"LAMBDA(x:T):theta!1")
(("1"
(split)
(("1" (postpone) nil nil)
("2"
(hide 2)
(("2"
(lemma
"scal_derivable_fun[T]")
(("2"
(inst - "w!1" "id[T]")
(("2"
(expand "id")
(("2"
(expand "*")
(("2"
(assert)
(("2"
(hide 2)
(("2"
(lemma
"id_derivable_fun[T]")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(lemma
"const_derivable_fun[T]")
(("3"
(inst - "theta!1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "cos_derivable_fun")
(("2"
(case-replace
"(LAMBDA (x: real): cos(x))=cos")
(("2"
(hide 2)
(("2"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 1) (("2" (postpone) nil nil)) nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil)
("2" (postpone) nil nil) ("3" (postpone) nil nil)
("4" (postpone) nil nil))
nil))
nil)
nil shostak))
(integral_cos_TCC1 0
(integral_cos_TCC1-1 nil 3577107599
("" (skosimp*)
(("" (lemma "cos_lin_integrable")
(("" (inst - "w!1" "v!1" "theta!1") (("" (assert) nil nil)) nil))
nil))
nil)
((cos_lin_integrable formula-decl nil integral_indef_sincos nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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))
(integral_cos 0
(integral_cos-1 nil 3577726639
("" (skeep)
(("" (lemma "indef_integral_thm[T]")
(("" (inst -1 "(LAMBDA (t: T): (v / w) * sin(theta + w * t))")
((""
(case "derivable?((LAMBDA (t: T): (v / w) * sin(theta + w * t)))")
(("1" (assert)
(("1" (skosimp*)
(("1" (inst + "c!1")
(("1" (lemma "deriv_sin_lin")
(("1" (inst -1 "w" "theta" "v/w")
(("1" (typepred "w") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "derivable_sin_lin")
(("2" (inst -1 "w" "theta" "v")
(("2" (typepred "w") (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (lemma "not_one_element") (("3" (propax) nil nil)) nil)
("4" (lemma "deriv_domain[T]")
(("1" (propax) nil nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil))
nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_indef_sincos 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)
(indef_integral_thm formula-decl nil indefinite_integral
"analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_sin_lin formula-decl nil integral_indef_sincos nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(derivable_const application-judgement "deriv_fun[T]" deriv_sincos
nil)
(const_fun_continuous application-judgement "continuous_fun[T]"
continuous_lambda "analysis/")
(derivable_sin_lin formula-decl nil integral_indef_sincos nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(deriv_domain formula-decl nil deriv_sincos nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin const-decl "real" sincos_def nil)
(nzreal nonempty-type-eq-decl nil reals 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)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil))
shostak))
(Integral_sin_TCC1 0
(Integral_sin_TCC1-1 nil 3572701399
("" (skosimp*)
(("" (lemma "derivable_Integrable?[T]")
(("1"
(inst - "t1!1" "t2!1"
" LAMBDA (t: T): v!1 * sin(theta!1 + w!1 * t)")
(("1" (assert)
(("1" (hide 3)
(("1" (lemma "derivable_sin_lin")
(("1" (inst - "w!1" "theta!1" "v!1*w!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_indef_sincos 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)
(derivable_Integrable? formula-decl nil fundamental_theorem
"analysis/")
(connected? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(derivable_sin_lin formula-decl nil integral_indef_sincos nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin const-decl "real" sincos_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil))
nil))
(Integral_sin 0
(Integral_sin-1 nil 3572800390
("" (skosimp*)
(("" (lemma "fundamental_indef[T]")
((""
(inst - "t1!1" "t2!1"
"LAMBDA (t: T): v!1 * sin(theta!1 + w!1 * t)")
(("" (assert)
((""
(case-replace
"continuous?(LAMBDA (t: T): v!1 * sin(w!1 * t + theta!1))")
(("1" (flatten)
(("1" (hide -1 -2 1)
(("1" (lemma "integral_sin")
(("1" (inst - "theta!1" "v!1" "w!1")
(("1" (assert)
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "+")
(("1"
(expand "const_fun")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (auto-rewrite-theory "continuous_lambda[T]")
(("2" (hide -1 -2 2 3)
(("2" (lemma "scal_mult_cont[T]")
(("2"
(inst - "(LAMBDA (t: T): sin(w!1 * t + theta!1))"
"v!1")
(("2" (hide 2)
(("2" (lemma "composition_cont_fun[T, real]")
(("2" (expand "o")
(("2"
(inst - "(LAMBDA(t:T):w!1 * t + theta!1)"
"(LAMBDA(t:real): sin(t))")
(("2" (assert)
(("2"
(hide 2)
(("2"
(lemma "sin_cont_fun")
(("2"
(case-replace
"(LAMBDA(t:real):sin(t))=sin")
(("2"
(apply-extensionality 1)
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 integral_indef_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_indef_sincos 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)
(fundamental_indef formula-decl nil indefinite_integral
"analysis/")
(cos_range application-judgement "trig_range" sincos_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(scal_mult_cont formula-decl nil continuous_lambda "analysis/")
(O const-decl "T3" function_props nil)
(const_cont formula-decl nil continuous_lambda "analysis/")
(id_cont formula-decl nil continuous_lambda "analysis/")
(add_cont formula-decl nil continuous_lambda "analysis/")
(sin_cont_fun formula-decl nil sincos nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(composition_cont_fun formula-decl nil composition_continuous
"analysis/")
(theta!1 skolem-const-decl "real" integral_indef_sincos nil)
(w!1 skolem-const-decl "nzreal" integral_indef_sincos nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions
"analysis/")
(integral_sin formula-decl nil integral_indef_sincos nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(bool nonempty-type-eq-decl nil booleans nil)
(continuous? const-decl "bool" continuous_functions "analysis/")
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin const-decl "real" sincos_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil))
shostak))
(Integral_cos_TCC1 0
(Integral_cos_TCC1-1 nil 3577107599
("" (skosimp*)
(("" (lemma "derivable_Integrable?[T]")
(("1"
(inst - "t1!1" "t2!1"
" LAMBDA (t: T): v!1 * cos(theta!1 + w!1 * t)")
(("1" (assert)
(("1" (hide 3)
(("1" (lemma "derivable_cos_lin")
(("1" (inst - "w!1" "theta!1" "v!1*w!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)
("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil integral_indef_sincos nil)
(T_pred const-decl "[real -> boolean]" integral_indef_sincos 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)
(derivable_Integrable? formula-decl nil fundamental_theorem
"analysis/")
(connected? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(derivable_cos_lin formula-decl nil integral_indef_sincos nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(cos const-decl "real" sincos_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(not_one_element formula-decl nil integral_indef_sincos nil)
(connected_domain formula-decl nil integral_indef_sincos nil))
nil))
(Integral_cos 0
(Integral_cos-1 nil 3578057477
("" (skosimp*)
(("" (lemma "fundamental_indef[T]")
((""
(inst - "t1!1" "t2!1"
"LAMBDA (t: T): v!1 * cos(theta!1 + w!1 * t)")
((""
(case-replace
"continuous?(LAMBDA (t: T): v!1 * cos(w!1 * t + theta!1))")
(("1" (flatten)
(("1" (lemma "integral_cos")
(("1" (inst - "theta!1" "v!1" "w!1")
(("1" (assert)
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1 -2 -3)
(("1" (expand "+")
(("1" (expand "const_fun")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (auto-rewrite-theory "continuous_lambda[T]")
(("2" (hide -1)
(("2" (lemma "scal_mult_cont[T]")
(("2"
(inst - "(LAMBDA (t: T): cos(w!1 * t + theta!1))"
"v!1")
(("2" (hide 2)
(("2" (lemma "composition_cont_fun[T, real]")
(("2" (expand "o")
(("2"
(inst - "(LAMBDA(t:T):w!1 * t + theta!1)"
"(LAMBDA(t:real): cos(t))")
(("2" (assert)
(("2"
(hide 2)
(("2"
(lemma "cos_cont_fun")
(("2"
(case-replace
"(LAMBDA(t:real):cos(t))=cos")
(("2"
(apply-extensionality 1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.62 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.
|
