Nuprl Lemma : loop-class-state-fun-eq

∀[Info,B:Type]. ∀[init:Id ─→ bag(B)]. ∀[X:EClass(B ─→ B)]. ∀[es:EO+(Info)]. ∀[e:E].
(loop-class-state(X;init)(e)

     = if e ∈_b X then if first(e) then X@e sv-bag-only(init loc(e)) else X@e loop-class-state(X;init)(pred(e)) fi

       if first(e) then sv-bag-only(init loc(e))
       else loop-class-state(X;init)(pred(e))
       fi
     ∈ B) supposing
     ((∀l:Id. single-valued-bag(init l;B)) and
     single-valued-classrel(es;X;B ─→ B) and
     (∀l:Id. (1 ≤ #(init l))))

Proof

Definitions occuring in Statement : loop-class-state: loop-class-state(X;init), 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 : eqtt_to_assert, eqff_to_assert, equal_wf, bool_wf, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, assert-bnot, all_wf, Id_wf, single-valued-bag_wf, single-valued-classrel_wf, le_wf, bag-size_wf, nat_wf, es-E_wf, event-ordering+_subtype, event-ordering+_wf, eclass_wf, bag_wf, member-eclass_wf, primed-class-opt-cases, loop-class-state_wf, es-interface-subtype_rel2, es-first_wf2, sv-bag-only-combine, bag-map_wf, es-loc_wf, single-valued-classrel-implies-bag, member-eclass-iff-size, bag-size-map, decidable__lt, false_wf, add_functionality_wrt_le, add-commutes, zero-add, le-add-cancel, classfun-res_wf, sv-bag-only_wf, iff_weakening_equal, single-valued-bag-map, sv-bag-only-map2, lt_int_wf, es-pred_wf, assert_of_lt_int, less_than_wf, squash_wf, true_wf, loop-class-state-single-val, assert-member-eclass, loop-class-state-exists

Latex:
\mforall{}[Info,B:Type]. \mforall{}[init:Id {}\mrightarrow{} bag(B)]. \mforall{}[X:EClass(B {}\mrightarrow{} B)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. (loop-class-state(X;init)(e) = if e \mmember{}\msubb{} X then if first(e) then X@e sv-bag-only(init loc(e)) else X@e loop-class-state(X;init)(pred(e)) fi if first(e) then sv-bag-only(init loc(e)) else loop-class-state(X;init)(pred(e)) fi ) supposing ((\mforall{}l:Id. single-valued-bag(init l;B)) and single-valued-classrel(es;X;B {}\mrightarrow{} B) and (\mforall{}l:Id. (1 \mleq{} \#(init l)))) Date html generated: 2015_07_21-PM-02_34_04 Last ObjectModification: 2015_02_04-PM-06_24_39 Home Index