|
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.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.
|
