Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: track.pvs Sprache: PVS

Original von: PVS^©

track : THEORY
BEGIN

  IMPORTING trig_fnd@to2pi,
            definitions

   trk        : VAR real
   s,v,vi,nvo : VAR Nz_vect2
   gsp        : VAR posreal

  trkgs2vect(trk,gsp) : Nz_vect2 =
    gsp*(sin(trk),cos(trk))

  track(v) : nnreal_lt_2pi =
    atan2(v`y,v`x)

  sin_track : LEMMA
    sin(track(v)) = v`x/norm(v)

  cos_track : LEMMA
    cos(track(v)) = v`y/norm(v)

  norm_id : LEMMA
    norm(trkgs2vect(trk,gsp)) = gsp

  track_id : LEMMA
    track(trkgs2vect(trk,gsp)) = to2pi(trk)

  trkgs2vect_id : LEMMA
    trkgs2vect(track(v),norm(v)) = v

  %% ordered eps=1
  ordered_eps_1 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) IFF
     0 < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < beta)

  ordered_det_ge : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) >= det(vi,s) IFF
     0 <= to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) <= beta)

  ordered_eps_neg_1 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) < det(vi,s) IFF
     beta < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < 2*pi)

  %% ordered within eps = 1
  ordered_eps_1_dot_gt_0 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) AND nvo*s > 0 IFF
     0 < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < beta/2)

  ordered_eps_1_dot_ge_0 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) AND nvo*s >= 0 IFF
     0 < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) <= beta/2)

  ordered_eps_1_dot_lt_0 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) AND nvo*s < 0 IFF
     beta/2 < to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < beta)

  ordered_eps_1_dot_le_0 : LEMMA
    abs(det(vi,s)/(norm(nvo)*norm(s))) <= 1 IMPLIES
    LET phi   = track(s),
        psi   = asin(det(vi,s)/(norm(nvo)*norm(s))),
        alpha = phi+psi,
        beta  = pi-2*psi IN
    (det(nvo,s) > det(vi,s) AND nvo*s <= 0 IFF
     beta/2 <= to2pi(track(nvo)-alpha) AND to2pi(track(nvo)-alpha) < beta)

END track

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