| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 714 B |
|
Quelle sigma_below_sub.pvs Sprache: PVS |
|||||||||
|
sigma_below_sub[N1,N2: nat]: THEORY
BEGIN IMPORTING sigma_below n0,n,m,i: VAR nat f1: VAR [below(N1) -> real] f2: VAR [below(N2) -> real] sigma_diff_eq: LEMMA n < N1 AND n < N2 AND n0 <= n AND (FORALL i: n0 <= i AND i <= n IMPLIES f1(i) = f2(i)) IMPLIES sigma[below(N1)](n0,n,f1) = sigma[below(N2)](n0,n,f2) sigma_diff_shift: LEMMA n < N1 AND n+m < N2 AND n0 <= n AND (FORALL i: n0 <= i AND i <= n IMPLIES f1(i) = f2(i+m)) IMPLIES sigma[below(N1)](n0,n,f1) = sigma[below(N2)](n0+m,n+m,f2) END sigma_below_sub ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28