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

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

Proof

Definitions occuring in Statement :  lifting-loc-gen-rev: `lifting-loc-gen-rev(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` equal: `s = t ∈ T` uncurry-rev: `uncurry-rev(n;f)` bag-member: `x ↓∈ bs` bag: `bag(T)` funtype: `funtype(n;A;T)`
Lemmas :  lifting-member-simple bag-member_wf lifting-loc-gen-rev_wf squash_wf exists_wf int_seg_wf uall_wf uncurry-rev_wf Id_wf funtype_wf bag_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;B)].  \mforall{}[b:B].
\mforall{}[l:Id].
(b  \mdownarrow{}\mmember{}  lifting-loc-gen-rev(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{}  ((uncurry-rev(n;f  l)  lst)  =  b)))

Date html generated: 2015_07_22-PM-00_07_58
Last ObjectModification: 2015_01_28-AM-11_42_09

Home Index