(interval_deriv
(deriv_domain_Xt 0
(deriv_domain_Xt-2 nil 3545779310
("" (typepred "X")
(("" (expand "StrictInterval?")
(("" (lemma "deriv_domain_closed")
(("" (inst - "lb(X)" "ub(X)")
(("" (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)
((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_plus_real_is_real application-judgement "real" reals nil)
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(|##| const-decl "bool" interval nil)
(Xt type-eq-decl nil interval_deriv nil)
(x!1 skolem-const-decl "Xt" interval_deriv nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(y!1 skolem-const-decl
"{u: nzreal | lb(X) <= u + x!1 AND u + x!1 <= ub(X)}"
interval_deriv nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(deriv_domain_closed formula-decl nil deriv_domain "analysis/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil))
nil)
(deriv_domain_Xt-1 nil 3472488588
("" (typepred "X")
(("" (expand "StrictlyProper?")
(("" (lemma "deriv_domain_closed")
(("" (inst - "lb(X)" "ub(X)")
(("" (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)
((deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(closed_interval type-eq-decl nil intervals_real "reals/")
(deriv_domain_closed formula-decl nil deriv_domain "analysis/")
(Interval type-eq-decl nil interval nil))
nil))
(IMP_derivatives_TCC1 0
(IMP_derivatives_TCC1-1 nil 3301761309
("" (lemma "deriv_domain_Xt") (("" (propax) nil nil)) nil)
((deriv_domain_Xt formula-decl nil interval_deriv nil)) shostak))
(IMP_derivatives_TCC2 0
(IMP_derivatives_TCC2-1 nil 3301761489
("" (expand "not_one_element?")
(("" (skeep)
(("" (typepred "x")
(("" (typepred "X")
(("" (inst 1 "if x=lb(X) then ub(X) else lb(X) endif")
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(x skolem-const-decl "Xt" interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(D_TCC1 0
(D_TCC1-1 nil 3304700431
("" (skosimp :preds? t)
(("" (expand "Diff?") (("" (propax) nil nil)) 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(Diffn?_TCC1 0
(Diffn?_TCC1-1 nil 3321368055
("" (skosimp*) (("" (assert) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(Diffn?_TCC2 0
(Diffn?_TCC2-1 nil 3321368055
("" (skosimp*) (("" (assert) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Diffn_derivn 0
(Diffn_derivn-2 nil 3445354344
("" (induct "n")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "Diffn?" 1)
(("2" (expand "derivable_n_times?" 1)
(("2" (expand "Diff?")
(("2" (inst -1 "D(f)")
(("1" (expand "D" -1 2) (("1" (replaces -1) nil nil))
nil)
("2" (expand "Diff?") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Diff? const-decl "bool" interval_deriv nil)
(D const-decl "[Xt -> real]" interval_deriv nil)
(f skolem-const-decl "[Xt -> real]" interval_deriv nil)
(nat_induction formula-decl nil naturalnumbers nil)
(derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
(Diffn? def-decl "bool" interval_deriv nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Xt type-eq-decl nil interval_deriv nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(StrictInterval type-eq-decl nil interval nil)
(StrictInterval? const-decl "bool" interval nil)
(|##| const-decl "bool" interval nil)
(Interval type-eq-decl nil interval nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(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)
(Diffn_derivn-1 nil 3321368515
("" (induct "n")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "Diffn?" 1)
(("2" (expand "derivable_n_times" 1)
(("2" (expand "Diff?")
(("2" (inst -1 "D(f)")
(("1" (expand "D" -1 2) (("1" (replaces -1) nil nil))
nil)
("2" (expand "Diff?") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Interval type-eq-decl nil interval nil)) shostak))
(Dn_TCC1 0
(Dn_TCC1-1 nil 3321368055 ("" (skosimp*) (("" (assert) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(Dn_TCC2 0
(Dn_TCC2-1 nil 3321368055
("" (skosimp* :preds? t)
(("" (expand "Diffn?") (("" (assert) nil nil)) nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diffn? def-decl "bool" interval_deriv nil))
nil))
(Dn_TCC3 0
(Dn_TCC3-1 nil 3321368055
("" (skosimp* :preds? t)
(("" (expand "Diffn?" -2) (("" (assert) nil nil)) nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diffn? def-decl "bool" interval_deriv nil))
nil))
(Dn_TCC4 0
(Dn_TCC4-1 nil 3321368055 ("" (skosimp) (("" (assert) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Dn_nderiv_TCC1 0
(Dn_nderiv_TCC1-1 nil 3321368411
("" (skosimp* :preds? t)
(("" (lemma "Diffn_derivn")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((Diffn_derivn formula-decl nil interval_deriv nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diffn? def-decl "bool" interval_deriv nil))
nil))
(Dn_nderiv 0
(Dn_nderiv-1 nil 3321368706
("" (induct "n")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (skeep :preds? t)
(("2" (expand "Dn" 1)
(("2" (expand "nderiv" 1)
(("2" (expand "Diffn?" -1)
(("2" (flatten)
(("2" (inst -3 "D(f)")
(("2" (expand "D" -3 2) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skeep :preds? t) (("3" (rewrite "Diffn_derivn") nil nil))
nil))
nil))
nil)
((Diffn_derivn formula-decl nil interval_deriv nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(D const-decl "[Xt -> real]" interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
(nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
(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)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diffn? def-decl "bool" interval_deriv nil)
(derivable_n_times? def-decl "bool" nth_derivatives "analysis/"))
shostak))
(Diff_id 0
(Diff_id-1 nil 3304425174
("" (expand "Diff?")
(("" (lemma "derivable_id")
(("" (expand "I") (("" (propax) nil nil)) nil)) nil))
nil)
((Xt type-eq-decl nil interval_deriv nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(StrictInterval type-eq-decl nil interval 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)
(derivable_id judgement-tcc nil derivatives "analysis/")
(I const-decl "(bijective?[T, T])" identity nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_id_TCC1 0
(D_id_TCC1-1 nil 3304424118 ("" (rewrite "Diff_id") nil nil)
((Diff_id formula-decl nil interval_deriv nil)) shostak))
(D_id 0
(D_id-1 nil 3304429116
("" (expand "D")
(("" (lemma "deriv_id_fun")
(("" (expand "I")
(("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((Xt type-eq-decl nil interval_deriv nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(StrictInterval type-eq-decl nil interval 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)
(deriv_id_fun formula-decl nil derivatives "analysis/")
(D const-decl "[Xt -> real]" interval_deriv nil))
shostak))
(Diff_const 0
(Diff_const-1 nil 3304425582
("" (skosimp)
(("" (expand "Diff?")
(("" (lemma "derivable_const")
(("" (inst?)
(("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((Diff? const-decl "bool" interval_deriv nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_const judgement-tcc nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil))
shostak))
(D_const_TCC1 0
(D_const_TCC1-1 nil 3304424144
("" (skosimp) (("" (rewrite "Diff_const") nil nil)) nil)
((Diff_const formula-decl nil interval_deriv 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))
shostak))
(D_const 0
(D_const-1 nil 3304430079
("" (skosimp)
(("" (expand "D")
(("" (lemma "deriv_const_fun")
(("" (inst -1 "a!1")
(("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv nil)
(deriv_const_fun formula-decl nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil))
shostak))
(Diff_add 0
(Diff_add-1 nil 3304429143
("" (skosimp :preds? t)
(("" (expand "Diff?")
(("" (lemma "derivable_sum")
(("" (inst -1 "f!1" "g!1")
(("" (expand "+") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_sum judgement-tcc nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
nil))
(D_add_TCC1 0
(D_add_TCC1-1 nil 3304424494
("" (skosimp) (("" (rewrite "Diff_add") nil nil)) nil)
((Diff_add formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_add 0
(D_add-1 nil 3304430121
("" (skosimp :preds? t)
(("" (expand* "Diff?" "D")
(("" (lemma "deriv_sum_fun")
(("" (inst -1 "f!1" "g!1")
(("" (expand "+") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_sum_fun formula-decl nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(Diff_mult 0
(Diff_mult-1 nil 3304429240
("" (skosimp :preds? t)
(("" (expand "Diff?")
(("" (lemma "derivable_prod")
(("" (inst -1 "f!1" "g!1")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_prod judgement-tcc nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_mult_TCC1 0
(D_mult_TCC1-1 nil 3304424503
("" (skosimp) (("" (rewrite "Diff_mult") nil nil)) nil)
((Diff_mult formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_mult 0
(D_mult-1 nil 3304430162
("" (skosimp :preds? t)
(("" (expand* "Diff?" "D")
(("" (lemma "deriv_prod_fun")
(("" (inst -1 "f!1" "g!1")
(("" (expand "*")
(("" (expand "+") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_prod_fun formula-decl nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(Diff_pow_TCC1 0
(Diff_pow_TCC1-1 nil 3305042267 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) shostak))
(Diff_pow 0
(Diff_pow-1 nil 3305042471
("" (skeep)
(("" (case "n=0")
(("1" (replaces)
(("1" (expand "^")
(("1" (expand "expt") (("1" (rewrite "Diff_const") nil nil))
nil))
nil))
nil)
("2" (expand "Diff?")
(("2" (lemma "deriv_x_to_n")
(("2" (inst -1 "n" "1")
(("1" (beta) (("1" (flatten) (("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers 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)
(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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(^ const-decl "real" exponentiation nil)
(Diff_const formula-decl nil interval_deriv nil)
(expt def-decl "real" exponentiation nil)
(deriv_x_to_n formula-decl nil derivatives "analysis/")
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(n skolem-const-decl "nat" interval_deriv nil)
(> const-decl "bool" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_pow_TCC1 0
(D_pow_TCC1-1 nil 3305042277 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) shostak))
(D_pow_TCC2 0
(D_pow_TCC2-1 nil 3305042285
("" (skosimp) (("" (rewrite "Diff_pow") nil nil)) nil)
((Diff_pow formula-decl nil interval_deriv 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil))
shostak))
(D_pow_TCC3 0
(D_pow_TCC3-1 nil 3305042306 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) shostak))
(D_pow 0
(D_pow-1 nil 3305042697
("" (skeep)
(("" (expand "D")
(("" (lemma "deriv_x_to_n")
(("" (inst -1 "m" "1")
(("" (beta) (("" (flatten) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv 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)
(real_times_real_is_real application-judgement "real" reals nil)
(deriv_x_to_n formula-decl nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil))
shostak))
(Diff_scal1 0
(Diff_scal1-2 nil 3304699767
("" (skosimp :preds? t)
(("" (expand "Diff?")
(("" (lemma "derivable_scal")
(("" (inst -1 "a!1" "f!1")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_scal judgement-tcc nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
nil))
(D_scal1_TCC1 0
(D_scal1_TCC1-2 nil 3304431213
("" (skosimp) (("" (rewrite "Diff_scal1") nil nil)) nil)
((Diff_scal1 formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
nil))
(D_scal1 0
(D_scal1-1 nil 3304431129
("" (skosimp :preds? t)
(("" (expand* "Diff?" "D")
(("" (lemma "deriv_scal_fun")
(("" (inst -1 "a!1" "f!1")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_scal_fun formula-decl nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
nil))
(Diff_scal2 0
(Diff_scal2-1 nil 3304431294
("" (skosimp :preds? t)
(("" (lemma "Diff_scal1")
(("" (inst -1 "a!1" "f!1") (("" (assert) nil nil)) nil)) nil))
nil)
((Diff_scal1 formula-decl nil interval_deriv nil)
(real_times_real_is_real application-judgement "real" reals 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_scal2_TCC1 0
(D_scal2_TCC1-2 nil 3304431448
("" (skosimp) (("" (rewrite "Diff_scal2") nil nil)) nil)
((Diff_scal2 formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
nil))
(D_scal2 0
(D_scal2-1 nil 3304431330
("" (skosimp :preds? t)
(("" (lemma "D_scal1")
(("" (inst -1 "a!1" "f!1") (("" (assert) nil nil)) nil)) nil))
nil)
((D_scal1 formula-decl nil interval_deriv nil)
(real_times_real_is_real application-judgement "real" reals 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(Diff_neg 0
(Diff_neg-2 nil 3442593099
("" (skosimp :preds? t)
(("" (expand "Diff?")
(("" (lemma "derivable_neg")
(("" (inst -1 "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((minus_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_neg judgement-tcc nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
nil)
(Diff_neg-1 nil 3304429291
("" (skosimp :preds? t)
(("" (expand "Diff?")
(("" (lemma "derivable_opp")
(("" (inst -1 "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((deriv_fun type-eq-decl nil derivatives "analysis/")
(Interval type-eq-decl nil interval nil))
shostak))
(D_neg_TCC1 0
(D_neg_TCC1-1 nil 3304424526
("" (skosimp) (("" (rewrite "Diff_neg") nil nil)) nil)
((Diff_neg formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_neg 0
(D_neg-2 nil 3442592991
("" (skosimp :preds? t)
(("" (expand* "Diff?" "D")
(("" (lemma "deriv_neg_fun")
(("" (inst -1 "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv nil)
(derivable? const-decl "bool" derivatives "analysis/")
(g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_neg_fun formula-decl nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
nil)
(D_neg-1 nil 3304430224
("" (skosimp :preds? t)
(("" (expand* "Diff?" "D")
(("" (lemma "deriv_opp_fun")
(("" (inst -1 "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((deriv_fun type-eq-decl nil derivatives "analysis/")
(Interval type-eq-decl nil interval nil))
shostak))
(Diff_sub 0
(Diff_sub-1 nil 3304429323
("" (skosimp :preds? t)
(("" (expand "Diff?")
(("" (lemma "derivable_diff")
(("" (inst -1 "f!1" "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_diff judgement-tcc nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_sub_TCC1 0
(D_sub_TCC1-1 nil 3304424618
("" (skosimp) (("" (rewrite "Diff_sub") nil nil)) nil)
((Diff_sub formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(D_sub 0
(D_sub-1 nil 3304430250
("" (skosimp :preds? t)
(("" (expand* "Diff?" "D")
(("" (lemma "deriv_diff_fun")
(("" (inst -1 "f!1" "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_diff_fun formula-decl nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil))
shostak))
(Diff_sq 0
(Diff_sq-1 nil 3304429366
("" (expand "sq")
(("" (rewrite "Diff_mult") (("" (rewrite "Diff_id") nil nil)) nil))
nil)
((Diff_mult formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(Diff_id formula-decl nil interval_deriv nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(D_sq_TCC1 0
(D_sq_TCC1-1 nil 3304424624 ("" (rewrite "Diff_sq") nil nil)
((Diff_sq formula-decl nil interval_deriv nil)) shostak))
(D_sq 0
(D_sq-1 nil 3304430266
("" (expand "sq")
(("" (rewrite "D_mult")
(("1" (rewrite "D_id") (("1" (assert) nil nil)) nil)
("2" (rewrite "Diff_id") nil nil))
nil))
nil)
((D_mult formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(D_id formula-decl nil interval_deriv nil)
(Diff_id formula-decl nil interval_deriv nil)
(sq const-decl "nonneg_real" sq "reals/"))
shostak))
(Diff_div_TCC1 0
(Diff_div_TCC1-1 nil 3304431499
("" (skosimp :preds? t)
(("" (inst -2 "t!1") (("" (assert) nil nil)) 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(/= const-decl "boolean" notequal nil))
shostak))
(Diff_div 0
(Diff_div-1 nil 3304431982
("" (skosimp :preds? t)
(("" (expand "Diff?")
(("" (lemma "derivable_div")
(("" (inst -1 "f!1" "k!1")
(("1" (expand "/") (("1" (propax) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(k!1 skolem-const-decl "(LAMBDA (f): FORALL (t: Xt): f(t) /= 0)"
interval_deriv nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives "analysis/")
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_div judgement-tcc nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(/= const-decl "boolean" notequal nil))
shostak))
(D_div_TCC1 0
(D_div_TCC1-1 nil 3304431524
("" (skosimp :preds? t) (("" (rewrite "Diff_div") nil nil)) nil)
((Diff_div formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(/= const-decl "boolean" notequal nil))
shostak))
(D_div_TCC2 0
(D_div_TCC2-1 nil 3304431579
("" (skosimp :preds? t)
(("" (inst -2 "t!1")
(("" (hide -1 -3)
(("" (expand "sq") (("" (grind-reals) nil nil)) nil)) nil))
nil))
nil)
((sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(nonzero_times3 formula-decl nil real_props 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(/= const-decl "boolean" notequal nil))
shostak))
(D_div 0
(D_div-1 nil 3304432155
("" (skosimp :preds? t)
(("" (expand* "Diff?" "D")
(("" (lemma "deriv_div_fun")
(("" (inst -1 "f!1" "k!1")
(("1" (expand "/")
(("1" (expand "sq")
(("1" (expand "*")
(("1" (assert)
(("1" (expand "-") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv nil)
(real_times_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(k!1 skolem-const-decl "(LAMBDA (f): FORALL (t: Xt): f(t) /= 0)"
interval_deriv nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives "analysis/")
(sq const-decl "nonneg_real" sq "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_div_fun formula-decl nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(/= const-decl "boolean" notequal nil))
shostak))
(Diff_scald1 0
(Diff_scald1-1 nil 3304432031
("" (skosimp :preds? t)
(("" (expand "Diff?")
(("" (lemma "derivable_div")
(("" (inst -1 "LAMBDA(t):a!1" "k!1")
(("1" (expand "/") (("1" (propax) nil nil)) nil)
("2" (assert) nil nil)
("3" (hide 2)
(("3" (lemma "derivable_const")
(("3" (expand "const_fun") (("3" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives "analysis/")
(a!1 skolem-const-decl "real" interval_deriv nil)
(k!1 skolem-const-decl "(LAMBDA (f): FORALL (t: Xt): f(t) /= 0)"
interval_deriv nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(deriv_fun type-eq-decl nil derivatives "analysis/")
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives "analysis/")
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_const judgement-tcc nil derivatives "analysis/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_div judgement-tcc nil derivatives "analysis/")
(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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(/= const-decl "boolean" notequal nil))
shostak))
(D_scald1_TCC1 0
(D_scald1_TCC1-1 nil 3304431707
("" (skosimp :preds? t) (("" (rewrite "Diff_scald1") nil nil)) nil)
((Diff_scald1 formula-decl nil interval_deriv 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_deriv nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(/= const-decl "boolean" notequal nil))
shostak))
(D_scald1 0
(D_scald1-1 nil 3304432324
("" (skosimp :preds? t)
(("" (expand* "Diff?" "D")
(("" (lemma "deriv_scaldiv_fun")
(("" (inst -1 "a!1" "k!1")
(("1" (expand "/")
(("1" (expand "-")
(("1" (expand "*")
(("1" (expand "sq") (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((D const-decl "[Xt -> real]" interval_deriv nil)
(derivable? const-decl "bool" derivatives "analysis/")
(k!1 skolem-const-decl "(LAMBDA (f): FORALL (t: Xt): f(t) /= 0)"
interval_deriv nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives "analysis/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_scaldiv_fun formula-decl nil derivatives "analysis/")
(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
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.32Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
*Bot Zugriff
|
|
