Quellcode-Bibliothek 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%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.