|
(derivatives_lam
(IMP_derivatives_TCC1 0
(IMP_derivatives_TCC1-1 nil 3301761309
("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
((deriv_domain formula-decl nil derivatives_lam nil)) shostak))
(IMP_derivatives_TCC2 0
(IMP_derivatives_TCC2-1 nil 3301761489
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil derivatives_lam nil)) shostak))
(derivable_id_lam 0
(derivable_id_lam-1 nil 3304425174
("" (expand "derivable?")
(("" (lemma "derivable_id")
(("" (expand "I")
(("" (skeep)
(("" (expand "derivable?" -1) (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil)
((T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam 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 nil)
(I const-decl "(bijective?[T, T])" identity nil)
(derivable? const-decl "bool" derivatives nil))
shostak))
(derivable_const_lam 0
(derivable_const_lam-1 nil 3304425582
("" (skosimp*)
(("" (lemma "const_derivable_fun")
(("" (inst?)
(("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam 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)
(const_derivable_fun formula-decl nil derivatives nil))
shostak))
(derivable_add_lam 0
(derivable_add_lam-1 nil 3304429143
("" (skosimp :preds? t)
(("" (lemma "sum_derivable_fun")
(("" (inst - "f!1" "g!1")
(("" (expand "+ ") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((sum_derivable_fun formula-decl nil derivatives nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil))
(derivable_mult_lam 0
(derivable_mult_lam-1 nil 3304429240
("" (skosimp*)
(("" (lemma "prod_derivable_fun")
(("" (inst - "f!1" "g!1")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam 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)
(prod_derivable_fun formula-decl nil derivatives nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil))
shostak))
(derivable_pow_lam_TCC1 0
(derivable_pow_lam_TCC1-1 nil 3305042267 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) shostak))
(derivable_pow_lam 0
(derivable_pow_lam-1 nil 3305042471
("" (skosimp*)
(("" (case-replace "n!1=0")
(("1" (expand "^")
(("1" (expand "expt")
(("1" (rewrite "derivable_const_lam") nil nil)) nil))
nil)
("2" (lemma "deriv_x_to_n")
(("2" (inst - "n!1" "1")
(("1" (assert)
(("1" (flatten)
(("1"
(case-replace
"(LAMBDA (t): t ^ n!1) = (LAMBDA (x: T): 1 * x ^ n!1)")
(("1" (apply-extensionality 1 :hide? t) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(expt def-decl "real" exponentiation nil)
(derivable_const_lam formula-decl nil derivatives_lam nil)
(^ const-decl "real" exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(n!1 skolem-const-decl "nat" derivatives_lam nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(deriv_x_to_n formula-decl nil derivatives nil))
shostak))
(derivable_scal1_lam 0
(derivable_scal1_lam-2 nil 3304699767
("" (skosimp :preds? t)
(("" (lemma "scal_derivable_fun")
(("" (inst - "a!1" "f!1")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((scal_derivable_fun formula-decl nil derivatives nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil))
(derivable_scal2_lam 0
(derivable_scal2_lam-2 nil 3472317982
("" (skosimp :preds? t)
(("" (lemma "scal_derivable_fun")
(("" (inst - "a!1" "f!1")
(("" (expand "*")
((""
(case-replace
"(LAMBDA (x: T): a!1 * f!1(x)) = (LAMBDA (t): f!1(t) * a!1)")
(("" (apply-extensionality 1 :hide? t) nil nil)) nil))
nil))
nil))
nil))
nil)
((scal_derivable_fun formula-decl nil derivatives nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil)
(derivable_scal2_lam-1 nil 3304431294
("" (skosimp :preds? t)
(("" (lemma "derivable_scal1_lam")
(("" (inst -1 "a!1" "f!1") (("" (assert) nil nil)) nil)) nil))
nil)
((derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(derivable_neg_lam 0
(derivable_neg_lam-2 nil 3442593099
("" (skosimp*)
(("" (lemma "neg_derivable_fun")
(("" (inst - "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam 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)
(neg_derivable_fun formula-decl nil derivatives nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil))
nil)
(derivable_neg_lam-1 nil 3304429291
("" (skosimp :preds? t)
(("" (expand "derivable?")
(("" (lemma "derivable_opp")
(("" (inst -1 "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((deriv_fun type-eq-decl nil derivatives nil)) shostak))
(derivable_sub_lam 0
(derivable_sub_lam-1 nil 3304429323
("" (skosimp :preds? t)
(("" (lemma "diff_derivable_fun")
(("" (inst - "f!1" "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((diff_derivable_fun formula-decl nil derivatives nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(derivable_sq_lam 0
(derivable_sq_lam-1 nil 3304429366
("" (expand "sq")
(("" (rewrite "derivable_mult_lam")
(("" (rewrite "derivable_id_lam") nil nil)) nil))
nil)
((derivable_mult_lam formula-decl nil derivatives_lam nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable_id_lam formula-decl nil derivatives_lam nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(derivable_div_lam 0
(derivable_div_lam-1 nil 3304431982
("" (skosimp :preds? t)
(("" (lemma "div_derivable_fun")
(("" (inst - "f!1" "k!1")
(("" (expand "/") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((div_derivable_fun formula-decl nil derivatives nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives nil))
shostak))
(derivable_scald1_lam 0
(derivable_scald1_lam-1 nil 3304432031
("" (skosimp :preds? t)
(("" (lemma "derivable_div")
(("" (inst -1 "LAMBDA(t):a!1" "k!1")
(("1" (expand "/") (("1" (propax) nil nil)) nil)
("2" (lemma "derivable_const")
(("2" (expand "const_fun") (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil)
((derivable_div judgement-tcc nil derivatives nil)
(derivable_const judgement-tcc nil derivatives nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_fun type-eq-decl nil derivatives nil)
(a!1 skolem-const-decl "real" derivatives_lam 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives nil))
shostak))
(derivable_scald2_lam 0
(derivable_scald2_lam-1 nil 3304432497
("" (skosimp)
(("" (lemma "derivable_scal1_lam")
(("" (inst -1 "1/b!1" "f!1") (("" (assert) nil nil)) nil)) nil))
nil)
((derivable_scal1_lam formula-decl nil derivatives_lam nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam 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)
(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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
shostak))
(deriv_id_lam_TCC1 0
(deriv_id_lam_TCC1-1 nil 3304424118
("" (rewrite "derivable_id_lam") nil nil)
((derivable_id_lam formula-decl nil derivatives_lam nil)) shostak))
(deriv_id_lam 0
(deriv_id_lam-1 nil 3304429116
("" (expand "D")
(("" (lemma "deriv_id_fun")
(("" (expand "I")
(("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((deriv_id_fun formula-decl nil derivatives nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil))
shostak))
(deriv_const_lam_TCC1 0
(deriv_const_lam_TCC1-1 nil 3304424144
("" (skosimp) (("" (rewrite "derivable_const_lam") nil nil)) nil)
((derivable_const_lam formula-decl nil derivatives_lam 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))
(deriv_const_lam 0
(deriv_const_lam-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)
((T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam 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_const_fun formula-decl nil derivatives nil))
shostak))
(deriv_add_lam_TCC1 0
(deriv_add_lam_TCC1-1 nil 3304424494
("" (skosimp) (("" (rewrite "derivable_add_lam") nil nil)) nil)
((derivable_add_lam formula-decl nil derivatives_lam nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_add_lam 0
(deriv_add_lam-1 nil 3304430121
("" (skosimp :preds? t)
(("" (expand* "derivable?" "D")
(("" (lemma "deriv_sum_fun")
(("" (inst -1 "f!1" "g!1")
(("" (expand "+") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((+ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_sum_fun formula-decl nil derivatives 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_mult_lam_TCC1 0
(deriv_mult_lam_TCC1-1 nil 3304424503
("" (skosimp) (("" (rewrite "derivable_mult_lam") nil nil)) nil)
((derivable_mult_lam formula-decl nil derivatives_lam nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_mult_lam 0
(deriv_mult_lam-1 nil 3304430162
("" (skosimp :preds? t)
(("" (expand* "derivable?" "D")
(("" (lemma "deriv_prod_fun")
(("" (inst -1 "f!1" "g!1")
(("" (expand "*")
(("" (expand "+") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((+ const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_prod_fun formula-decl nil derivatives 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_pow_lam_TCC1 0
(deriv_pow_lam_TCC1-1 nil 3305042277 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) shostak))
(deriv_pow_lam_TCC2 0
(deriv_pow_lam_TCC2-1 nil 3305042285
("" (skosimp) (("" (rewrite "derivable_pow_lam") nil nil)) nil)
((derivable_pow_lam formula-decl nil derivatives_lam 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))
(deriv_pow_lam_TCC3 0
(deriv_pow_lam_TCC3-1 nil 3305042306 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) shostak))
(deriv_pow_lam 0
(deriv_pow_lam-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)
((T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam 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_x_to_n formula-decl nil derivatives nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil))
shostak))
(deriv_scal1_lam_TCC1 0
(deriv_scal1_lam_TCC1-2 nil 3304431213
("" (skosimp) (("" (rewrite "derivable_scal1_lam") nil nil)) nil)
((derivable_scal1_lam formula-decl nil derivatives_lam nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil))
(deriv_scal1_lam 0
(deriv_scal1_lam-1 nil 3304431129
("" (skosimp :preds? t)
(("" (expand* "derivable?" "D")
(("" (lemma "deriv_scal_fun")
(("" (inst -1 "a!1" "f!1")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_scal_fun formula-decl nil derivatives 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil))
(deriv_scal2_lam_TCC1 0
(deriv_scal2_lam_TCC1-2 nil 3304431448
("" (skosimp) (("" (rewrite "derivable_scal2_lam") nil nil)) nil)
((derivable_scal2_lam formula-decl nil derivatives_lam nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil))
(deriv_scal2_lam 0
(deriv_scal2_lam-1 nil 3304431330
("" (skosimp :preds? t)
(("" (lemma "deriv_scal1_lam")
(("" (inst -1 "a!1" "f!1") (("" (assert) nil nil)) nil)) nil))
nil)
((deriv_scal1_lam formula-decl nil derivatives_lam 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_neg_lam_TCC1 0
(deriv_neg_lam_TCC1-1 nil 3304424526
("" (skosimp) (("" (rewrite "derivable_neg_lam") nil nil)) nil)
((derivable_neg_lam formula-decl nil derivatives_lam nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_neg_lam 0
(deriv_neg_lam-2 nil 3442592991
("" (skosimp :preds? t)
(("" (expand* "derivable?" "D")
(("" (lemma "deriv_neg_fun")
(("" (inst -1 "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((- const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_neg_fun formula-decl nil derivatives 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
nil)
(deriv_neg_lam-1 nil 3304430224
("" (skosimp :preds? t)
(("" (expand* "derivable?" "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 nil)) shostak))
(deriv_sub_lam_TCC1 0
(deriv_sub_lam_TCC1-1 nil 3304424618
("" (skosimp) (("" (rewrite "derivable_sub_lam") nil nil)) nil)
((derivable_sub_lam formula-decl nil derivatives_lam nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_sub_lam 0
(deriv_sub_lam-1 nil 3304430250
("" (skosimp :preds? t)
(("" (expand* "derivable?" "D")
(("" (lemma "deriv_diff_fun")
(("" (inst -1 "f!1" "g!1")
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((- const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_diff_fun formula-decl nil derivatives 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_sq_lam_TCC1 0
(deriv_sq_lam_TCC1-1 nil 3304424624
("" (rewrite "derivable_sq_lam") nil nil)
((derivable_sq_lam formula-decl nil derivatives_lam nil)) shostak))
(deriv_sq_lam 0
(deriv_sq_lam-1 nil 3304430266
("" (expand "sq")
(("" (rewrite "deriv_mult_lam")
(("1" (rewrite "deriv_id_lam") (("1" (assert) nil nil)) nil)
("2" (rewrite "derivable_id_lam") nil nil))
nil))
nil)
((deriv_mult_lam formula-decl nil derivatives_lam nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(deriv_id_lam formula-decl nil derivatives_lam nil)
(derivable_id_lam formula-decl nil derivatives_lam nil)
(sq const-decl "nonneg_real" sq "reals/"))
shostak))
(deriv_div_lam_TCC1 0
(deriv_div_lam_TCC1-1 nil 3304431524
("" (skosimp :preds? t) (("" (rewrite "derivable_div_lam") nil nil))
nil)
((derivable_div_lam formula-decl nil derivatives_lam 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_div_lam 0
(deriv_div_lam-1 nil 3304432155
("" (skosimp :preds? t)
(("" (expand* "derivable?" "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)
((real_times_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types 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 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_scald1_lam_TCC1 0
(deriv_scald1_lam_TCC1-1 nil 3304431707
("" (skosimp :preds? t)
(("" (rewrite "derivable_scald1_lam") nil nil)) nil)
((derivable_scald1_lam formula-decl nil derivatives_lam 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_scald1_lam 0
(deriv_scald1_lam-1 nil 3304432324
("" (skosimp :preds? t)
(("" (expand* "derivable?" "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)
((- 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)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types 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 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)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(derivable? const-decl "bool" derivatives nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nz_deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_scald2_lam_TCC1 0
(deriv_scald2_lam_TCC1-1 nil 3304432644
("" (skosimp) (("" (rewrite "derivable_scald2_lam") nil nil)) nil)
((derivable_scald2_lam formula-decl nil derivatives_lam 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam nil)
(T formal-subtype-decl nil derivatives_lam nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil))
shostak))
(deriv_scald2_lam 0
(deriv_scald2_lam-1 nil 3304432554
("" (skosimp)
(("" (lemma "deriv_scal1_lam")
(("" (inst -1 "1/b!1" "f!1") (("" (assert) nil nil)) nil)) nil))
nil)
((deriv_scal1_lam formula-decl nil derivatives_lam nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_lam nil)
(T_pred const-decl "[real -> boolean]" derivatives_lam 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)
(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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
shostak)))
¤ Dauer der Verarbeitung: 0.85 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.
|
