Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 1 kB

Quelle to2pi.pvs Sprache: PVS

to2pi :THEORY
BEGIN

  IMPORTING atan2,
            trig_ineq,
     reals@abs_lems

  a,b   : VAR real
  alpha : VAR nnreal_lt_2pi
  beta  : VAR real
  k     : VAR int

  to2pi(a) : nnreal_lt_2pi =
    LET n = floor(a/(2*pi)) IN
    a - 2*n*pi

  to2pi_id : LEMMA
    to2pi(alpha) = alpha

  to2pi_period : LEMMA
    to2pi(a) = to2pi(a+2*k*pi)

  sin_id_to2pi : LEMMA
    sin(to2pi(a)) = sin(a)

  cos_id_to2pi : LEMMA
    cos(to2pi(a)) = cos(a)

  to2pi_to2pi : LEMMA
    to2pi(to2pi(a)+b) = to2pi(a+b)

  to2pi_to2pi_sub : LEMMA
    to2pi(b-to2pi(a)) = to2pi(b-a)

  to2pi_neg : LEMMA
    -2*pi <= a AND a < 0 IMPLIES to2pi(a) = a+2*pi

  to2pi_equal : LEMMA
    to2pi(a) = to2pi(b) IMPLIES
      EXISTS(k:int): a = b + k*2*pi

  to2pi_to2pi_add : LEMMA
    to2pi(to2pi(a)+b) = to2pi(a+b)

  to2pi_closed_diff :  LEMMA
    abs(to2pi(a) - to2pi(b)) < 2*pi

  to2pi_eq: LEMMA
    FORALL (k: int): a = b + 2*k*pi IMPLIES
    to2pi(a) = to2pi(b)

  to2pi_sep : LEMMA
    a < b AND b < a + 2*pi IMPLIES
    ((EXISTS (k:int): (a < 2*k*pi AND 2*k*pi <= b))
     OR
     (EXISTS (k: int): (2*k*pi <= a AND b < 2*(k+1)*pi)))

  sin_gt_to2pi : LEMMA
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) > sin(b) IFF b < to2pi(a+pi/2)-pi/2 AND to2pi(a+pi/2)-pi/2 < pi-b)

  sin_lt_to2pi : LEMMA
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) < sin(b) IFF b > to2pi(a+pi/2)-pi/2 OR to2pi(a+pi/2)-pi/2 > pi-b)

  sin_ge_to2pi : LEMMA
    -pi/2 <= b AND b <= pi/2 IMPLIES
   (sin(a) >= sin(b) IFF b <= to2pi(a+pi/2)-pi/2 AND to2pi(a+pi/2)-pi/2 <= pi-b)

  cos_pos_to2pi : LEMMA
    cos(a) > 0 IFF -pi/2 < to2pi(a+pi/2)-pi/2 AND to2pi(a+pi/2)-pi/2 < pi/2

  cos_nneg_to2pi : LEMMA
    cos(a) >= 0 IFF -pi/2 <= to2pi(a+pi/2)-pi/2 AND to2pi(a+pi/2)-pi/2 <= pi/2

END to2pi

quality98%

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