Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis_ax/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 11 kB image not shown  

Quelle  chain_rule.prf   Sprache: Lisp

 
(chain_rule
 (composition_derivable_TCC1 0
  (composition_derivable_TCC1-1 nil 3313840193
   ("" (lemma "deriv_domain[T1]") (("" (propax) nil nil)) nil)
   ((deriv_domain formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T1_pred const-decl "[real -> boolean]" chain_rule nil)
    (T1 formal-subtype-decl nil chain_rule nil))
   nil))
 (composition_derivable_TCC2 0
  (composition_derivable_TCC2-1 nil 3313840193
   ("" (lemma "not_one_element1") (("" (propax) nil nil)) nil)
   ((not_one_element1 formula-decl nil chain_rule nil)) nil))
 (composition_derivable_TCC3 0
  (composition_derivable_TCC3-1 nil 3602243133
   ("" (lemma "deriv_domain[T2]") (("" (skosimp*) nil nil)) nil)
   ((deriv_domain formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T2_pred const-decl "[real -> boolean]" chain_rule nil)
    (T2 formal-subtype-decl nil chain_rule nil))
   nil))
 (composition_derivable_TCC4 0
  (composition_derivable_TCC4-1 nil 3602243133
   ("" (lemma "not_one_element2") (("" (skosimp*) nil nil)) nil)
   ((not_one_element2 formula-decl nil chain_rule nil)) nil))
 (composition_derivable 0
  (composition_derivable-3 nil 3475836001
   ("" (expand "derivable?")
    (("" (expand "convergent?")
      (("" (skosimp*)
        (("" (forward-chain "chain_rule_cnvg") (("" (inst?) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable? const-decl "bool" derivatives_def nil)) nil)
  (composition_derivable-2 nil 3445340288
   ("" (expand "derivable?")
    (("" (expand "convergent?")
      (("" (skosimp*)
        (("" (forward-chain "chain_rule") (("" (inst?) nil nil)) nil))
        nil))
      nil))
    nil)
   ((derivable? const-decl "bool" derivatives_def nil)) nil)
  (composition_derivable-1 nil 3313840193
   ("" (expand "derivable")
    (("" (expand "convergent?")
      (("" (skosimp*)
        (("" (forward-chain "chain_rule") (("" (inst?) nil nil)) nil))
        nil))
      nil))
    nil)
   nil nil))
 (composition_derivable_fun_TCC1 0
  (composition_derivable_fun_TCC1-1 nil 3313840193
   ("" (skosimp*)
    (("" (lemma "deriv_domain2") (("" (propax) nil nil)) nil)) nil)
   ((deriv_domain2 formula-decl nil chain_rule nil)) nil))
 (composition_derivable_fun_TCC2 0
  (composition_derivable_fun_TCC2-1 nil 3313840193
   ("" (skosimp*)
    (("" (lemma not_one_element2) (("" (propax) nil nil)) nil)) nil)
   ((not_one_element2 formula-decl nil chain_rule nil)) nil))
 (composition_derivable_fun 0
  (composition_derivable_fun-1 nil 3313840193
   ("" (expand "derivable?")
    (("" (skosimp*)
      (("" (rewrite "composition_derivable")
        (("1" (inst?) nil nil) ("2" (inst? -2) nil nil)) nil))
      nil))
    nil)
   ((T2 formal-subtype-decl nil chain_rule nil)
    (T2_pred const-decl "[real -> boolean]" chain_rule nil)
    (T1 formal-subtype-decl nil chain_rule nil)
    (T1_pred const-decl "[real -> boolean]" chain_rule 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)
    (composition_derivable formula-decl nil chain_rule nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (deriv_composition_TCC1 0
  (deriv_composition_TCC1-1 nil 3313840193
   ("" (lemma "composition_derivable")
    (("" (skosimp*)
      (("" (inst?) (("" (expand "O") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (T2 formal-subtype-decl nil chain_rule nil)
    (T2_pred const-decl "[real -> boolean]" chain_rule nil)
    (T1 formal-subtype-decl nil chain_rule nil)
    (T1_pred const-decl "[real -> boolean]" chain_rule 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)
    (composition_derivable formula-decl nil chain_rule nil))
   nil))
 (deriv_composition 0
  (deriv_composition-1 nil 3313840193
   ("" (skosimp)
    (("" (forward-chain "composition_derivable")
      ((""
        (auto-rewrite "deriv_TCC[T1]" "deriv_TCC[T2]"
                      ("deriv[T1]" "derivable?[T1]" "deriv[T2]"
                       "derivable?[T2]")
                      ("lim_fun_lemma[(A[T1](x!1))]"
                       "lim_fun_lemma[(A[T2](f!1(x!1)))]"))
        (("1" (assert)
          (("1" (rewrite "lim_fun_def[(A[T1](x!1))]")
            (("1" (rewrite "chain_rule_cnvg") nil nil)) nil))
          nil)
         ("2" (skosimp*)
          (("2" (lemma "not_one_element2")
            (("2" (expand "not_one_element?") (("2" (inst?) nil nil))
              nil))
            nil))
          nil)
         ("3" (lemma "deriv_domain2 ")
          (("3" (skosimp*)
            (("3" (expand "deriv_domain?") (("3" (inst?) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv const-decl "real" derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (not_one_element? const-decl "bool" deriv_domain_def nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil))
   nil))
 (gg_TCC1 0
  (gg_TCC1-1 nil 3313840193
   ("" (lemma "deriv_domain2") (("" (propax) nil nil)) nil)
   ((deriv_domain2 formula-decl nil chain_rule nil)) nil))
 (gg_TCC2 0
  (gg_TCC2-1 nil 3313840193
   ("" (lemma "not_one_element2") (("" (propax) nil nil)) nil)
   ((not_one_element2 formula-decl nil chain_rule nil)) nil))
 (deriv_comp_fun_TCC1 0
  (deriv_comp_fun_TCC1-1 nil 3313840193
   ("" (skosimp) (("" (rewrite "composition_derivable_fun") nil nil))
    nil)
   ((composition_derivable_fun formula-decl nil chain_rule 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)
    (T1_pred const-decl "[real -> boolean]" chain_rule nil)
    (T1 formal-subtype-decl nil chain_rule nil)
    (T2_pred const-decl "[real -> boolean]" chain_rule nil)
    (T2 formal-subtype-decl nil chain_rule nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (deriv_comp_fun 0
  (deriv_comp_fun-1 nil 3313840193
   ("" (skolem-typepred)
    (("" (assert)
      (("" (expand "derivable?")
        (("" (auto-rewrite "composition_derivable_fun")
          (("" (apply-extensionality :hide? t)
            (("" (expand "*")
              (("" (expand "o" 1 2)
                (("" (expand "deriv")
                  (("" (rewrite "deriv_composition")
                    (("1" (inst? -1) nil nil) ("2" (inst? -2) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (deriv_composition formula-decl nil chain_rule nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (O const-decl "T3" function_props nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (T2 formal-subtype-decl nil chain_rule nil)
    (T2_pred const-decl "[real -> boolean]" chain_rule nil)
    (derivable? const-decl "bool" derivatives nil)
    (T1 formal-subtype-decl nil chain_rule nil)
    (T1_pred const-decl "[real -> boolean]" chain_rule 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))
   nil))
 (comp_derivable_fun 0
  (comp_derivable_fun-1 nil 3475834576
   ("" (skosimp*)
    (("" (lemma "composition_derivable_fun")
      (("" (expand "o ") (("" (inst?) (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((composition_derivable_fun formula-decl nil chain_rule 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)
    (T1_pred const-decl "[real -> boolean]" chain_rule nil)
    (T1 formal-subtype-decl nil chain_rule nil)
    (T2_pred const-decl "[real -> boolean]" chain_rule nil)
    (T2 formal-subtype-decl nil chain_rule nil)
    (O const-decl "T3" function_props nil))
   shostak))
 (chain_rule_TCC1 0
  (chain_rule_TCC1-1 nil 3475835726
   ("" (skosimp*)
    (("" (lemma comp_derivable_fun)
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((comp_derivable_fun formula-decl nil chain_rule nil)
    (derivable? const-decl "bool" derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-subtype-decl nil chain_rule nil)
    (T2_pred const-decl "[real -> boolean]" chain_rule nil)
    (T1 formal-subtype-decl nil chain_rule nil)
    (T1_pred const-decl "[real -> boolean]" chain_rule 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))
 (chain_rule 0
  (chain_rule-1 nil 3475853574
   ("" (skosimp*)
    (("" (lemma deriv_comp_fun)
      (("" (expand "o ") (("" (inst?) nil nil)) nil)) nil))
    nil)
   ((deriv_comp_fun formula-decl nil chain_rule nil)
    (derivable? const-decl "bool" derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T2 formal-subtype-decl nil chain_rule nil)
    (T2_pred const-decl "[real -> boolean]" chain_rule nil)
    (T1 formal-subtype-decl nil chain_rule nil)
    (T1_pred const-decl "[real -> boolean]" chain_rule 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)
    (O const-decl "T3" function_props nil))
   shostak)))

100%


¤ Dauer der Verarbeitung: 0.14 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.