%-------------------------------------------------------------------------
%
% Equivalence classes of automorphisms.
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[T], relations[pred[[T, T]]], relations[T]
% orders: isomorphism[T,T], isomorphism_equivalence[T], relations_extra[T]
%
%-------------------------------------------------------------------------
isomorphism_equivalence[T: TYPE]: THEORY
EXPORTING ALL WITH orders[T], relations[pred[[T, T]]], relations[T],
isomorphism[T, T], relations_extra[T]
BEGIN
IMPORTING function_inverse_def[T, T] % Proofs only
IMPORTING relations[pred[[T, T]]], isomorphism[T, T]
isomorphism_reflexive: THEOREM reflexive?(isomorphic?)
isomorphism_symmetric: THEOREM symmetric?(isomorphic?)
isomorphism_transitive: THEOREM transitive?(isomorphic?)
isomorphism_equivalence: JUDGEMENT
isomorphic? HAS_TYPE equivalence[pred[[T, T]]]
END isomorphism_equivalence
¤ Dauer der Verarbeitung: 0.20 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.
|
