Quelle  rr_rel.pvs

%--------------------------------------------------------------%
%   Author: Dragan Stosic                                      %
%--------------------------------------------------------------%

rr_rel[T, U: TYPE+]: THEORY
 BEGIN
  IMPORTING relation_extension[T, U],
            relation_inverse_extension[T, U]

 le_T: VAR equivalence[T]

 le_U: VAR equivalence[U]

 n: VAR [T, U]

 f: VAR [T -> U]

 g: VAR [U -> T]

% Definition 1:
% Relation [T, U]
% Domain T partitioned with the le_T equivalence relation 
% Codomain U  partitioned with the le_U equivalence relation 
% Functions: f[ T -> U] and g [U -> T]

 RR(le_T, le_U, f, g):set[[T,U]] = 
   { (n) | LET Fn = (n`1,f(n`1)), 
                 Gn  = (g(n`2), n`2), 
                   GFn  = (g(n`2), f(n`1))  IN 
                     rel_extension(le_T, le_U)(Fn, Gn)     OR
                       rel_extension(le_T, le_U)(GFn, Fn)  OR
                         rel_extension(le_T, le_U)(GFn, Gn)  
   }

% Definition 2:
% Relation [T, U]
% Domain T partitioned with the le_T equivalence relation 
% Codomain U  partitioned with the le_U equivalence relation 
% Functions: f[ T -> U] and g [U -> T]

RR2(le_T, le_U, f, g):set[[T,U]] = 
   { (n) | LET Fn = (n`1,f(n`1)), 
                 Gn  = (g(n`2), n`2), 
                   GFn  = (g(n`2), f(n`1))  IN 
                     rel_inv_extension2(le_T, le_U, f, g)(Fn, Gn)     OR
                       rel_inv_extension2(le_T, le_U, f, g)(GFn, Fn)  OR
                         rel_inv_extension2(le_T, le_U, f, g)(GFn, Gn)  
   }

 g_conistent_with_RR: LEMMA 
   le_T( n`1, g(n`2) ) IMPLIES RR(le_T, le_U, f, g)(n)  
 
 f_conistent_with_RR: LEMMA 
   le_U( n`2, f(n`1) ) IMPLIES RR(le_T, le_U, f, g)(n)  


% Connection between RR and RR2
 
 RR_functional_conditional_equal_RR2: LEMMA
    LET GFn=(g(n`2),f(n`1)) IN 
      RR(le_T, le_U, f, g)(GFn) IFF  RR2(le_T, le_U, f, g)(n)
 
END rr_rel