| products/sources/formale sprachen/PVS/vect_analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: vect_fun_ops_rv.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.18 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.Bot Zugriff |
