%-------------------------------------------------------------------------
%
% Isomorphisms are symmetric.
%
% For PVS version 3.2. January 18, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[T1], orders[T2], relations[T1], relations[T2]
% orders: isomorphism[T1,T2], isomorphism[T2,T1],
% isomorphism_symmetric[T1,T2], relations_extra[T1], relations_extra[T2]
%
%-------------------------------------------------------------------------
isomorphism_symmetric[T1: TYPE, T2: TYPE]: THEORY
EXPORTING ALL WITH orders[T1], orders[T2], relations[T1], relations[T2],
isomorphism[T1, T2], isomorphism[T2, T1],
relations_extra[T1], relations_extra[T2]
BEGIN
IMPORTING function_inverse_def[T1, T2] % Proofs only
IMPORTING function_inverse_def[T2, T1] % Proofs only
IMPORTING isomorphism[T1, T2], isomorphism[T2, T1]
rel1: VAR pred[[T1, T1]]
rel2: VAR pred[[T2, T2]]
isomorphism_symmetric: THEOREM
FORALL rel1, rel2: isomorphic?(rel1, rel2) IFF isomorphic?(rel2, rel1)
END isomorphism_symmetric
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
