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

Proof not projected

Definitions occuring in Statement : classrel: v

X(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: (

x

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

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

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: 2011_10_20-PM-03_44_37 Last ObjectModification: 2011_08_24-PM-02_03_18 Home Index