### Nuprl Lemma : concat-lifting-loc-member

`∀[B:Type]. ∀[n:ℕ]. ∀[A:ℕn ─→ Type]. ∀[bags:k:ℕn ─→ bag(A k)]. ∀[f:Id ─→ funtype(n;A;bag(B))]. ∀[b:B]. ∀[l:Id].`
`  (b ↓∈ concat-lifting-loc(n;bags;l;f)`
`  `⇐⇒` ↓∃lst:k:ℕn ─→ (A k). ((∀[k:ℕn]. lst k ↓∈ bags k) ∧ b ↓∈ uncurry-rev(n;f l) lst))`

Proof

Definitions occuring in Statement :  concat-lifting-loc: `concat-lifting-loc(n;bags;loc;f)` Id: `Id` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` squash: `↓T` and: `P ∧ Q` apply: `f a` function: `x:A ─→ B[x]` natural_number: `\$n` universe: `Type` uncurry-rev: `uncurry-rev(n;f)` bag-member: `x ↓∈ bs` bag: `bag(T)` funtype: `funtype(n;A;T)`
Lemmas :  concat-lifting-member bag-member_wf concat-lifting-loc_wf squash_wf exists_wf int_seg_wf uall_wf uncurry-rev_wf bag_wf Id_wf funtype_wf nat_wf

Latex:
\mforall{}[B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)].  \mforall{}[f:Id  {}\mrightarrow{}  funtype(n;A;bag(B))].
\mforall{}[b:B].  \mforall{}[l:Id].
(b  \mdownarrow{}\mmember{}  concat-lifting-loc(n;bags;l;f)
\mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}lst:k:\mBbbN{}n  {}\mrightarrow{}  (A  k).  ((\mforall{}[k:\mBbbN{}n].  lst  k  \mdownarrow{}\mmember{}  bags  k)  \mwedge{}  b  \mdownarrow{}\mmember{}  uncurry-rev(n;f  l)  lst))

Date html generated: 2015_07_22-PM-00_08_02
Last ObjectModification: 2015_01_28-AM-11_42_02

Home Index