Nuprl Lemma : rec-combined-class-opt-1-es-sv

[Info,A:Type]. ∀[es:EO+(Info)]. ∀[F:Top]. ∀[X:EClass(A)]. ∀[init:Id ─→ bag(Top)].
  (es-sv-class(es;lifting-2(F)|X,Prior(self)?init|)) supposing (es-sv-class(es;X) and (∀l:Id. (#(init l) ≤ 1)))


Proof




Definitions occuring in Statement :  rec-combined-class-opt-1: F|X,Prior(self)?init| es-sv-class: es-sv-class(es;X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id uimplies: supposing a uall: [x:A]. B[x] top: Top le: A ≤ B all: x:A. B[x] apply: a function: x:A ─→ B[x] natural_number: $n universe: Type lifting-2: lifting-2(f) bag-size: #(bs) bag: bag(T)
Lemmas :  less_than_wf bag-size_wf top_wf rec-combined-class-opt-1_wf lifting-2_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf nat_wf es-sv-class_wf all_wf Id_wf le_wf bag_wf rec-comb-es-sv false_wf int_seg_wf select_wf cons_wf nil_wf sq_stable__le length_wf length_nil non_neg_length length_wf_nil length_cons length_wf_nat bag-combine_wf lelt_wf single-bag_wf decidable__equal_int not-equal-2 add_functionality_wrt_le zero-add add-zero le-add-cancel less-iff-le condition-implies-le add-commutes minus-add minus-zero add-associates le-add-cancel2 subtype_base_sq int_subtype_base bag-size-zero le_weakening bag-combine-empty-left bag_size_empty_lemma bag-size-one bag-combine-single-left bag-only_wf2 single-valued-bag-if-le1 decidable__lt le_antisymmetry_iff bag_size_single_lemma squash_wf true_wf iff_weakening_equal

Latex:
\mforall{}[Info,A:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[F:Top].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(Top)].
    (es-sv-class(es;lifting-2(F)|X,Prior(self)?init|))  supposing 
          (es-sv-class(es;X)  and 
          (\mforall{}l:Id.  (\#(init  l)  \mleq{}  1)))



Date html generated: 2015_07_22-PM-00_16_48
Last ObjectModification: 2015_02_04-PM-04_39_50

Home Index