product_fseq_posnat.pvs

product_fseq_posnat: THEORY
%-------------------------------------------------------------------------------
%
%  products over finite sequences of posnats
%
%  Author: Rick Butler    NASA Langley
%
%  NOTE: Later we may derive this theory from product_fseq
%
%-------------------------------------------------------------------------------
BEGIN

   

   IMPORTING structures@fseqs[posnat], product_nat

   unk: VAR fsq[posnat]
   fs,fs1,fs2: VAR fseq    
   n,m: VAR nat

   F: VAR [nat -> posnat]

   product_nat_nat: JUDGEMENT product(m,n,F) HAS_TYPE posnat

   product(fs): posnat = IF length(fs) = 0 THEN 1
                         ELSE product(0,length(fs)-1,fs`seq)
                         ENDIF

   len0: LEMMA length(fs) = 0 IMPLIES product(fs) = 1

   l1,l2: VAR nat

   product_fseq_shift: LEMMA  product(l1, l1 + l2 - 1,
                                 LAMBDA (n: nat): IF n < l1 THEN unk`seq(n)
                                                  ELSE fs`seq(n - l1)  ENDIF)
                         = product(0, l2 - 1, fs`seq)


   product_fseq_concat: LEMMA product(fs1 o fs2) = product(fs1) * product(fs2)


   product_fseq_empty_seq: LEMMA product(empty_seq) = 1

   product_fseq_split: LEMMA length(fs) > 1 IMPLIES
                            product(fs) = product(fs ^ (0, length(fs) - 2)) * 
                                           seq(fs)(length(fs) - 1) 

   product_fseq_ge: LEMMA FORALL (n: below(length(fs))): product(fs) >= seq(fs)(n)


   nn: VAR posnat
   product_fseq_concat1:  LEMMA nn * product(fs)  = product(fs o fseq1(nn))

   product_fseq1:  LEMMA product(fseq1(nn)) = nn

END product_fseq_posnat