|
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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
