| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle isomorphism_symmetric.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Isomorphisms are symmetric. % % For PVS version 3.2. January 18, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), 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.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28