Quellcode-Bibliothek deriv_real_vect.prf Sprache: Lisp

(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)))

quality100%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.4Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.