Quelle deriv_cont_2D.prf Sprache: Lisp

(deriv_cont_2D
(derivable_rv_cont_rv_TCC1 0
  (derivable_rv_cont_rv_TCC1-1 nil 3474295379
   ("" (lemma deriv_domain) (("" (propax) nil nil)) nil)
   ((deriv_domain formula-decl nil deriv_cont_2D nil)) nil))
(derivable_rv_cont_rv_TCC2 0
  (derivable_rv_cont_rv_TCC2-1 nil 3474295379
   ("" (lemma not_one_element) (("" (propax) nil nil)) nil)
   ((not_one_element formula-decl nil deriv_cont_2D nil)) nil))
(derivable_rv_cont_rv 0
  (derivable_rv_cont_rv-1 nil 3474295432
   ("" (skosimp*)
    (("" (lemma cont_rv_iff_comps[T])
      (("" (inst?)
        (("" (assert)
          (("" (hide 2)
            (("" (expand "derivable_rv?")
              (("" (flatten)
                (("" (lemma derivable_cont_fun[T])
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (hide -1 -2)
                        (("1" (lemma derivable_cont_fun[T])
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide - 2)
                    (("2" (lemma "not_one_element")
                      (("2" (propax) nil nil)) nil))
                    nil)
                   ("3" (hide 2)
                    (("3" (lemma "deriv_domain")
                      (("3" (expand "deriv_domain?")
                        (("3" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-subtype-decl nil deriv_cont_2D nil)
    (T_pred const-decl "[real -> boolean]" deriv_cont_2D 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)
    (cont_rv_iff_comps formula-decl nil cont_real_vect2 nil)
    (derivable_rv? const-decl "bool" deriv_real_vect2 nil)
    (derivable_cont_fun formula-decl nil derivatives "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (not_one_element formula-decl nil deriv_cont_2D nil)
    (deriv_domain formula-decl nil deriv_cont_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.