Nuprl Definition : prior-classrel-list
prior-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-locl: (e <loc e'),
es-E: E,
sorted-by: sorted-by(R;L),
l_all: (∀x∈L.P[x]),
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
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]
FDL editor aliases :
prior-classrel-list
Latex:
prior-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' <loc e) \mwedge{} (\mexists{}a:A. a \mmember{} X(e')) \mLeftarrow{}{}\mRightarrow{} (e' \mmember{} map(\mlambda{}p.(snd(p));L))))
Date html generated:
2015_07_22-PM-00_17_24
Last ObjectModification:
2012_11_29-AM-11_16_01
Home
Index