Nuprl Lemma : rec-comb-es-sv

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


Definitions occuring in Statement :  rec-comb: rec-comb(X;f;init) es-sv-class: es-sv-class(es;X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] implies:  Q apply: a function: x:A ─→ B[x] natural_number: $n universe: Type bag-size: #(bs) bag: bag(T)
Lemmas :  es-causl-swellfnd event-ordering+_subtype nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf bag-size_wf rec-comb_wf2 nat_wf es-E_wf le_wf decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__lt es-causl_wf eclass_wf event-ordering+_wf es-loc_wf primed-class-opt_wf primed-class-opt-es-sv0 es-locl_wf zero-le-nat add-mul-special zero-mul all_wf int_seg_wf bag_wf Id_wf es-sv-class_wf

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

Date html generated: 2015_07_22-PM-00_15_27
Last ObjectModification: 2015_01_28-AM-10_45_46

Home Index