products/sources/formale Sprachen/PVS/trig/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: TcpTest.java   Sprache: Lisp

Original von: PVS©
(integral_sincos
 (IMP_deriv_sincos_TCC1 0
  (IMP_deriv_sincos_TCC1-1 nil 3476447258
   ("" (lemma "connected_deriv_domain[T]") (("" (assert) nil nil)) nil)
   ((connected_domain formula-decl nil integral_sincos nil)
    (connected_deriv_domain formula-decl nil deriv_domain_def
     "analysis_ax/")
    (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]" integral_sincos nil)
    (T formal-nonempty-subtype-decl nil integral_sincos nil))
   nil))
 (IMP_deriv_sincos_TCC2 0
  (IMP_deriv_sincos_TCC2-1 nil 3476447258 ("" (assert) nil nil)
   ((not_one_element formula-decl nil integral_sincos nil)) nil))
 (sin_Integrable 0
  (sin_Integrable-1 nil 3476447279
   ("" (skosimp*)
    (("" (lemma "sin_derivable[T]")
      (("" (inst?)
        (("" (lemma "derivable_Integrable?")
          (("" (inst?) (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-subtype-decl nil integral_sincos nil)
    (T_pred const-decl "[real -> boolean]" integral_sincos 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)
    (sin_derivable formula-decl nil deriv_sincos nil)
    (derivable_Integrable? formula-decl nil fundamental_theorem
     "analysis_ax/")
    (sin_range application-judgement "trig_range" trig_basic nil)
    (sin const-decl "real" trig_basic nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (cos_Integrable 0
  (cos_Integrable-2 nil 3479113925
   ("" (skosimp*)
    (("" (lemma "cos_derivable[T]")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "derivable_Integrable?")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-subtype-decl nil integral_sincos nil)
    (T_pred const-decl "[real -> boolean]" integral_sincos 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)
    (cos_derivable formula-decl nil deriv_sincos nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos const-decl "real" trig_basic nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (derivable_Integrable? formula-decl nil fundamental_theorem
     "analysis_ax/"))
   nil)
  (cos_Integrable-1 nil 3476446588
   ("" (skosimp*)
    (("" (lemma "cos_derivable")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "derivable_Integrable?")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((cos_derivable formula-decl nil deriv_sincos nil)
    (derivable_Integrable? formula-decl nil fundamental_theorem
     "analysis_ax/"))
   shostak))
 (Integral_sin_TCC1 0
  (Integral_sin_TCC1-1 nil 3476447258
   ("" (skosimp*)
    (("" (lemma sin_Integrable) (("" (inst?) nil nil)) nil)) nil)
   ((sin_Integrable formula-decl nil integral_sincos 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]" integral_sincos nil)
    (T formal-nonempty-subtype-decl nil integral_sincos nil))
   nil))
 (Integral_sin 0
  (Integral_sin-1 nil 3476447372
   ("" (skosimp*)
    (("" (lemma "fundamental3")
      (("" (inst?)
        ((""
          (inst - "(LAMBDA (x: T): -k!1 / alpha!1* cos(alpha!1 * x))")
          (("" (assert)
            (("" (lemma "cos_derivable[T]")
              (("" (inst - "alpha!1" "-k!1/alpha!1")
                (("" (assert)
                  (("" (lemma "deriv_cos[T]")
                    (("" (inst - "alpha!1" "-k!1/alpha!1")
                      (("" (assert)
                        (("" (hide-all-but 1)
                          (("" (lemma "sin_continuous[T]")
                            (("" (inst?) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-subtype-decl nil integral_sincos nil)
    (T_pred const-decl "[real -> boolean]" integral_sincos 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)
    (fundamental3 formula-decl nil fundamental_theorem "analysis_ax/")
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (cos const-decl "real" trig_basic nil)
    (cos_derivable formula-decl nil deriv_sincos nil)
    (sin_continuous formula-decl nil deriv_sincos nil)
    (deriv_cos formula-decl nil deriv_sincos nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (sin const-decl "real" trig_basic nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (Integral_cos_TCC1 0
  (Integral_cos_TCC1-1 nil 3476447258
   ("" (skosimp*)
    (("" (lemma cos_Integrable) (("" (inst?) nil nil)) nil)) nil)
   ((cos_Integrable formula-decl nil integral_sincos 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]" integral_sincos nil)
    (T formal-nonempty-subtype-decl nil integral_sincos nil))
   nil))
 (Integral_cos 0
  (Integral_cos-2 nil 3479114004
   ("" (skosimp*)
    (("" (lemma "fundamental3")
      (("" (inst?)
        ((""
          (inst - "(LAMBDA (x: T): k!1 / alpha!1* sin(alpha!1 * x))")
          (("" (assert)
            (("" (lemma "sin_derivable[T]")
              (("" (inst - "alpha!1" "k!1/alpha!1")
                (("" (assert)
                  (("" (lemma "deriv_sin[T]")
                    (("" (inst - "alpha!1" "k!1/alpha!1")
                      (("" (assert)
                        (("" (hide-all-but 1)
                          (("" (lemma "cos_continuous[T]")
                            (("" (inst?) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-nonempty-subtype-decl nil integral_sincos nil)
    (T_pred const-decl "[real -> boolean]" integral_sincos 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)
    (fundamental3 formula-decl nil fundamental_theorem "analysis_ax/")
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (sin const-decl "real" trig_basic nil)
    (sin_derivable formula-decl nil deriv_sincos nil)
    (cos_continuous formula-decl nil deriv_sincos nil)
    (deriv_sin formula-decl nil deriv_sincos nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (cos const-decl "real" trig_basic nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil)
  (Integral_cos-1 nil 3476449527
   ("" (skosimp*)
    (("" (lemma "fundamental3")
      (("" (inst?)
        ((""
          (inst - "(LAMBDA (x: T): k!1 / alpha!1* sin(alpha!1 * x))")
          (("" (assert)
            (("" (lemma "sin_derivable")
              (("" (inst - "alpha!1" "k!1/alpha!1")
                (("" (assert)
                  (("" (lemma "deriv_sin")
                    (("" (inst - "alpha!1" "k!1/alpha!1")
                      (("" (assert)
                        (("" (hide-all-but 1)
                          (("" (lemma "cos_continuous")
                            (("" (inst?) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((fundamental3 formula-decl nil fundamental_theorem "analysis_ax/")
    (sin_derivable formula-decl nil deriv_sincos nil)
    (cos_continuous formula-decl nil deriv_sincos nil)
    (deriv_sin formula-decl nil deriv_sincos nil))
   nil)))


¤ Dauer der Verarbeitung: 0.20 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff