Nuprl Lemma : apply-Id-alist-function
[x:Id]. [F:Top]. [L:Id List]. apply-alist(IdDeq;map(
x.<x, F[x]>;L);x) ~ inl F[x] supposing (x 
L)
Proof not projected
Definitions occuring in Statement :
id-deq: IdDeq,
Id: Id,
map: map(f;as),
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
lambda: x.A[x],
pair: <a, b>,
inl: inl x ,
list: type List,
sqequal: s ~ t,
l_member: (x l),
apply-alist: apply-alist(eq;L;x)
Definitions :
bfalse: ff,
guard: {T},
btrue: tt,
ycomb: Y,
pi2: snd(t),
pi1: fst(t),
ifthenelse: if b then t else f fi ,
all: x:A. B[x],
implies: P 
Q,
member: t T,
map: map(f;as),
apply-alist: apply-alist(eq;L;x),
uimplies: b supposing a,
Id: Id,
uall: [x:A]. B[x],
not: 
A,
sq_type: SQType(T),
uiff: uiff(P;Q),
unit: Unit,
bool: 
,
or: P 
Q,
and: P 
Q,
iff: P 
Q,
false: False,
eq_id: a = b,
it: 
,
prop: 
Lemmas :
l_member_wf,
top_wf,
not_functionality_wrt_uiff,
assert_of_bnot,
eqff_to_assert,
not_wf,
bnot_wf,
atom2_subtype_base,
subtype_base_sq,
assert-eq-id,
eqtt_to_assert,
assert_wf,
equal_wf,
uiff_transitivity,
bool_wf,
eq_id_wf,
cons_member,
Id_wf,
nil_member
\mforall{}[x:Id]. \mforall{}[F:Top]. \mforall{}[L:Id List].
apply-alist(IdDeq;map(\mlambda{}x.<x, F[x]>L);x) \msim{} inl F[x] supposing (x \mmember{} L)
Date html generated:
2012_01_23-AM-11_53_06
Last ObjectModification:
2011_12_09-PM-07_12_47
Home
Index