### Nuprl Lemma : loop-class-memory-fun-eq

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

Proof

Definitions occuring in Statement :  loop-class-memory: `loop-class-memory(X;init)` 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 :  es-local-pred_wf lt_int_wf bag-size_wf eclass3_wf loop-class-memory_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf nat_wf or_wf sq_exists_wf es-locl_wf assert_wf all_wf not_wf es-locl-first assert_elim btrue_neq_bfalse es-loc_wf sv-bag-only_wf decidable__lt false_wf add_functionality_wrt_le add-commutes zero-add le-add-cancel equal_wf assert_of_lt_int member-eclass-iff-size es-pred_property es-pred-locl es-causl_weakening es-pred_wf es-loc-pred less_than_wf member-eclass_wf loop-class-memory-member loop-class-memory-single-val classfun-res_wf assert_functionality_wrt_uiff squash_wf true_wf member-eclass-eclass3 classfun-res-eclass3 iff_weakening_equal single-valued-classrel_wf es-locl-trichotomy bag_wf es-locl_transitivity2 es-le_weakening_eq es-locl_irreflexivity es-causl_transitivity2 es-causle_weakening es-causl_irreflexivity es-le_weakening and_wf eclass3-single-val Id_wf es-pred-loc-base single-valued-bag_wf

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

Date html generated: 2015_07_23-AM-11_29_54
Last ObjectModification: 2015_02_04-PM-04_46_21

Home Index