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

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders