product_seq_scaf.pvs

product_seq_scaf: THEORY
BEGIN


   IMPORTING finite_sequences[posnat]

   fs: VAR finite_sequence

   product_rec(fs: finite_sequence, i: below(length(fs)) ): RECURSIVE posnat = 
                 IF i = 0 THEN seq(fs)(0)
                 ELSE seq(fs)(i) * product_rec(fs,i-1)
                 ENDIF MEASURE i

   fs1,fs2: VAR finite_sequence
   n,m: VAR nat

   product_rec_mult: LEMMA n < length(fs1 o fs2) IMPLIES
                   product_rec(fs1 o fs2,n) = 
                          IF n < length(fs1) THEN
                             product_rec(fs1,n)
                          ELSIF length(fs1) = 0 THEN
                             product_rec(fs2,n)
                          ELSE
                             product_rec(fs1,length(fs1)-1) 
                             * product_rec(fs2,n-length(fs1))
                          ENDIF

   product_rec_caret: LEMMA n < length(fs) AND m < length(fs) 
                               AND n <= m IMPLIES product_rec(fs, n) =
                               product_rec(fs ^ (0, m), n)

END product_seq_scaf