| 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 |
|
Quellcode-Bibliothek similarity.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Similar ordered sets. Two totally ordered sets are similar if there % exists an bijective function from the first to the second that % preserves ordering. This is a special case of isomorphism. % % For PVS version 3.2. March 5, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: orders[D], orders[R] % orders: isomorphism[D,R], similarity[D,R] % %------------------------------------------------------------------------- similarity[D: TYPE, R: TYPE]: THEORY BEGIN IMPORTING isomorphism[D, R] Dord: VAR (total_order?[D]) Rord: VAR (total_order?[R]) f: VAR (bijective?[D, R]) similarity?(Dord, Rord)(f): bool = preserves(f, Dord, Rord) similar?(Dord, Rord): bool = EXISTS f: similarity?(Dord, Rord)(f) similarity_is_isomorphism: LEMMA FORALL Dord, Rord, f: similarity?(Dord, Rord)(f) IMPLIES isomorphism?(Dord, Rord)(f) similar_is_isomorphic: COROLLARY FORALL Dord, Rord: similar?(Dord, Rord) IMPLIES isomorphic?(Dord, Rord) END similarity ¤ 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.0.13Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28