|
%--------------------------------------------------------------%
% Author: Dragan Stosic %
%--------------------------------------------------------------%
relation_extension[T, U: TYPE+]: THEORY
BEGIN
le_T: VAR equivalence[T]
le_U: VAR equivalence[U]
m, n: VAR [T, U]
f: VAR [T -> U]
g: VAR [U -> T]
R: VAR equivalence[[T, U]]
p_r1: VAR [[[T,U] -> T]]
p_r2: VAR [[[T,U] -> U]]
proj_tuple_1: [[[T,U] -> T]] = LAMBDA (m:[T,U]): m`1
proj_tuple_2: [[[T,U] -> U]] = LAMBDA (m:[T,U]): m`2
extended_equiv_class(R)(m): set[[T,U]] = { n | R(m, n) }
extended_equiv_classT(R, p_r1, m, n) : set[T] =
{ (t : T) | t= p_r1(m) AND extended_equiv_class(R)(n)(m) }
extended_equiv_classU(R, p_r2, m, n) : set[U] =
{ (u : U) | u= p_r2(m) AND extended_equiv_class(R)(n)(m) }
% extended equivalence relation based on two equivalence
% relations : le_T , le_U
rel_extension(le_T, le_U) : set[[[T, U], [T, U]]] =
{ (m, n) | le_T(m`1, n`1) AND le_U(m`2, n`2) }
rel_extension_is_equivalence: JUDGEMENT
rel_extension(le_T, le_U) HAS_TYPE equivalence[[T, U]]
% class representative for the rel_extension equivalence relation
repEC_ext(le_T, le_U, m): [[T, U]] = repEC(rel_extension(le_T, le_U))(m)
END relation_extension
¤ Dauer der Verarbeitung: 0.12 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.
|
