### Nuprl Lemma : Memory-classrel1

`∀[Info,B,A:Type]. ∀[f:A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].`
`  uiff(v ∈ Memory-class(f;init;X)(e);↓((↑first(e)) ∧ v ↓∈ init loc(e))`
`                                      ∨ ((¬↑first(e))`
`                                        ∧ ((∃a:A`
`                                             (a ∈ X(pred(e))`
`                                             ∧ (∃b:B. (b ∈ Memory-class(f;init;X)(pred(e)) ∧ (v = (f a b) ∈ B)))))`
`                                          ∨ ((∀a:A. (¬a ∈ X(pred(e)))) ∧ v ∈ Memory-class(f;init;X)(pred(e))))))`

Proof

Definitions occuring in Statement :  Memory-class: `Memory-class(f;init;X)` classrel: `v ∈ X(e)` 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` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` squash: `↓T` or: `P ∨ Q` and: `P ∧ Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T` bag-member: `x ↓∈ bs` bag: `bag(T)`
Lemmas :  es-first_wf2 event-ordering+_subtype bool_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot lt_int_wf bag-size_wf es-pred_wf assert_of_lt_int less_than_wf Id_wf atom2_subtype_base es-loc_wf es-pred-loc-base es-E_wf iff_weakening_equal not_wf true_wf or_wf exists_wf classrel_wf Memory-class_wf all_wf bag-member_wf squash_wf Accum-class_wf eclass_wf event-ordering+_wf nat_wf bag-size-bag-member Accum-classrel-Memory false_wf uiff_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].
\mforall{}[v:B].
uiff(v  \mmember{}  Memory-class(f;init;X)(e);\mdownarrow{}((\muparrow{}first(e))  \mwedge{}  v  \mdownarrow{}\mmember{}  init  loc(e))
\mvee{}  ((\mneg{}\muparrow{}first(e))
\mwedge{}  ((\mexists{}a:A
(a  \mmember{}  X(pred(e))
\mwedge{}  (\mexists{}b:B
(b  \mmember{}  Memory-class(f;init;X)(pred(e))
\mwedge{}  (v  =  (f  a  b))))))
\mvee{}  ((\mforall{}a:A.  (\mneg{}a  \mmember{}  X(pred(e))))
\mwedge{}  v  \mmember{}  Memory-class(f;init;X)(pred(e))))))

Date html generated: 2015_07_22-PM-00_11_49
Last ObjectModification: 2015_02_04-PM-04_42_27

Home Index