Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bands_util.pvs Sprache: PVS

Original von: PVS^©

bands_util : THEORY
BEGIN

  % various non-parameterized definitions and lemmas used in bands

  IMPORTING definitions_3D,
            track

  vo3,vi3   : VAR Nzv2_vect3
  x,k,y,trk,vsp   : VAR real
  vo2,vi2,nvo2    : VAR Nz_vect2
  gsp      : VAR posreal
  %----------------------%
  % Definitions bands 2d %
  %----------------------%

  trk2v2(vo2)(trk) : (trk_only?(vo2)) =
    trkgs2vect(trk,norm(vo2))

  trk2v2_Nzv : JUDGEMENT
    trk2v2(vo2)(trk) HAS_TYPE Nz_vect2

  Vtrk(vo2,vi2)(trk:real): Vect2 =
    trk2v2(vo2)(trk) - vi2

  gs2v2(vo2)(k) : Vect2 = k*^(vo2)

  gs2v2_gs_only : JUDGEMENT
    gs2v2(vo2)(gsp) HAS_TYPE (gs_only?(vo2))

  gs2v2_id: LEMMA
    gs_only?(vo2)(nvo2)
    IMPLIES
    gs2v2(vo2)(gs(nvo2)) = nvo2

  %----------------------%
  % Definitions bands 3d %
  %----------------------%

  % Track %

  trk2v3(vo3)(trkz:real) : (trk_only_3D?(vo3)) =
    trkgs2vect(trkz,norm(vect2(vo3))) WITH [z |-> vo3`z]

  vect2_trk2v3 : LEMMA
    vect2(trk2v3(vo3)(trk)) = trk2v2(vo3)(trk)

  trk2v3_Nzv : JUDGEMENT
    trk2v3(vo3)(trk) HAS_TYPE Nzv2_vect3

  Vtrk_3D(vo3,vi3)(trkz:real):(horizontal_only?(vo3-vi3)) =
    trk2v3(vo3)(trkz) - vi3

  trk2v3_trk2v3 : LEMMA
    trk2v3(trk2v3(vo3)(trk))(trk)=trk2v3(vo3)(trk)

  trk2v3_0 : LEMMA
    vect2(vo3) /= zero AND x >= 0 AND x < 2 * pi IMPLIES vect2(trk2v3(vo3)(x)) /= zero

  gs2v3(vo3)(k) : Vect3 = gs2v2(vo3)(k) WITH [z |-> vo3`z]

  gs2v3_gs_only : JUDGEMENT
    gs2v3(vo3)(gsp) HAS_TYPE (gs_only_3D?(vo3))

  vect2_gs2v3 : LEMMA
    vect2(gs2v3(vo3)(gsp)) = gs2v2(vo3)(gsp)

  Vgs_3D(vo3,vi3)(k) : (horizontal_only?(vo3-vi3)) =
    gs2v3(vo3)(k)-vi3

  vs2v3(vo3)(vsp) : (vs_only?(vo3)) = vo3 WITH [z := vsp]

  vect2_vs2v3 : LEMMA
    vect2(vs2v3(vo3)(vsp)) = vect2(vo3)

  Vs(vo3,vi3)(vsp) : (vs_only?(vo3-vi3)) =
    vs2v3(vo3)(vsp)-vi3

END bands_util

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