%-------------------------------------------------------------------------
%
% 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
