### 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) as bs;↓∃a:A. ∃b:B. (a ↓∈ as ∧ b ↓∈ bs ∧ (c (f b) ∈ C)))

Proof

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: a function: x:A ─→ B[x] universe: Type equal: t ∈ T bag-member: x ↓∈ bs bag: bag(T)
Lemmas :  bag-member_wf lifting-loc-2_wf squash_wf exists_wf Id_wf bag_wf bag-member-combine bag-combine_wf single-bag_wf bag-member-single sq_stable__bag-member

Latex:
\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: 2015_07_22-PM-00_07_53
Last ObjectModification: 2015_01_28-AM-11_42_26

Home Index