### 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: 2015_07_22-PM-00_14_18
Last ObjectModification: 2012_11_29-AM-11_14_54

Home Index