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

Quelle  deriv_sincos_ax.prf   Sprache: Lisp

 
(deriv_sincos_ax
 (sin_derivable_TCC1 0
  (sin_derivable_TCC1-1 nil 3476447874
   ("" (lemma "connected_deriv_domain[T]") (("" (assertnil nil)) nil)
   ((connected_domain formula-decl nil deriv_sincos_ax nil)
    (not_one_element formula-decl nil deriv_sincos_ax nil)
    (connected_deriv_domain formula-decl nil deriv_domain_def
     "analysis/")
    (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_sincos_ax nil)
    (T formal-subtype-decl nil deriv_sincos_ax nil))
   nil))
 (sin_derivable_TCC2 0
  (sin_derivable_TCC2-1 nil 3476447874
   ("" (assert)
    (("" (skosimp*)
      (("" (lemma "not_one_element")
        (("" (assert)
          (("" (expand "not_one_element?") (("" (inst?) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((not_one_element formula-decl nil deriv_sincos_ax nil)) nil))
 (deriv_sin_TCC1 0
  (deriv_sin_TCC1-1 nil 3476447874
   ("" (skosimp*)
    (("" (lemma "sin_derivable") (("" (inst?) nil nil)) nil)) nil)
   ((sin_derivable formula-decl nil deriv_sincos_ax 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_cos_TCC1 0
  (deriv_cos_TCC1-1 nil 3476447874
   ("" (skosimp*)
    (("" (lemma "cos_derivable") (("" (inst?) nil nil)) nil)) nil)
   ((cos_derivable formula-decl nil deriv_sincos_ax 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)))

100%


¤ Dauer der Verarbeitung: 0.1 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.