|
%--------------------------------------------------------------%
% Author: Dragan Stosic %
%--------------------------------------------------------------%
rr_rel[T, U: TYPE+]: THEORY
BEGIN
IMPORTING relation_extension[T, U],
relation_inverse_extension[T, U]
le_T: VAR equivalence[T]
le_U: VAR equivalence[U]
n: VAR [T, U]
f: VAR [T -> U]
g: VAR [U -> T]
% Definition 1:
% Relation [T, U]
% Domain T partitioned with the le_T equivalence relation
% Codomain U partitioned with the le_U equivalence relation
% Functions: f[ T -> U] and g [U -> T]
RR(le_T, le_U, f, g):set[[T,U]] =
{ (n) | LET Fn = (n`1,f(n`1)),
Gn = (g(n`2), n`2),
GFn = (g(n`2), f(n`1)) IN
rel_extension(le_T, le_U)(Fn, Gn) OR
rel_extension(le_T, le_U)(GFn, Fn) OR
rel_extension(le_T, le_U)(GFn, Gn)
}
% Definition 2:
% Relation [T, U]
% Domain T partitioned with the le_T equivalence relation
% Codomain U partitioned with the le_U equivalence relation
% Functions: f[ T -> U] and g [U -> T]
RR2(le_T, le_U, f, g):set[[T,U]] =
{ (n) | LET Fn = (n`1,f(n`1)),
Gn = (g(n`2), n`2),
GFn = (g(n`2), f(n`1)) IN
rel_inv_extension2(le_T, le_U, f, g)(Fn, Gn) OR
rel_inv_extension2(le_T, le_U, f, g)(GFn, Fn) OR
rel_inv_extension2(le_T, le_U, f, g)(GFn, Gn)
}
g_conistent_with_RR: LEMMA
le_T( n`1, g(n`2) ) IMPLIES RR(le_T, le_U, f, g)(n)
f_conistent_with_RR: LEMMA
le_U( n`2, f(n`1) ) IMPLIES RR(le_T, le_U, f, g)(n)
% Connection between RR and RR2
RR_functional_conditional_equal_RR2: LEMMA
LET GFn=(g(n`2),f(n`1)) IN
RR(le_T, le_U, f, g)(GFn) IFF RR2(le_T, le_U, f, g)(n)
END rr_rel
¤ Dauer der Verarbeitung: 0.1 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.
|
