Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
isomorphism_symmetric.pvs
Sprache: PVS
%-------------------------------------------------------------------------
%
% 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
[ zur Elbe Produktseite wechseln0.20Quellennavigators
Analyse erneut starten
]
|
|
