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].

(State-comb(init;f;X)(e)

     = if e ∈_b 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)) fi

       if first(e) then sv-bag-only(init loc(e))
       else State-comb(init;f;X)(pred(e))
       fi
     ∈ B) supposing
     (single-valued-classrel(es;X;A) and
     (∀l:Id. single-valued-bag(init l;B)) and
     (∀l:Id. (1 ≤ #(init l))))

Proof

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 b then t else f fi , uimplies: b supposing a, uall: ∀[x:A]. B[x], le: A ≤ B, all: ∀x:A. B[x], apply: f a, function: x:A ─→ B[x], natural_number: $n, universe: Type, equal: s = 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

Latex:
\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]. (State-comb(init;f;X)(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)) fi 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