Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: trig_aux.prf Sprache: Lisp

Original von: PVS^©

(trig_aux
(sin_cos_eq_0 0
  (sin_cos_eq_0-1 nil 3385302546
   ("" (skosimp)
    (("" (rewrite "sin_eq_0")
      (("" (skosimp)
        (("" (replace -1)
          (("" (rewrite "cos_k_pi") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((sin_eq_0 formula-decl nil trig_basic "trig/")
    (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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (rat_exp application-judgement "rat" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (cos_k_pi formula-decl nil trig_basic "trig/"))
   shostak))
(eq_iff_periodic 0
  (eq_iff_periodic-1 nil 3385302828
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (lemma "cos_minus" ("a" "a!1" "b" "b!1"))
          (("1" (replace -2)
            (("1" (replace -3)
              (("1" (rewrite "sq_rew")
                (("1" (rewrite "sq_rew")
                  (("1" (lemma "sin2_cos2" ("a" "b!1"))
                    (("1" (assert)
                      (("1" (replace -1)
                        (("1" (rewrite "cos_eq_1" -2)
                          (("1" (skosimp)
                            (("1" (inst + "i!1")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (replace -1)
          (("2" (rewrite "sin_period" 1 :dir rl)
            (("2" (rewrite "cos_period" 1 :dir rl) nil nil)) nil))
          nil))
        nil))
      nil))
    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_minus formula-decl nil trig_basic "trig/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sin const-decl "real" trig_basic "trig/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cos_eq_1 formula-decl nil trig_basic "trig/")
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sin2_cos2 formula-decl nil trig_basic "trig/")
    (sq_rew formula-decl nil sq "reals/")
    (cos const-decl "real" trig_basic "trig/")
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sin_range application-judgement "trig_range" trig_basic "trig/")
    (cos_range application-judgement "trig_range" trig_basic "trig/")
    (cos_period formula-decl nil trig_basic "trig/")
    (integer nonempty-type-from-decl nil integers nil)
    (sin_period formula-decl nil trig_basic "trig/"))
   shostak)))

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