Quellcode-Bibliothek linear_independence_3D.pvs   Sprache: PVS

linear_independence_3D: THEORY
%------------------------------------------------------------------------------
% 
%  EXPERIMENTAL
%
%  Author: Rick Butler    NASA Langley
%
%------------------------------------------------------------------------------
BEGIN

   IMPORTING vectors_3D

   IMPORTING fseqs_ops_vect3, sigma_fseq_3D


   linearly_dependent?(av: fseq[Vect3]): bool = 
        EXISTS (rk: fseq[real]): length(rk) = length(av) AND
                       EXISTS (jj: nat): jj < length(rk) AND rk(jj) /= 0 AND
               sigma(rk*av) = zero
  
   linearly_independent?(av: fseq[Vect3]): bool =  NOT linearly_dependent?(av)         

   IMPORTING cross_3D


   get_around_bug: LEMMA (FORALL (n: int): 0 <= n AND n < 2 
                           IMPLIES n = 0 OR n = 1)

   av: VAR fseq[Vect3]
   test2: LEMMA l(av) = 2 IMPLIES   %% PVS BUG %%
        (linearly_dependent?(av) IFF linearly_dependent?(av(0),av(1)))

% ------------ The following in cross_3D ------------
%
%    linearly_dependent?(a,b: Vect3): bool = 
%        (EXISTS (k1,k2: real): (k1 /= 0 OR k2 /= 0) AND
%                                k1*a + k2*b = zero)
%
%    linearly_independent?(a,b: Vect3): bool = NOT linearly_dependent?(a,b)
%
%     a,b: VAR Nz_vect3
%     lin_indep_cross: LEMMA linearly_dependent?(a,b) IFF
%                               cross(a,b) = zero
 


END linear_independence_3D