Quelle  function_props_aux.pvs

% Additions to standard prelude theories function_props, and function_props_alt
%
% David Lester, Manchester University, NIA, Université Perpignan 8/6/06


function_props_aux[T1,T2,T3:TYPE]: THEORY

BEGIN

  f1: VAR [T1->T2]
  f2: VAR [T2->T3]
  Y:  VAR set[T3]

  inverse_image_composition: LEMMA
    inverse_image(f1, inverse_image(f2,Y)) = inverse_image(f2 o f1, Y)


  composition_inverse_alt: LEMMA FORALL (f1:(bijective?[T1,T2]),
                                         f2:(bijective?[T2,T3])):
                                 inverse_alt(f2 o f1)
                                          = inverse_alt(f1) o inverse_alt(f2)

END function_props_aux