Quellcode-Bibliothek bands_util.pvs Sprache: 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

quality100%

¤ 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.11Bemerkung: (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.