Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: vect_3D_2D.pvs Sprache: PVS

Original von: PVS^©

vect_3D_2D: THEORY
BEGIN

  IMPORTING vectors_2D, vectors_3D

  vect2(v:Vect3): Vect2 = (v`x,v`y)

  CONVERSION vect2

  v2   : VAR Vect2
  v,w  : VAR Vect3
  a,vz : VAR real

  vect2_add : LEMMA
    vect2(v+w) = vect2(v) + vect2(w)

  vect2_sub   : LEMMA
    vect2(v-w) = vect2(v) - vect2(w)

  vect2_scal : LEMMA
    vect2(a*v) = a*vect2(v)

  vect2_neg : LEMMA
    vect2(-v)  = -vect2(v)

  vect2_zero  : LEMMA
    vect2(zero) = zero

  vect2_eq : LEMMA
     vect2(v WITH [z := vz]) = vect2(v)

  vect2_eq_ext : LEMMA
     vect2(v2 WITH [z |-> vz]) = v2

  vect2_ext_id :LEMMA
    vect2(v) WITH [z |-> v`z] = v

  AUTO_REWRITE+ vect2_zero
  AUTO_REWRITE+ vect2_eq
  AUTO_REWRITE+ vect2_eq_ext
  AUTO_REWRITE+ vect2_ext_id

END vect_3D_2D

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