| 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 det_2D.pvs Sprache: PVS |
|||||||||
|
det_2D: THEORY
%------------------------------------------------------------------------------ % % 2-Dimensional Determinant of two vectors (aka 2D-cross product) % % %------------------------------------------------------------------------------ BEGIN IMPORTING vectors_2D, perpendicular_2D u,v,w : VAR Vect2 k : VAR real nzu,nzv : VAR Nz_vect2 det(u,v): real = u`x*v`y - u`y*v`x det_zero_left : LEMMA det(zero,v) = 0 det_zero_right : LEMMA det(u,zero) = 0 det_eq_0 : LEMMA det(u,u) = 0 det_scal_left : LEMMA det(k*u,v) = k*det(u,v) det_scal_right : LEMMA det(u,k*v) = k*det(u,v) det_add_left : LEMMA det(u+v,w) = det(u,w) + det(v,w) det_add_right : LEMMA det(w,u+v) = det(w,u) + det(w,v) det_sub_left : LEMMA det(u-v,w) = det(u,w) - det(v,w) det_sub_right : LEMMA det(w,u-v) = det(w,u) - det(w,v) det_symm : LEMMA det(u,v) = det(-u,-v) det_asym : LEMMA det(u,v) = -det(v,u) det_symm_0 : LEMMA det(u,v) = 0 IFF det(v,u) = 0 sq_det : LEMMA sq(det(u,v)) = sqv(v)*sqv(u) - sq(u*v) det_norm : LEMMA det(u,v) <= norm(u)*norm(v) det_perpR : LEMMA det(u,v) = u*perpR(v) det_perpL : LEMMA det(u,v) = perpL(u)*v dot_perpR : LEMMA u*v = -det(u,perpR(v)) dot_perpL : LEMMA u*v = -det(perpL(u),v) perpR_dot : LEMMA perpR(u)*v = -det(u,v) perpL_dot : LEMMA u*perpL(v) = -det(u,v) det_dot_0 : LEMMA det(nzu,nzv) = 0 IMPLIES nzu*nzv /= 0 AUTO_REWRITE+ det_eq_0 END det_2D ¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28