Nuprl Lemma : State-comb-fun-eq2

[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-res: X@e 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 :  State-comb-fun-eq 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

\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_03
Last ObjectModification: 2015_01_28-AM-10_12_27

Home Index