Top File of PVS vectors Library

 
top : THEORY
%----------------------------------------------------------------------------

%
%   Vectors Library V3.0               1/6/2009
%
%   Authors:  Cesar Munoz              National Institute of Aerospace
%             Rick Butler              NASA Langley
%             Ben Di Vito              NASA Langley
%             Jeff Maddalon            NASA Langley
%             Hanne Gottliebsen        National Institute of Aerospace
%
%
%   Strategies: vect-distr, vect-distr-off
%
%----------------------------------------------------------------------------
BEGIN
  IMPORTING 
     vectors,         	  % N-dimensional vectors and operations
     nvectors,            % N-dimensional vectors based on finite sequences 
     vectors_rew,     	  % Adds distributive rewrites
                      	  % See strategies (vect-distr) (vect-distr-off) 
     vect2D,          	  % Define 2-D Vector from N-dimensional vectors
     vect3D,          	  % Define 3-D Vector from N-dimensional vectors

     vectors_2D,       	  % 2-dimensional vectors and operations
     vectors_2D_rew,   	  % Adds distributive rewrites
                      	  % See strategies (vect-distr) (vect-distr-off) 

     vectors_3D,       	  % 3-dimensional vectors and operations
     vectors_3D_rew,   	  % Adds distributive rewrites
                      	  % See strategies (vect-distr) (vect-distr-off) 

     vectors_4D,       	  % 4-dimensional vectors and operations

     vectors_cos,     	  % Law of cosines for n-D vectors 
     vectors_2D_cos,   	  % Law of cosines for 2D vectors 
     vectors_3D_cos,   	  % Law of cosines for 3D vectors 

     distance,        	  % distance function
     distance_2D,      	  % 2D-distance function
     distance_3D,      	  % 3D-distance function

     lines,           	  % Using vectors to define lines, and motion
     lines_2D,         	  % Using vectors to define lines, and motion
     lines_3D,         	  % Using vectors to define lines, and motion

     law_cos_pos_2D,   	  % Law of cosines for 2D positions 
     law_cos_pos_3D,   	  % Law of cosines for 3D positions 

     closest_approach,    % calculate t_cpa for moving particles     
     closest_approach_2D, % calculate t_cpa for moving particles      
     closest_approach_relative_2D, % 
     closest_approach_3D, % calculate t_cpa for moving particles      

     perpendicular_2D,    % line perpendicular to a line through a point
     perpendicular_3D,    % line perpendicular to a line through a point
     intersections_2D,    % finding intersection points of lines
     basis_2D,            % orthonormal basis

     matrices,            % Theory of matrices

     vect_trig_2D,        % trigonometric properties of 2D vectors
     vect_trig_3D,        % trigonometric properties of 3D vectors

     cross_3D,            % cross-product
     linear_independence_3D,   % linear independence
     sigma_2D,            % summations over 2D vectors
     sigma_3D,            % summations over 3D vectors
     sigma_fseq_3D,
     fseqs_ops_vect3,

     vect_3D_2D,          % Projection of a 3D vector (x,y,z) into (x,y) 
     vect_4D_3D_2D,       % Projection of a 4D vector (x,y,z,t) into (x,y,z) and (x,y) 
     det_2D,              % 2D determinant
     parallel_2D,         % 2D parallel
     parallel_3D,         % 3D parallel
     angles_2D,           % angle of vector 
     trackAngles_2D,      % track angles (Air Traffic Management)
     between_2D,          % defines predicate between?(v1,v2)(u)  EXPERIMENTAL

     vect3_basis,
     ECEF,                % Earth-Centered Earth Fixed Cartesian coordinate system

     vect_fun_ops,        % defines function operators
     vect2_fun_ops,
     vect3_fun_ops,
     linear_transformations_2D, % Linear Functions [Vect2 -> Vect2] AND [Vect2 -> real]

     vectors_dot_alt,     % dot product defined using sigma[nat] rather than sigma[below(n)]

     test_vec             % test auto_rewrite+ statements

END top

The tag identifies links that are outside the NASA domain