### Nuprl Lemma : simple-comb-es-sv

`∀[Info,B:Type]. ∀[n:ℕ]. ∀[A:ℕn ─→ Type]. ∀[Xs:k:ℕn ─→ EClass(A k)]. ∀[F:(k:ℕn ─→ bag(A k)) ─→ bag(B)]. ∀[es:EO+(Info)].`
`  (es-sv-class(es;simple-comb(F;Xs))) supposing `
`     ((∀bs:k:ℕn ─→ bag(A k). ((∀k:ℕn. (#(bs k) ≤ 1)) `` (#(F bs) ≤ 1))) and `
`     (∀k:ℕn. es-sv-class(es;Xs k)))`

Proof

Definitions occuring in Statement :  simple-comb: `simple-comb(F;Xs)` es-sv-class: `es-sv-class(es;X)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` int_seg: `{i..j-}` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ─→ B[x]` natural_number: `\$n` universe: `Type` bag-size: `#(bs)` bag: `bag(T)`
Lemmas :  es-E_wf event-ordering+_subtype less_than_wf bag-size_wf simple-comb_wf eclass_wf event-ordering+_wf nat_wf all_wf int_seg_wf bag_wf le_wf es-sv-class_wf

Latex:
\mforall{}[Info,B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[Xs:k:\mBbbN{}n  {}\mrightarrow{}  EClass(A  k)].
\mforall{}[F:(k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k))  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].
(es-sv-class(es;simple-comb(F;Xs)))  supposing
((\mforall{}bs:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k).  ((\mforall{}k:\mBbbN{}n.  (\#(bs  k)  \mleq{}  1))  {}\mRightarrow{}  (\#(F  bs)  \mleq{}  1)))  and
(\mforall{}k:\mBbbN{}n.  es-sv-class(es;Xs  k)))

Date html generated: 2015_07_22-PM-00_16_08
Last ObjectModification: 2015_01_28-AM-10_43_47

Home Index