SSL IUnion_extra.pvs

%%-------------------** Term Rewriting System (TRS) **------------------------
%%                                                                          
%% Authors         : Andre Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%
%%                         and 
%%
%%                   Mauricio Ayala Rincon  
%%                   Universidade de Brasília - Brasil  
%%       
%% Last Modified On: March 24, 2008                                      
%%                                                                          
%%----------------------------------------------------------------------------


IUnion_extra[T: TYPE]: THEORY
  BEGIN


                   i, n: VAR nat
                   x, y: VAR T
                   A, B, 
                   C, D: VAR set[T]


%%%%%%%%%%%% Defining the finite set 1 <= i <= n %%%%%%%%%%%%%%%%%%%%%%%%%%


  upto?(n: posnat): NONEMPTY_TYPE = {i: posnat | i <= n} CONTAINING n



%%%%%%%%%%%% Auxiliar Properties %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  disjoint_subset: LEMMA subset?(A,B) & subset?(C,D) & disjoint?(B,D) 
                            => disjoint?(A,C)

  disjoint_commute: LEMMA disjoint?(A,B) => disjoint?(B,A)

  IUnion_of_finite_is_finite: LEMMA
    FORALL (n: posnat, (f:[upto?(n) -> set[T]])):
      (FORALL (i: upto?(n)): is_finite(f(i)))
       => is_finite(IUnion(LAMBDA (i: upto?(n)): f(i)))


  IUnion_of_finite_is_finite1: LEMMA
    FORALL (n: posnat, (f:[below[n] -> set[T]])):
      (FORALL (i: below[n]): is_finite(f(i)))
       => is_finite(IUnion(LAMBDA (i: below[n]): f(i)))

END IUnion_extra