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)
}
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.
