Nuprl Definition : classrel-multi-list
classrel-multi-list(es;A;Xs;L;e;n1;n2) ==
(∀x:n:{n1..n2-} × A n × E
((x ∈ L) ⇒ (fst(snd(x)) ∈ Xs (fst(x))(snd(snd(x))) ∧ (∀m:{n1..fst(x)-}. ∀v:A m. (¬v ∈ Xs m(snd(snd(x))))))))
∧ sorted-by(λp1,p2. (snd(snd(p1)) <loc snd(snd(p2)));L)
∧ no_repeats(E;map(λp.(snd(snd(p)));L))
∧ (∀e':E
(e' ≤loc e ∧ (∃n:{n1..n2-}. ∃a:A n. (a ∈ Xs n(e') ∧ (∀m:{n1..n-}. ∀v:A m. (¬v ∈ Xs m(e')))))
⇐⇒ (e' ∈ map(λp.(snd(snd(p)));L))))
Definitions occuring in Statement :
classrel: v ∈ X(e),
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-E: E,
sorted-by: sorted-by(R;L),
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
map: map(f;as),
int_seg: {i..j-},
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
product: x:A × B[x]
FDL editor aliases :
classrel-multi-list
Latex:
classrel-multi-list(es;A;Xs;L;e;n1;n2) ==
(\mforall{}x:n:\{n1..n2\msupminus{}\} \mtimes{} A n \mtimes{} E
((x \mmember{} L)
{}\mRightarrow{} (fst(snd(x)) \mmember{} Xs (fst(x))(snd(snd(x)))
\mwedge{} (\mforall{}m:\{n1..fst(x)\msupminus{}\}. \mforall{}v:A m. (\mneg{}v \mmember{} Xs m(snd(snd(x))))))))
\mwedge{} sorted-by(\mlambda{}p1,p2. (snd(snd(p1)) <loc snd(snd(p2)));L)
\mwedge{} no\_repeats(E;map(\mlambda{}p.(snd(snd(p)));L))
\mwedge{} (\mforall{}e':E
(e' \mleq{}loc e
\mwedge{} (\mexists{}n:\{n1..n2\msupminus{}\}. \mexists{}a:A n. (a \mmember{} Xs n(e') \mwedge{} (\mforall{}m:\{n1..n\msupminus{}\}. \mforall{}v:A m. (\mneg{}v \mmember{} Xs m(e')))))
\mLeftarrow{}{}\mRightarrow{} (e' \mmember{} map(\mlambda{}p.(snd(snd(p)));L))))
Date html generated:
2016_05_17-AM-09_26_04
Last ObjectModification:
2012_11_29-AM-11_14_54
Theory : classrel!lemmas
Home
Index