%-------------------------------------------------------------------------
%
% Isomorphisms are transitive.
%
% For PVS version 3.2. January 18, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), 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
¤ Dauer der Verarbeitung: 0.17 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.
|
