Quelle sigma_lemmas.pvs Sprache: PVS

sigma_lemmas: THEORY

% Linear Algebra library
% Heber Herencia-Zapana NIA
% Gilberto Pérez        University of Coruña Spain
% Pablo Ascariz         University of Coruña Spain
% Felicidad Aguado      University of Coruña Spain
% Date: December, 2013

BEGIN

IMPORTING vectors@vectors

%------------------------------------------------------------
% Lemmas about sums
%------------------------------------------------------------

% These lemmas go from more specific to more general
% There are three kinds of lemmas:
% 1. Restricting the domain of the function
% 2. Shifting the domain of the function
% 3. Changing the notation of the domain of the function (although it remains the same)

sigma_restrict_dom: LEMMA FORALL (j: posnat, m: posnat, F: [below[m] -> real],G: [below[m+1] -> real]): (FORALL (i: below[m]): F(i) = G(i)) IMPLIES (j <= m IMPLIES sigma[below[m]](0,j - 1,F) = sigma[below[m+1]](0,j-1,G))

sigma_restrict_dom2:  LEMMA FORALL (j: posnat, m: posnat, F: [below[m] -> real],G: [below[m+1] -> real]): (FORALL (i: below[m]): F(i) = G(i)) IMPLIES (j < m IMPLIES sigma[below[m]](1,j,F) = sigma[below[m+1]](1,j,G))

sigma_below_shift: LEMMA FORALL (m: posnat, F:[below[m + 1] -> real]):  sigma(1, m, LAMBDA (i: below[1 + m]): F(i)) =  sigma(0, m - 1, LAMBDA (i: below[m]): F(i + 1))

sigma_eq_index: LEMMA FORALL (m,n: posnat, F: [below[m] -> real],G: [below[n] -> real]): (m = n AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(0,m - 1,LAMBDA(i: Index[m]): F(i)) = sigma(0,n - 1,LAMBDA(i: Index[n]): G(i))

aux_sigma: LEMMA FORALL (m: posnat,n: nat, F: [below[m] -> real],G: [below[m + n] -> real]): (n = 0 AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(0,m - 1,LAMBDA(i: below[m]): F(i)) = sigma(0,m + n - 1,LAMBDA(i: below[m + n]): G(i))

aux_sigma2: LEMMA FORALL (m,j: posnat,n: nat, F: [below[m] -> real],G: [below[m + n] -> real]): (n = 0 AND j <= m AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(0,j - 1,LAMBDA(i: below[m]): F(i)) = sigma(0,j + n - 1,LAMBDA(i: below[m + n]): G(i))

sigma_restrict_gen: LEMMA FORALL (j: posnat, m,n: posnat, F: [below[m] -> real],G: [below[m + n] -> real]): (FORALL (i: below[m]): F(i) = G(i)) IMPLIES (j <= m IMPLIES sigma[below[m]](0,j - 1,F) = sigma[below[m + n]](0,j-1,G))

sigma_eq_index2: LEMMA FORALL (m,n,j: posnat, F: [below[m] -> real],G: [below[n] -> real]): (m = n AND j <= m AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(0,j - 1,LAMBDA(i: Index[m]): F(i)) = sigma(0,j - 1,LAMBDA(i: Index[n]): G(i))

  sigma_restrict_gen2: LEMMA FORALL (j: posnat,k: nat,m,n: posnat, F: [below[m] -> real],G: [below[m + n] -> real]): (FORALL (i: below[m]): F(i) = G(i)) IMPLIES (j <= m AND k < j IMPLIES sigma[below[m]](k,j - 1,F) = sigma[below[m + n]](k,j-1,G))

sigma_eq_index3: LEMMA FORALL (m,n,j,k: posnat, F: [below[m] -> real],G: [below[n] -> real]): (m = n AND j <= m AND k < j AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(k,j - 1,LAMBDA(i: Index[m]): F(i)) = sigma(k,j - 1,LAMBDA(i: Index[n]): G(i))

sigma_shift_gen: LEMMA FORALL (j: posnat, m,n: posnat,F: [below[m + n] -> real]): (j <= m IMPLIES sigma[below[m]](0,j - 1,LAMBDA (i: below[m]): F(i + n)) = sigma[below[m + n]](n,j - 1 + n, LAMBDA (i: below[m + n]): F(i)))

END sigma_lemmas

quality85%

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.