Nuprl Lemma : State-comb-fun-eq

[Info,B,A:Type]. ∀[f:A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
     if e ∈b then if first(e) then X(e) sv-bag-only(init loc(e)) else X(e) State-comb(init;f;X)(pred(e)) fi 
       if first(e) then sv-bag-only(init loc(e))
       else State-comb(init;f;X)(pred(e))
     ∈ B) supposing 
     (single-valued-classrel(es;X;A) and 
     (∀l:Id. single-valued-bag(init l;B)) and 
     (∀l:Id. (1 ≤ #(init l))))


Definitions occuring in Statement :  State-comb: State-comb(init;f;X) classfun: X(e) single-valued-classrel: single-valued-classrel(es;X;T) member-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-first: first(e) es-pred: pred(e) es-loc: loc(e) es-E: E Id: Id ifthenelse: if then else fi  uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] apply: a function: x:A ─→ B[x] natural_number: $n universe: Type equal: t ∈ T sv-bag-only: sv-bag-only(b) single-valued-bag: single-valued-bag(b;T) bag-size: #(bs) bag: bag(T)
Lemmas :  eqtt_to_assert eqff_to_assert equal_wf bool_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot single-valued-classrel_wf all_wf Id_wf single-valued-bag_wf le_wf bag-size_wf nat_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf bag_wf bag-null_wf assert-bag-null equal-wf-T-base assert_wf bnot_wf eq_int_wf bag_size_empty_lemma es-local-pred_wf lt_int_wf or_wf sq_exists_wf es-locl_wf es-locl-first assert_elim btrue_neq_bfalse not_wf rec-comb_wf 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 lelt_wf lifting-2_wf es-loc_wf sv-bag-only-combine bag-combine_wf single-bag_wf single-valued-classrel-implies-bag member-eclass-iff-size single-valued-bag-single single-valued-bag-combine sv-bag-only_wf decidable__lt add_functionality_wrt_le add-commutes zero-add le-add-cancel bag-member-sv-bag-only bag_size_single_lemma bag-combine-size-bound2 sv-bag-only-single es-first_wf2 bool_cases assert_of_bnot State-comb_wf es-pred_wf less_than_wf assert_of_lt_int iff_transitivity iff_weakening_uiff State-comb-single-val iff_weakening_equal State-comb-exists squash_wf true_wf reduce_hd_cons_lemma State-comb-exists-iff not-gt-2 bag-member-size member-eclass-iff-non-empty State-comb-functional btrue_wf and_wf isl_wf bfalse_wf

\mforall{}[Info,B,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
          =  if  e  \mmember{}\msubb{}  X
                  then  if  first(e)
                            then  f  X(e)  sv-bag-only(init  loc(e))
                            else  f  X(e)  State-comb(init;f;X)(pred(e))
              if  first(e)  then  sv-bag-only(init  loc(e))
              else  State-comb(init;f;X)(pred(e))
              fi  )  supposing 
          (single-valued-classrel(es;X;A)  and 
          (\mforall{}l:Id.  single-valued-bag(init  l;B))  and 
          (\mforall{}l:Id.  (1  \mleq{}  \#(init  l))))

Date html generated: 2015_07_22-PM-00_22_00
Last ObjectModification: 2015_02_04-PM-04_44_00

Home Index