| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle vect_4D_3D_2D.pvs Sprache: PVS |
|||||||||
|
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 ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28