Nuprl Definition : classrel-multi-list

classrel-multi-list(es;A;Xs;L;e;n1;n2) ==
(

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))))

Proof not projected

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), 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, and: P

Q, apply: f a, lambda:

x.A[x], product: x:A

B[x], l_all: (

x

L.P[x]), no_repeats: no_repeats(T;l), l_member: (x

l), sorted-by: sorted-by(R;L)
FDL editor aliases : classrel-multi-list

classrel-multi-list(es;A;Xs;L;e;n1;n2) == (\mforall{}x\mmember{}L.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: 2011_10_20-PM-03_35_45 Last ObjectModification: 2011_08_15-PM-01_14_25 Home Index