|
vect_4D_3D_2D: THEORY
BEGIN
IMPORTING vectors_2D, vectors_3D, vectors_4D
vect2(v:Vect4): Vect2 = (v`x,v`y)
vect3(v:Vect4): Vect3 = (v`x,v`y,v`z)
CONVERSION vect2
CONVERSION vect3
v2 : VAR Vect2
v3 : VAR Vect3
v,w : VAR Vect4
a,vz,vt : 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] WITH [t |-> vt]) = v2
vect2_ext_id :LEMMA
vect2(v) WITH [z |-> v`z] WITH [t |-> v`t] = v
AUTO_REWRITE+ vect2_zero
AUTO_REWRITE+ vect2_eq
AUTO_REWRITE+ vect2_eq_ext
AUTO_REWRITE+ vect2_ext_id
vect3_add : LEMMA
vect3(v+w) = vect3(v) + vect3(w)
vect3_sub : LEMMA
vect3(v-w) = vect3(v) - vect3(w)
vect3_scal : LEMMA
vect3(a*v) = a*vect3(v)
vect3_neg : LEMMA
vect3(-v) = -vect3(v)
vect3_zero : LEMMA
vect3(zero) = zero
vect3_eq : LEMMA
vect3(v WITH [t := vt]) = vect3(v)
vect3_eq_ext : LEMMA
vect3(v3 WITH [t |-> vt]) = v3
vect3_ext_id :LEMMA
vect3(v) WITH [t |-> v`t] = v
AUTO_REWRITE+ vect3_zero
AUTO_REWRITE+ vect3_eq
AUTO_REWRITE+ vect3_eq_ext
AUTO_REWRITE+ vect3_ext_id
END vect_4D_3D_2D
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.7Angebot
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
|
