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