products/sources/formale sprachen/PVS/vectors/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: constrextern.ml   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.4 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff