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: simp.ML   Sprache: Lisp

Original von: PVS©
(trig_rew
 (tr_rew1 0
  (tr_rew1-1 nil 3507028921 ("" (rewrite "cos_0") nil nil)
   ((cos_0 formula-decl nil trig_basic nil)) nil))
 (tr_rew2 0
  (tr_rew2-1 nil 3507028921 ("" (rewrite "sin_0") nil nil)
   ((sin_0 formula-decl nil trig_basic nil)) nil))
 (tr_rew3 0
  (tr_rew3-1 nil 3507028921 ("" (rewrite "sin_pi2") nil nil)
   ((sin_pi2 formula-decl nil trig_basic nil)) nil))
 (tr_rew4 0
  (tr_rew4-1 nil 3507028921 ("" (rewrite "cos_pi2") nil nil)
   ((cos_pi2 formula-decl nil trig_basic nil)) nil))
 (tr_rew5_TCC1 0
  (tr_rew5_TCC1-1 nil 3507028921
   ("" (expand "Tan?")
    (("" (rewrite "cos_0") (("" (assert) nil nil)) nil)) nil)
   ((cos_0 formula-decl nil trig_basic nil)
    (Tan? const-decl "bool" trig_basic nil))
   nil))
 (tr_rew5 0
  (tr_rew5-1 nil 3507028921 ("" (rewrite "tan_0") nil nil)
   ((tan_0 formula-decl nil trig_basic nil)) nil))
 (tr_rew6 0
  (tr_rew6-1 nil 3507028921 ("" (rewrite "sin_pi") nil nil)
   ((sin_pi formula-decl nil trig_basic nil)) nil))
 (tr_rew7 0
  (tr_rew7-1 nil 3507028921 ("" (rewrite "cos_pi") nil nil)
   ((cos_pi formula-decl nil trig_basic nil)) nil))
 (tr_rew8_TCC1 0
  (tr_rew8_TCC1-1 nil 3507028921
   ("" (expand "Tan?")
    (("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil)
   ((cos_pi formula-decl nil trig_basic nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (Tan? const-decl "bool" trig_basic nil))
   nil))
 (tr_rew8 0
  (tr_rew8-1 nil 3507028921 ("" (rewrite "tan_pi") nil nil)
   ((tan_pi formula-decl nil trig_basic nil)) nil))
 (tr_rew9 0
  (tr_rew9-1 nil 3507028921 ("" (rewrite "sin_3pi2") nil nil)
   ((sin_3pi2 formula-decl nil trig_basic nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil))
 (tr_rew10 0
  (tr_rew10-1 nil 3507028921 ("" (rewrite "cos_3pi2") nil nil)
   ((cos_3pi2 formula-decl nil trig_basic nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil))
 (tr_rew11 0
  (tr_rew11-1 nil 3507028921 ("" (rewrite "sin_2pi") nil nil)
   ((sin_2pi formula-decl nil trig_basic nil)) nil))
 (tr_rew12 0
  (tr_rew12-1 nil 3507028921 ("" (rewrite "cos_2pi") nil nil)
   ((cos_2pi formula-decl nil trig_basic nil)) nil))
 (tr_rew13_TCC1 0
  (tr_rew13_TCC1-1 nil 3507028921
   ("" (expand "Tan?")
    (("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil)
   ((cos_2pi formula-decl nil trig_basic nil)
    (Tan? const-decl "bool" trig_basic nil))
   nil))
 (tr_rew13 0
  (tr_rew13-1 nil 3507028921 ("" (rewrite "tan_2pi") nil nil)
   ((tan_2pi formula-decl nil trig_basic nil)) nil))
 (tr_rew14 0
  (tr_rew14-1 nil 3507028921
   ("" (skosimp*) (("" (rewrite "sin_shift") nil nil)) nil)
   ((sin_shift formula-decl nil trig_basic 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))
 (tr_rew15 0
  (tr_rew15-1 nil 3507028921
   ("" (skosimp*) (("" (rewrite "cos_shift") nil nil)) nil)
   ((cos_shift formula-decl nil trig_basic 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))
 (tr_rew16 0
  (tr_rew16-1 nil 3507028921
   ("" (skosimp*) (("" (rewrite "sin_k_pi") nil nil)) nil)
   ((sin_k_pi formula-decl nil trig_basic 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (integer nonempty-type-from-decl nil integers nil))
   nil))
 (tr_rew17 0
  (tr_rew17-1 nil 3507028921
   ("" (skosimp*) (("" (rewrite "cos_2k_pi") nil nil)) nil)
   ((cos_2k_pi formula-decl nil trig_basic 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (integer nonempty-type-from-decl nil integers nil))
   nil))
 (tr_rew20_TCC1 0
  (tr_rew20_TCC1-1 nil 3507028921
   ("" (skosimp*)
    (("" (expand "Tan?")
      (("" (rewrite "cos_k_pi") (("" (rewrite "expt_nonzero") nil nil))
        nil))
      nil))
    nil)
   ((Tan? const-decl "bool" trig_basic nil)
    (expt_nonzero formula-decl nil exponentiation nil)
    (int nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (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)
    (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_k_pi formula-decl nil trig_basic nil))
   nil))
 (tr_rew20 0
  (tr_rew20-1 nil 3507028921
   ("" (skosimp*) (("" (rewrite "tan_k_pi") nil nil)) nil)
   ((tan_k_pi formula-decl nil trig_basic 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (integer nonempty-type-from-decl nil integers nil))
   nil))
 (tr_rew22 0
  (tr_rew22-1 nil 3507028921
   ("" (skosimp*) (("" (rewrite "sin_neg") nil nil)) nil)
   ((sin_neg formula-decl nil trig_basic 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))
 (tr_rew23 0
  (tr_rew23-1 nil 3507028921
   ("" (skosimp*) (("" (rewrite "cos_neg") nil nil)) nil)
   ((cos_neg formula-decl nil trig_basic 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))
 (tr_rew24_TCC1 0
  (tr_rew24_TCC1-1 nil 3507028921
   ("" (skosimp*)
    (("" (typepred "a!1")
      (("" (expand "Tan?") (("" (rewrite "cos_neg") nil nil)) nil))
      nil))
    nil)
   ((Tan? const-decl "bool" trig_basic 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)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (cos_neg formula-decl nil trig_basic nil))
   nil))
 (tr_rew24 0
  (tr_rew24-1 nil 3507028921
   ("" (skosimp*) (("" (rewrite "tan_neg") nil nil)) nil)
   ((tan_neg formula-decl nil trig_basic 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Tan? const-decl "bool" trig_basic nil))
   nil)))


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