|
(deriv_real_vect
(IMP_deriv_real_vect_def_TCC1 0
(IMP_deriv_real_vect_def_TCC1-1 nil 3460367906
("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
((deriv_domain formula-decl nil deriv_real_vect nil)) nil))
(IMP_deriv_real_vect_def_TCC2 0
(IMP_deriv_real_vect_def_TCC2-1 nil 3460367906
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil deriv_real_vect nil)) nil))
(deriv_TCC1 0
(deriv_TCC1-1 nil 3253536989
("" (auto-rewrite "derivable")
(("" (skosimp :preds? t)
(("" (expand "derivable?" -1) (("" (inst?) nil 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)
(T_pred const-decl "[real -> boolean]" deriv_real_vect nil)
(T formal-subtype-decl nil deriv_real_vect 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)
(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 nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(derivable? const-decl "bool" deriv_real_vect nil)
(deriv_vfun type-eq-decl nil deriv_real_vect nil))
nil))
(sum_derivable_vfun 0
(sum_derivable_vfun-1 nil 3253536989
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (inst?)
(("" (inst?)
(("" (lemma "sum_derivable")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((derivable? const-decl "bool" deriv_real_vect 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 nil)
(T formal-subtype-decl nil deriv_real_vect nil)
(n formal-const-decl "posnat" deriv_real_vect 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)
(sum_derivable formula-decl nil deriv_real_vect_def nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(neg_derivable_vfun 0
(neg_derivable_vfun-1 nil 3253536989
("" (expand "derivable?")
(("" (grind :defs nil :rewrites "neg_derivable") 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)
(T_pred const-decl "[real -> boolean]" deriv_real_vect nil)
(T formal-subtype-decl nil deriv_real_vect nil)
(n formal-const-decl "posnat" deriv_real_vect 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)
(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)
(neg_derivable formula-decl nil deriv_real_vect_def nil)
(derivable? const-decl "bool" deriv_real_vect nil))
nil))
(diff_derivable_vfun 0
(diff_derivable_vfun-1 nil 3253536989
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (inst?)
(("" (inst?)
(("" (lemma "diff_derivable")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((derivable? const-decl "bool" deriv_real_vect 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 nil)
(T formal-subtype-decl nil deriv_real_vect nil)
(n formal-const-decl "posnat" deriv_real_vect 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)
(diff_derivable formula-decl nil deriv_real_vect_def nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(dot_derivable_vfun 0
(dot_derivable_vfun-1 nil 3475586756
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (lemma "dot_prod_derivable")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((derivable? const-decl "bool" derivatives "analysis/")
(derivable? const-decl "bool" deriv_real_vect nil)
(n formal-const-decl "posnat" deriv_real_vect 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)
(T formal-subtype-decl nil deriv_real_vect nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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)
(dot_prod_derivable formula-decl nil deriv_dot_prod nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(scal_derivable_vfun 0
(scal_derivable_vfun-1 nil 3253536989
("" (expand "derivable?")
(("" (grind :defs nil :rewrites "scal_derivable") nil nil)) nil)
((T_pred const-decl "[real -> boolean]" deriv_real_vect nil)
(T formal-subtype-decl nil deriv_real_vect nil)
(n formal-const-decl "posnat" deriv_real_vect 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)
(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)
(scal_derivable formula-decl nil 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)
(derivable? const-decl "bool" deriv_real_vect nil))
nil))
(const_derivable_vfun 0
(const_derivable_vfun-1 nil 3253536989
("" (skosimp*)
(("" (expand "derivable?")
(("" (skosimp*)
(("" (lemma "const_derivable")
(("" (inst?) (("" (postpone) nil nil)) nil)) nil))
nil))
nil))
nil)
((derivable? const-decl "bool" deriv_real_vect nil)
(n formal-const-decl "posnat" deriv_real_vect 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)
(T formal-subtype-decl nil deriv_real_vect nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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 deriv_real_vect_def nil))
nil))
(inv_derivable_vfun 0
(inv_derivable_vfun-1 nil 3253536989
("" (expand "derivable?")
(("" (grind :defs nil :rewrites "inv_derivable") 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)
(T_pred const-decl "[real -> boolean]" deriv_real_vect nil)
(T formal-subtype-decl nil deriv_real_vect nil)
(inv_derivable formula-decl nil derivatives_def "analysis/")
(derivable? const-decl "bool" derivatives "analysis/"))
nil))
(derivable_sum 0
(derivable_sum-1 nil 3253536989
("" (skolem!) (("" (rewrite "sum_derivable_vfun") nil nil)) nil)
((sum_derivable_vfun formula-decl nil deriv_real_vect 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 nil)
(T formal-subtype-decl nil deriv_real_vect 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 nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(derivable? const-decl "bool" deriv_real_vect nil)
(deriv_vfun type-eq-decl nil deriv_real_vect nil))
nil))
(derivable_diff 0
(derivable_diff-1 nil 3253536989
("" (skolem!) (("" (rewrite "diff_derivable_vfun") nil nil)) nil)
((diff_derivable_vfun formula-decl nil deriv_real_vect 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 nil)
(T formal-subtype-decl nil deriv_real_vect 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 nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(derivable? const-decl "bool" deriv_real_vect nil)
(deriv_vfun type-eq-decl nil deriv_real_vect nil))
nil))
(derivable_scal 0
(derivable_scal-1 nil 3253536989
("" (skosimp*)
(("" (lemma "scal_derivable_vfun")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((scal_derivable_vfun formula-decl nil deriv_real_vect nil)
(deriv_vfun type-eq-decl nil deriv_real_vect nil)
(derivable? const-decl "bool" deriv_real_vect nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" deriv_real_vect 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)
(T formal-subtype-decl nil deriv_real_vect nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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))
(derivable_neg 0
(derivable_neg-1 nil 3253536989
("" (skosimp*)
(("" (lemma "neg_derivable_vfun")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((neg_derivable_vfun formula-decl nil deriv_real_vect nil)
(deriv_vfun type-eq-decl nil deriv_real_vect nil)
(derivable? const-decl "bool" deriv_real_vect nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" deriv_real_vect 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)
(T formal-subtype-decl nil deriv_real_vect nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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))
(derivable_const 0
(derivable_const-1 nil 3253536989
("" (skosimp*) (("" (rewrite "const_derivable_vfun") nil nil)) nil)
((const_derivable_vfun formula-decl nil deriv_real_vect 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))
nil))
(deriv_sum_vfun 0
(deriv_sum_vfun-1 nil 3253536989
("" (skosimp*)
(("" (typepred "ff1!1")
(("" (typepred "ff2!1")
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_sum")
(("1" (inst - "ff1!1" "ff2!1" "x!1")
(("1" (expand "deriv" 1)
(("1" (assert)
(("1" (hide 2)
(("1" (expand "derivable?" -1)
(("1" (expand "derivable?" -2)
(("1" (inst?)
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "+")
(("2" (lemma "sum_derivable_vfun")
(("2" (inst - "ff1!1" "ff2!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_vfun type-eq-decl nil deriv_real_vect nil)
(derivable? const-decl "bool" deriv_real_vect nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" deriv_real_vect 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 nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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)
(deriv const-decl "[T -> Vector[n]]" deriv_real_vect nil)
(+ const-decl "real" vectors "vectors/")
(ff1!1 skolem-const-decl "deriv_vfun" deriv_real_vect nil)
(ff2!1 skolem-const-decl "deriv_vfun" deriv_real_vect nil)
(deriv_sum formula-decl nil deriv_real_vect_def nil)
(sum_derivable_vfun formula-decl nil deriv_real_vect nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(deriv_neg_vfun 0
(deriv_neg_vfun-2 nil 3460370332
("" (skosimp*)
(("" (typepred "ff!1")
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_neg")
(("1" (inst - "ff!1" "x!1")
(("1" (expand "deriv" 1)
(("1" (assert)
(("1" (hide 2)
(("1" (expand "derivable?" -1)
(("1" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "neg_derivable_vfun")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((deriv_vfun type-eq-decl nil deriv_real_vect nil)
(derivable? const-decl "bool" deriv_real_vect nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" deriv_real_vect 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 nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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)
(neg_derivable_vfun formula-decl nil deriv_real_vect nil)
(deriv_neg formula-decl nil deriv_real_vect_def nil)
(ff!1 skolem-const-decl "deriv_vfun" deriv_real_vect nil)
(- const-decl "Vector" vectors "vectors/")
(deriv const-decl "[T -> Vector[n]]" deriv_real_vect nil))
nil)
(deriv_neg_vfun-1 nil 3253536989
("" (skolem-typepred)
(("" (expand "derivable?")
(("" (apply-extensionality :hide? t)
(("" (expand "-" 1 2)
(("" (expand "deriv")
(("" (rewrite "deriv_neg") (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((deriv_neg formula-decl nil derivatives_def "analysis/")
(deriv const-decl "[T -> real]" derivatives "analysis/")
(T formal-subtype-decl nil derivatives "analysis/")
(T_pred const-decl "[<#store-print-type real> -> boolean]"
derivatives "analysis/"))
nil))
(deriv_diff_vfun 0
(deriv_diff_vfun-2 nil 3460370191
("" (skosimp*)
(("" (typepred "ff1!1")
(("" (typepred "ff2!1")
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_diff")
(("1" (inst - "ff1!1" "ff2!1" "x!1")
(("1" (expand "deriv" 1)
(("1" (assert)
(("1" (hide 2)
(("1" (expand "derivable?" -1)
(("1" (expand "derivable?" -2)
(("1" (inst?)
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "diff_derivable_vfun")
(("2" (inst - "ff1!1" "ff2!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_vfun type-eq-decl nil deriv_real_vect nil)
(derivable? const-decl "bool" deriv_real_vect nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" deriv_real_vect 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 nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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)
(deriv const-decl "[T -> Vector[n]]" deriv_real_vect nil)
(- const-decl "real" vectors "vectors/")
(ff1!1 skolem-const-decl "deriv_vfun" deriv_real_vect nil)
(ff2!1 skolem-const-decl "deriv_vfun" deriv_real_vect nil)
(deriv_diff formula-decl nil deriv_real_vect_def nil)
(diff_derivable_vfun formula-decl nil deriv_real_vect nil))
nil)
(deriv_diff_vfun-1 nil 3253536989
("" (skolem-typepred)
(("" (expand "derivable?")
(("" (apply-extensionality :hide? t)
(("" (expand "-" 1 2)
(("" (expand "deriv")
(("" (rewrite "deriv_diff")
(("1" (inst?) nil nil) ("2" (inst? -2) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((deriv_diff formula-decl nil derivatives_def "analysis/")
(deriv const-decl "[T -> real]" derivatives "analysis/")
(T formal-subtype-decl nil derivatives "analysis/")
(T_pred const-decl "[<#store-print-type real> -> boolean]"
derivatives "analysis/"))
nil))
(deriv_dot_vfun_TCC1 0
(deriv_dot_vfun_TCC1-1 nil 3475586920
("" (skosimp*) (("" (rewrite "dot_derivable_vfun") nil nil)) nil)
((dot_derivable_vfun formula-decl nil deriv_real_vect 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 nil)
(T formal-subtype-decl nil deriv_real_vect 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 nil)
(Index type-eq-decl nil vectors "vectors/")
(Vector type-eq-decl nil vectors "vectors/")
(derivable? const-decl "bool" deriv_real_vect nil)
(deriv_vfun type-eq-decl nil deriv_real_vect nil))
nil))
(deriv_dot_vfun 0
(deriv_dot_vfun-1 nil 3475586989
("" (skosimp*)
(("" (typepred "ff1!1")
(("" (typepred "ff2!1")
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_dot_prod")
(("1" (inst - "ff1!1" "ff2!1" "x!1")
(("1" (expand "deriv" 1)
(("1" (assert)
(("1" (expand "derivable?" -2)
(("1" (expand "derivable?" -3)
(("1" (inst?)
(("1" (inst?)
(("1" (assert)
(("1" (assert)
(("1"
(expand "+")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "dot_derivable_vfun")
(("2" (inst - "ff1!1" "ff2!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_vfun type-eq-decl nil deriv_real_vect nil)
(derivable? const-decl "bool" deriv_real_vect nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" deriv_real_vect 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 nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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)
(deriv const-decl "[T -> Vector[n]]" deriv_real_vect nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv const-decl "[T -> real]" derivatives "analysis/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(derivable? const-decl "bool" derivatives "analysis/")
(* const-decl "real" vectors "vectors/")
(ff1!1 skolem-const-decl "deriv_vfun" deriv_real_vect nil)
(ff2!1 skolem-const-decl "deriv_vfun" deriv_real_vect nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(deriv_dot_prod formula-decl nil deriv_dot_prod nil)
(dot_derivable_vfun formula-decl nil deriv_real_vect nil))
nil))
(deriv_scal_vfun 0
(deriv_scal_vfun-2 nil 3460370441
("" (skosimp*)
(("" (typepred "ff!1")
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_scal")
(("1" (inst?)
(("1" (inst - "x!1")
(("1" (expand "deriv" 1)
(("1" (assert)
(("1" (hide 2)
(("1" (expand "derivable?" -1)
(("1" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "scal_derivable_vfun")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((deriv_vfun type-eq-decl nil deriv_real_vect nil)
(derivable? const-decl "bool" deriv_real_vect nil)
(Vector type-eq-decl nil vectors "vectors/")
(Index type-eq-decl nil vectors "vectors/")
(n formal-const-decl "posnat" deriv_real_vect 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 nil)
(T_pred const-decl "[real -> boolean]" deriv_real_vect 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)
(scal_derivable_vfun formula-decl nil deriv_real_vect nil)
(deriv_scal formula-decl nil deriv_real_vect_def nil)
(ff!1 skolem-const-decl "deriv_vfun" deriv_real_vect nil)
(b!1 skolem-const-decl "real" deriv_real_vect nil)
(* const-decl "Vector" vectors "vectors/")
(deriv const-decl "[T -> Vector[n]]" deriv_real_vect nil))
nil)
(deriv_scal_vfun-1 nil 3253536989
("" (skolem-typepred)
(("" (expand "derivable?")
(("" (apply-extensionality :hide? t)
(("" (expand "*" 1 2)
(("" (expand "deriv")
(("" (rewrite "deriv_scal") (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((deriv_scal formula-decl nil derivatives_def "analysis/")
(deriv const-decl "[T -> real]" derivatives "analysis/")
(T formal-subtype-decl nil derivatives "analysis/")
(T_pred const-decl "[<#store-print-type real> -> boolean]"
derivatives "analysis/"))
nil))
(deriv_const_vfun 0
(deriv_const_vfun-1 nil 3253536989
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "deriv_const")
(("1" (inst?)
(("1" (expand "zero")
(("1" (inst - "x!1")
(("1" (assert)
(("1" (expand "deriv")
(("1" (replace -1 + :dir rl) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "const_derivable_vfun") (("2" (inst?) nil nil))
nil))
nil))
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 nil)
(T formal-subtype-decl nil deriv_real_vect 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 nil)
(Index type-eq-decl nil vectors "vectors/")
(deriv const-decl "[T -> Vector[n]]" deriv_real_vect nil)
(deriv_vfun type-eq-decl nil deriv_real_vect nil)
(Vector type-eq-decl nil vectors "vectors/")
(derivable? const-decl "bool" deriv_real_vect nil)
(below type-eq-decl nil naturalnumbers nil)
(b!1 skolem-const-decl "real" deriv_real_vect nil)
(deriv const-decl "Vector[n]" deriv_real_vect_def nil)
(zero const-decl "Vector" vectors "vectors/")
(deriv_const formula-decl nil deriv_real_vect_def nil)
(const_derivable_vfun formula-decl nil deriv_real_vect nil))
nil)))
¤ Dauer der Verarbeitung: 0.65 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.
|
