classrel-list(es;A;X;L;e) ==
(
p
L.fst(p) X(snd(p)))
sorted-by(
p1,p2.(snd(p1) <loc snd(p2));L)
no_repeats(E;map(p.(snd(p));L))
(e':E. (e' 
loc e (
a:A. a X(e')) 
(e' map(p.(snd(p));L))))
Definitions occuring in Statement :
classrel: v X(e),
es-le: e loc e' ,
es-locl: (e <loc e'),
es-E: E,
map: map(f;as),
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
and: P Q,
lambda: x.A[x],
product: x:A 
B[x],
l_all: (xL.P[x]),
no_repeats: no_repeats(T;l),
l_member: (x l),
sorted-by: sorted-by(R;L)
FDL editor aliases :
classrel-list
classrel-list(es;A;X;L;e) ==
(\mforall{}p\mmember{}L.fst(p) \mmember{} X(snd(p)))
\mwedge{} sorted-by(\mlambda{}p1,p2.(snd(p1) <loc snd(p2));L)
\mwedge{} no\_repeats(E;map(\mlambda{}p.(snd(p));L))
\mwedge{} (\mforall{}e':E. (e' \mleq{}loc e \mwedge{} (\mexists{}a:A. a \mmember{} X(e')) \mLeftarrow{}{}\mRightarrow{} (e' \mmember{} map(\mlambda{}p.(snd(p));L))))
Date html generated:
2011_08_17-PM-06_25_27
Last ObjectModification:
2011_07_24-PM-04_04_37
Home
Index