Quelle  isomorphism_transitive.pvs

%-------------------------------------------------------------------------
%
%  Isomorphisms are transitive.
%
%  For PVS version 3.2.  January 18, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: orders[T1], orders[T2], orders[T3], relations[T1],
%    relations[T2], relations[T3]
%  orders: isomorphism[T1,T2], isomorphism[T1,T3], isomorphism[T2,T3],
%    isomorphism_transitive[T1,T2,T3], relations_extra[T1],
%    relations_extra[T2], relations_extra[T3]
%
%-------------------------------------------------------------------------
isomorphism_transitive[T1: TYPE, T2: TYPE, T3: TYPE]: THEORY
 BEGIN

  IMPORTING isomorphism[T1, T2], isomorphism[T2, T3], isomorphism[T1, T3]

  rel1: VAR pred[[T1, T1]]
  rel2: VAR pred[[T2, T2]]
  rel3: VAR pred[[T3, T3]]

  isomorphism_transitive: THEOREM
    FORALL rel1, rel2, rel3:
      isomorphic?(rel1, rel2) AND isomorphic?(rel2, rel3) =>
       isomorphic?(rel1, rel3)

 END isomorphism_transitive