|
(subinterval_deriv
(deriv_domain_Xt 0
(deriv_domain_Xt-2 nil 3545779475
("" (skosimp*)
(("" (typepred "X!1")
(("" (expand "StrictInterval?")
(("" (lemma "deriv_domain_closed")
(("" (inst - "lb(X!1)" "ub(X!1)")
(("" (assert)
(("" (expand "deriv_domain?")
(("" (skosimp*)
(("" (inst - "e!1" "x!1")
(("1" (skosimp*)
(("1" (inst + "y!1") (("1" (grind) nil nil))
nil))
nil)
("2" (assert)
(("2" (hide 2)
(("2" (typepred "x!1")
(("2" (expand "##") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((StrictInterval? const-decl "bool" interval nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(deriv_domain_closed formula-decl nil deriv_domain "analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(y!1 skolem-const-decl
"{u: nzreal | lb(X!1) <= u + x!1 AND u + x!1 <= ub(X!1)}"
subinterval_deriv nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(X!1 skolem-const-decl "(StrictInterval?)" subinterval_deriv nil)
(|##| const-decl "bool" interval nil)
(Xt type-eq-decl nil interval_deriv nil)
(x!1 skolem-const-decl "Xt[X!1]" subinterval_deriv nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(real_plus_real_is_real application-judgement "real" 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)
(number nonempty-type-decl nil numbers nil))
nil)
(deriv_domain_Xt-1 nil 3472488092
("" (skosimp*)
(("" (typepred "X!1")
(("" (expand "StrictlyProper?")
(("" (lemma "deriv_domain_closed")
(("" (inst - "lb(X!1)" "ub(X!1)")
(("" (assert)
(("" (expand "deriv_domain?")
(("" (skosimp*)
(("" (inst - "e!1" "x!1")
(("1" (skosimp*)
(("1" (inst + "y!1") (("1" (grind) nil nil))
nil))
nil)
("2" (assert)
(("2" (hide 2)
(("2" (typepred "x!1")
(("2" (expand "##") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Interval type-eq-decl nil interval nil)
(deriv_domain_closed formula-decl nil deriv_domain "analysis/")
(closed_interval type-eq-decl nil intervals_real "reals/")
(Xt type-eq-decl nil interval_deriv nil)
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(subinterval_deriv_TCC1 0
(subinterval_deriv_TCC1-1 nil 3350435325 ("" (subtype-tcc) nil nil)
((StrictInterval? const-decl "bool" interval nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(Xt type-eq-decl nil interval_deriv nil)
(<< const-decl "bool" interval nil)
(fullset const-decl "set" sets nil)
(adh const-decl "setof[real]" convergence_functions "analysis/")
(NQ const-decl "real" derivatives_def "analysis/")
(convergence const-decl "bool" convergence_functions "analysis/")
(convergence const-decl "bool" lim_of_functions "analysis/")
(convergent? const-decl "bool" lim_of_functions "analysis/")
(derivable? const-decl "bool" derivatives_def "analysis/")
(derivable? const-decl "bool" derivatives "analysis/")
(Diff? const-decl "bool" interval_deriv nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(|##| const-decl "bool" interval nil))
nil))
(subinterval_deriv 0
(subinterval_deriv-2 nil 3472488084
("" (skeep :preds? t)
(("" (lemma "restrict2_derivable[Xt[Y],Xt[X]]")
(("1" (inst -1 "f")
(("1" (expand "restrict2")
(("1" (expand "Diff?" 1)
(("1" (assert)
(("1" (lemma "restrict2_deriv[Xt[Y],Xt[X]]")
(("1" (decompose-equality 1)
(("1" (inst -1 "x!1" f)
(("1" (expand "restrict2")
(("1" (expand "D")
(("1" (replaces -1 :dir rl) nil nil)) nil))
nil)
("2" (expand "Diff?") (("2" (propax) nil nil))
nil))
nil)
("2" (expand "Diff?") (("2" (propax) nil nil)) nil)
("3" (hide-all-but (-5 1)) (("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "Diff?" -4) (("2" (propax) nil nil)) nil))
nil)
("2" (skeep)
(("2" (inst 1 "x")
(("2" (typepred "x")
(("2" (hide-all-but (-1 -4 1)) (("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("3" (hide -4 2)
(("3" (expand "not_one_element?")
(("3" (skeep)
(("3" (case "x=lb(X)")
(("1" (inst 1 "ub(X)")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("4" (hide -4 2)
(("4" (expand "not_one_element?")
(("4" (skeep)
(("4" (case "x=lb(Y)")
(("1" (inst 1 "ub(Y)")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("5" (hide -4 2) (("5" (rewrite "deriv_domain_Xt") nil nil))
nil)
("6" (hide -4 2) (("6" (rewrite "deriv_domain_Xt") nil nil))
nil))
nil))
nil)
((Xt type-eq-decl nil interval_deriv nil)
(StrictInterval? const-decl "bool" interval nil)
(|##| const-decl "bool" interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Interval type-eq-decl nil interval 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)
(restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(= const-decl "[T, T -> boolean]" equalities nil)
(restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
(Y skolem-const-decl "(StrictInterval?)" subinterval_deriv nil)
(D const-decl "[Xt -> real]" interval_deriv nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<< const-decl "bool" interval nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
(Diff? const-decl "bool" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(X skolem-const-decl "(StrictInterval?)" subinterval_deriv nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f skolem-const-decl "[Xt[X] -> real]" subinterval_deriv nil)
(x skolem-const-decl "Xt[Y]" subinterval_deriv nil)
(/= const-decl "boolean" notequal nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(deriv_domain_Xt formula-decl nil subinterval_deriv nil))
nil)
(subinterval_deriv-1 nil 3350435426
("" (skeep :preds? t)
(("" (lemma "restrict2_derivable[Xt[Y],Xt[X]]")
(("1" (inst -1 "f")
(("1" (expand "restrict2")
(("1" (expand "Diff?" 1)
(("1" (assert)
(("1" (lemma "restrict2_deriv[Xt[Y],Xt[X]]")
(("1" (decompose-equality 1)
(("1" (inst -1 "x!1" f)
(("1" (expand "restrict2")
(("1" (expand "D")
(("1" (replaces -1 :dir rl) nil nil)) nil))
nil)
("2" (expand "Diff?") (("2" (propax) nil nil))
nil))
nil)
("2" (expand "Diff?") (("2" (propax) nil nil)) nil)
("3" (hide-all-but (-5 1)) (("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "Diff?" -4) (("2" (propax) nil nil)) nil))
nil)
("2" (skeep)
(("2" (inst 1 "x")
(("2" (typepred "x")
(("2" (hide-all-but (-1 -4 1)) (("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("3" (hide -4 2)
(("3" (skeep)
(("3" (case "x=lb(X)")
(("1" (inst 1 "ub(X)")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil)
("4" (hide -4 2)
(("4" (skeep)
(("4" (case "x=lb(Y)")
(("1" (inst 1 "ub(Y)")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil)
("5" (hide -4 2) (("5" (rewrite "deriv_domain_XtY") nil nil))
nil)
("6" (hide -4 2) (("6" (rewrite "deriv_domain_XtY") nil nil))
nil))
nil))
nil)
((derivable? const-decl "bool" derivatives "analysis/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(Diff? const-decl "bool" interval_deriv nil)
(restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
(<< const-decl "bool" interval nil)
(D const-decl "[Xt -> real]" interval_deriv nil)
(restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
(Interval type-eq-decl nil interval nil)
(Xt type-eq-decl nil interval_deriv nil))
shostak))
(subinterval_derivn_TCC1 0
(subinterval_derivn_TCC1-1 nil 3350435325 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" 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)
(>= const-decl "bool" reals 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Interval type-eq-decl nil interval nil)
(StrictInterval? const-decl "bool" interval nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Xt type-eq-decl nil interval_deriv nil)
(<< const-decl "bool" interval nil)
(|##| const-decl "bool" interval nil))
nil))
(subinterval_derivn 0
(subinterval_derivn-1 nil 3350512779
("" (induct "n")
(("1" (skeep)
(("1" (expand "Diffn?")
(("1" (expand "Dn") (("1" (propax) nil nil)) nil)) nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "Diffn?" 1)
(("2" (expand "Dn" 1)
(("2" (expand "Diffn?" -3)
(("2" (flatten)
(("2" (inst -1 "X" "Y" "D(f)")
(("2" (assert)
(("2" (flatten)
(("2" (lemma "subinterval_deriv")
(("2" (inst -1 "X" "Y" "f")
(("2" (assert)
(("2" (flatten) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skeep) (("3" (hide -1 -3) (("3" (grind) nil nil)) nil))
nil))
nil)
("4" (hide 2)
(("4" (skeep)
(("4" (match "Diffn?" step (hide $1n)) (("4" (grind) nil nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(D const-decl "[Xt -> real]" interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(subinterval_deriv formula-decl nil subinterval_deriv nil)
(nat_induction formula-decl nil naturalnumbers nil)
(Dn def-decl "[Xt -> real]" interval_deriv nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types 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)
(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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Interval type-eq-decl nil interval nil)
(StrictInterval? const-decl "bool" interval nil)
(|##| const-decl "bool" interval nil)
(Xt type-eq-decl nil interval_deriv nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<< const-decl "bool" interval nil)
(Diffn? def-decl "bool" interval_deriv nil))
shostak)))
¤ Dauer der Verarbeitung: 0.58 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.
|
