| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/series/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 631 B |
|
SSL isomorphism_equivalence.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Equivalence classes of automorphisms. % % For PVS version 3.2. November 4, 2004 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), 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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28