Nuprl Lemma : bag-member-lifting-loc-2
[C,B,A:Type]. [f:Id 
A B C]. [as:bag(A)]. [bs:bag(B)]. [i:Id]. [c:C].
uiff(c 
lifting-loc-2(f) i as bs;
a:A. b:B. (a as 
b bs (c = (f i a b))))
Proof not projected
Definitions occuring in Statement :
lifting-loc-2: lifting-loc-2(f),
Id: Id,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
exists: x:A. B[x],
squash: T,
and: P Q,
apply: f a,
function: x:A B[x],
universe: Type,
equal: s = t,
bag-member: x bs,
bag: bag(T)
Definitions :
so_lambda: 
x.t[x],
true: True,
member: t T,
uimplies: b supposing a,
and: P Q,
squash: T,
bag-member: x bs,
uiff: uiff(P;Q),
exists: x:A. B[x],
lt_int: i <z j,
bnot: 
b,
le_int: i 
z j,
bfalse: ff,
btrue: tt,
eq_int: (i =
j),
ifthenelse: if b then t else f fi ,
ycomb: Y,
lifting-gen-list-rev: lifting-gen-list-rev(n;bags),
lifting-gen-rev: lifting-gen-rev(n;f;bags),
select: l[i],
lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f),
lifting2-loc: lifting2-loc(f;loc;abag;bbag),
lifting-loc-2: lifting-loc-2(f),
so_apply: x[s],
uall: [x:A]. B[x],
all: x:A. B[x],
rev_uimplies: rev_uimplies(P;Q),
implies: P 
Q,
sq_stable: SqStable(P),
prop: 
Lemmas :
bag_wf,
Id_wf,
equal_wf,
and_wf,
exists_wf,
squash_wf,
lifting-loc-2_wf,
bag-member_wf,
bag-member-single,
single-bag_wf,
bag-combine_wf,
bag-member-combine,
sq_stable__bag-member
\mforall{}[C,B,A:Type]. \mforall{}[f:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} C]. \mforall{}[as:bag(A)]. \mforall{}[bs:bag(B)]. \mforall{}[i:Id]. \mforall{}[c:C].
uiff(c \mdownarrow{}\mmember{} lifting-loc-2(f) i as bs;\mdownarrow{}\mexists{}a:A. \mexists{}b:B. (a \mdownarrow{}\mmember{} as \mwedge{} b \mdownarrow{}\mmember{} bs \mwedge{} (c = (f i a b))))
Date html generated:
2012_01_23-PM-12_54_27
Last ObjectModification:
2011_12_13-PM-05_26_37
Home
Index