|
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
