|
(deriv_real_vect_def
(IMP_derivatives_TCC1 0
(IMP_derivatives_TCC1-1 nil 3460302085
("" (lemma "deriv_domain")
(("" (expand "deriv_domain?") (("" (propax) nil nil)) nil)) nil)
((deriv_domain formula-decl nil deriv_real_vect_def nil)) nil))
(IMP_derivatives_TCC2 0
(IMP_derivatives_TCC2-1 nil 3460302085
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil deriv_real_vect_def nil)) nil))
(deriv_TCC1 0
(deriv_TCC1-1 nil 3253536989
("" (auto-rewrite "derivable?")
(("" (skosimp :preds? t) (("" (assert) (("" (inst?) nil nil)) nil))
nil))
nil)
((below type-eq-decl nil naturalnumbers nil)
(derivable? const-decl "bool" deriv_real_vect_def nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" deriv_real_vect_def 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(T formal-subtype-decl nil deriv_real_vect_def nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(below type-eq-decl nil nat_types nil)
(derivable? const-decl "bool" derivatives_def "analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(sum_derivable 0
(sum_derivable-1 nil 3253536989
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (expand "+ ")
(("" (inst - "i!1")
(("" (inst - "i!1")
(("" (lemma "sum_derivable")
(("" (expand "+ ")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((derivable? const-decl "bool" deriv_real_vect_def nil)
(+ const-decl "real" vectors "vectors/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(T formal-subtype-decl nil deriv_real_vect_def nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def nil)
(sum_derivable formula-decl nil derivatives_def "analysis/")
(below type-eq-decl nil nat_types nil)
(n formal-const-decl "posnat" deriv_real_vect_def 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)
(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))
(diff_derivable 0
(diff_derivable-1 nil 3460371074
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (inst - "i!1")
(("" (inst - "i!1")
(("" (lemma "diff_derivable")
(("" (inst?)
(("" (assert)
(("" (expand "-")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((derivable? const-decl "bool" deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(below type-eq-decl nil nat_types nil)
(diff_derivable formula-decl nil derivatives_def "analysis/")
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "real" vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/"))
nil))
(neg_derivable 0
(neg_derivable-1 nil 3442586144
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (inst - "i!1")
(("" (expand "-")
(("" (expand "-")
(("" (lemma "neg_derivable")
(("" (inst?)
(("" (assert)
(("" (expand "-") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((derivable? const-decl "bool" deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(below type-eq-decl nil nat_types nil)
(neg_derivable formula-decl nil derivatives_def "analysis/")
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(- const-decl "Vector" vectors "vectors/"))
nil))
(scal_derivable 0
(scal_derivable-1 nil 3253536989
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (inst - "i!1")
(("" (expand "*")
(("" (expand "*")
(("" (lemma "scal_derivable")
(("" (expand "*")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((derivable? const-decl "bool" deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(below type-eq-decl nil nat_types nil)
(scal_derivable formula-decl nil derivatives_def "analysis/")
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "Vector" vectors "vectors/"))
nil))
(const_derivable 0
(const_derivable-1 nil 3253536989
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (lemma "const_derivable")
(("" (inst?)
(("" (expand "const_fun") (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((derivable? const-decl "bool" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def 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 formula-decl nil derivatives_def "analysis/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(deriv_sum_TCC1 0
(deriv_sum_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "sum_derivable") nil nil)) nil)
((sum_derivable formula-decl nil deriv_real_vect_def 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]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/"))
nil))
(deriv_sum 0
(deriv_sum-1 nil 3253536989
("" (skosimp)
(("" (expand "deriv")
(("" (lemma "sum_derivable")
(("" (inst - "f1!1" "f2!1" "x1!1")
(("" (assert)
(("" (expand "derivable?" -2)
(("" (expand "derivable?" -3)
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_sum")
(("1" (expand "+ ")
(("1" (inst?)
(("1" (assert)
(("1" (hide -1 2)
(("1" (inst?)
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "+")
(("2" (assert)
(("2" (expand "derivable?" -1)
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv const-decl "Vector[n]" deriv_real_vect_def 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]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(derivable? const-decl "bool" deriv_real_vect_def nil)
(below type-eq-decl nil naturalnumbers nil)
(deriv const-decl "real" derivatives_def "analysis/")
(+ const-decl "real" vectors "vectors/")
(f2!1 skolem-const-decl "[T -> Vector[n]]" deriv_real_vect_def nil)
(derivable? const-decl "bool" derivatives_def "analysis/")
(f1!1 skolem-const-decl "[T -> Vector[n]]" deriv_real_vect_def nil)
(x1!1 skolem-const-decl "T" deriv_real_vect_def nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(below type-eq-decl nil nat_types nil)
(deriv_sum formula-decl nil derivatives_def "analysis/")
(sum_derivable formula-decl nil deriv_real_vect_def nil))
nil))
(deriv_neg_TCC1 0
(deriv_neg_TCC1-1 nil 3442582979
("" (lemma "neg_derivable") (("" (propax) nil nil)) nil)
((neg_derivable formula-decl nil deriv_real_vect_def nil)) shostak))
(deriv_neg 0
(deriv_neg-3 nil 3460373415
("" (skosimp)
(("" (expand "deriv")
(("" (lemma "neg_derivable")
(("" (assert)
(("" (expand "derivable?" -2)
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_neg")
(("1" (expand "-")
(("1" (inst?)
(("1" (assert)
(("1" (hide -1 2) (("1" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "-")
(("2" (expand "derivable?" -1)
(("2" (inst?)
(("2" (assert)
(("2" (replace -2) (("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv const-decl "Vector[n]" deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(below type-eq-decl nil naturalnumbers nil)
(deriv const-decl "real" derivatives_def "analysis/")
(- const-decl "Vector" vectors "vectors/")
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def nil)
(derivable? const-decl "bool" derivatives_def "analysis/")
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(f!1 skolem-const-decl "[T -> Vector[n]]" deriv_real_vect_def nil)
(x1!1 skolem-const-decl "T" deriv_real_vect_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(below type-eq-decl nil nat_types nil)
(deriv_neg formula-decl nil derivatives_def "analysis/")
(derivable? const-decl "bool" deriv_real_vect_def nil)
(neg_derivable formula-decl nil deriv_real_vect_def nil))
nil)
(deriv_neg-2 nil 3442586421
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "neg_derivable" "derivable?" "deriv"
"neg_NQ" "lim_neg_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
((neg_NQ formula-decl nil derivatives_def "analysis/")
(A const-decl "setof[nzreal]" derivatives_def "analysis/")
(T formal-subtype-decl nil derivatives_def "analysis/")
(T_pred const-decl "[<#store-print-type real> -> boolean]"
derivatives_def "analysis/")
(lim_neg_fun formula-decl nil lim_of_functions "analysis/")
(deriv const-decl "real" derivatives_def "analysis/"))
nil)
(deriv_neg-1 nil 3442586370
(";;; Proof for formula derivatives_def.deriv_opposite" (skosimp)
((";;; Proof for formula derivatives_def.deriv_opposite"
(auto-rewrite "deriv_TCC" "opposite_derivable" "derivable?"
"deriv" "opposite_NQ" "lim_opposite_fun[(A(x!1))]")
((";;; Proof for formula derivatives_def.deriv_opposite" (assert)
nil))))
"")
nil nil))
(deriv_diff_TCC1 0
(deriv_diff_TCC1-1 nil 3253536989
("" (skosimp*) (("" (rewrite "diff_derivable") nil nil)) nil)
((diff_derivable formula-decl nil deriv_real_vect_def 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]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/"))
nil))
(deriv_diff 0
(deriv_diff-2 nil 3460373064
("" (skosimp)
(("" (expand "deriv")
(("" (lemma "diff_derivable")
(("" (inst - "f1!1" "f2!1" "x1!1")
(("" (assert)
(("" (expand "derivable?" -2)
(("" (expand "derivable?" -3)
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_diff")
(("1" (expand "-")
(("1" (inst?)
(("1" (assert)
(("1" (hide -1 2)
(("1" (inst?)
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "-")
(("2" (assert)
(("2" (expand "derivable?" -1)
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv const-decl "Vector[n]" deriv_real_vect_def 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]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(derivable? const-decl "bool" deriv_real_vect_def nil)
(below type-eq-decl nil naturalnumbers nil)
(deriv const-decl "real" derivatives_def "analysis/")
(- const-decl "real" vectors "vectors/")
(f2!1 skolem-const-decl "[T -> Vector[n]]" deriv_real_vect_def nil)
(derivable? const-decl "bool" derivatives_def "analysis/")
(f1!1 skolem-const-decl "[T -> Vector[n]]" deriv_real_vect_def nil)
(x1!1 skolem-const-decl "T" deriv_real_vect_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(below type-eq-decl nil nat_types nil)
(deriv_diff formula-decl nil derivatives_def "analysis/")
(diff_derivable formula-decl nil deriv_real_vect_def nil))
nil)
(deriv_diff-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "diff_derivable" "derivable?" "deriv"
"diff_NQ" "lim_diff_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
((diff_NQ formula-decl nil derivatives_def "analysis/")
(A const-decl "setof[nzreal]" derivatives_def "analysis/")
(T formal-subtype-decl nil derivatives_def "analysis/")
(T_pred const-decl "[<#store-print-type real> -> boolean]"
derivatives_def "analysis/")
(lim_diff_fun formula-decl nil lim_of_functions "analysis/")
(deriv const-decl "real" derivatives_def "analysis/"))
nil))
(deriv_const_TCC1 0
(deriv_const_TCC1-1 nil 3253536989
("" (lemma "const_derivable") (("" (propax) nil nil)) nil)
((const_derivable formula-decl nil deriv_real_vect_def nil)) nil))
(deriv_const 0
(deriv_const-1 nil 3253536989
("" (skosimp*)
(("" (expand "deriv")
(("" (lemma "const_derivable")
(("" (assert)
(("" (expand "derivable?" -1)
(("" (inst?)
(("" (inst - "x!1")
(("" (apply-extensionality 1 :hide? t)
(("" (lemma "deriv_const")
(("" (inst?)
(("" (expand "const_fun") (("" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv const-decl "Vector[n]" deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(below type-eq-decl nil naturalnumbers nil)
(zero const-decl "Vector" vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(deriv const-decl "real" derivatives_def "analysis/")
(derivable? const-decl "bool" derivatives_def "analysis/")
(b!1 skolem-const-decl "real" deriv_real_vect_def nil)
(x!1 skolem-const-decl "T" deriv_real_vect_def nil)
(comp_zero formula-decl nil vectors "vectors/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_const formula-decl nil derivatives_def "analysis/")
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def nil)
(derivable? const-decl "bool" deriv_real_vect_def nil)
(const_derivable formula-decl nil deriv_real_vect_def nil))
nil))
(deriv_scal_TCC1 0
(deriv_scal_TCC1-1 nil 3253536989
("" (lemma "scal_derivable") (("" (propax) nil nil)) nil)
((scal_derivable formula-decl nil deriv_real_vect_def nil)) nil))
(deriv_scal 0
(deriv_scal-2 nil 3460373644
("" (skosimp)
(("" (expand "deriv")
(("" (lemma "scal_derivable")
(("" (assert)
(("" (expand "derivable?" -2)
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_scal")
(("1" (expand "*")
(("1" (inst?)
(("1" (assert)
(("1" (hide -1 2) (("1" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "*")
(("2" (expand "derivable?" -1)
(("2" (inst?)
(("2" (assert)
(("2" (replace -2) (("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv const-decl "Vector[n]" deriv_real_vect_def 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)
(< 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)
(n formal-const-decl "posnat" deriv_real_vect_def nil)
(below type-eq-decl nil naturalnumbers nil)
(deriv const-decl "real" derivatives_def "analysis/")
(* const-decl "Vector" vectors "vectors/")
(b!1 skolem-const-decl "real" deriv_real_vect_def nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect_def nil)
(T formal-subtype-decl nil deriv_real_vect_def nil)
(derivable? const-decl "bool" derivatives_def "analysis/")
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(f!1 skolem-const-decl "[T -> Vector[n]]" deriv_real_vect_def nil)
(x1!1 skolem-const-decl "T" deriv_real_vect_def nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(below type-eq-decl nil nat_types nil)
(deriv_scal formula-decl nil derivatives_def "analysis/")
(derivable? const-decl "bool" deriv_real_vect_def nil)
(scal_derivable formula-decl nil deriv_real_vect_def nil))
nil)
(deriv_scal-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "scal_derivable" "derivable?" "deriv"
"scal_NQ" "lim_scal_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
((scal_NQ formula-decl nil derivatives_def "analysis/")
(A const-decl "setof[nzreal]" derivatives_def "analysis/")
(T formal-subtype-decl nil derivatives_def "analysis/")
(T_pred const-decl "[<#store-print-type real> -> boolean]"
derivatives_def "analysis/")
(lim_scal_fun formula-decl nil lim_of_functions "analysis/")
(deriv const-decl "real" derivatives_def "analysis/"))
nil)))
¤ Dauer der Verarbeitung: 0.14 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.
|
