Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: leminv.ml Sprache: PVS

Original von: PVS^©

to2pi :THEORY
BEGIN

  IMPORTING atan2,
            trig_ineq

  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

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.