Quelle track.pvs Sprache: 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

quality100%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.