%-------------------------------------------------------------------------
%
% Properties of similar sets.
%
% For PVS version 3.2. March 5, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[D], orders[R]
% finite_sets: finite_sets_inductions, finite_sets_minmax
% orders: bounded_orders[D], bounded_orders[R], closure_ops[D],
% closure_ops[R], finite_below[D], finite_below[R], indexed_sets_extra,
% isomorphism[D,R], minmax_orders[D], minmax_orders[R],
% relations_extra[D], relations_extra[R], relation_iterate[D],
% relation_iterate[R], similarity[D,R], similarity_props[D,R]
%
%-------------------------------------------------------------------------
similarity_props[D: TYPE, R: TYPE]: THEORY
BEGIN
IMPORTING minmax_orders[D], minmax_orders[R]
IMPORTING similarity[D, R], finite_below[D], finite_below[R]
Dord: VAR (total_order?[D])
Rord: VAR (total_order?[R])
f: VAR (bijective?[D, R])
d: VAR D
similarity_greatest: LEMMA
FORALL Dord, Rord, f, d:
similarity?(Dord, Rord)(f) AND greatest?(d, fullset[D], Dord) IMPLIES
greatest?(f(d), fullset[R], Rord)
similar_has_greatest: COROLLARY
FORALL Dord, Rord:
similar?(Dord, Rord) AND has_greatest?(fullset[D], Dord) IMPLIES
has_greatest?(fullset[R], Rord)
similarity_least: LEMMA
FORALL Dord, Rord, f, d:
similarity?(Dord, Rord)(f) AND least?(d, fullset[D], Dord) IMPLIES
least?(f(d), fullset[R], Rord)
similar_has_least: COROLLARY
FORALL Dord, Rord:
similar?(Dord, Rord) AND has_least?(fullset[D], Dord) IMPLIES
has_least?(fullset[R], Rord)
similar_finite: LEMMA
is_finite_type[D] AND
is_finite_type[R] AND card(fullset[D]) = card(fullset[R])
IMPLIES (FORALL Dord, Rord: similar?(Dord, Rord))
END similarity_props
¤ Dauer der Verarbeitung: 0.15 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.
|
