### Nuprl Lemma : Memory-loc-classrel1

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

Proof

Definitions occuring in Statement :  Memory-loc-class: `Memory-loc-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 :  classrel_wf Memory-loc-class_wf squash_wf or_wf assert_wf es-first_wf2 event-ordering+_subtype bag-member_wf es-loc_wf not_wf exists_wf es-pred_wf all_wf es-E_wf event-ordering+_wf eclass_wf Id_wf bag_wf 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 assert_of_lt_int less_than_wf atom2_subtype_base es-pred-loc-base iff_weakening_equal true_wf Accum-loc-class_wf nat_wf bag-size-bag-member Accum-loc-classrel-Memory false_wf uiff_wf

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  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-loc-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-loc-class(f;init;X)(pred(e))
\mwedge{}  (v  =  (f  loc(e)  a  b))))))
\mvee{}  ((\mforall{}a:A.  (\mneg{}a  \mmember{}  X(pred(e))))
\mwedge{}  v  \mmember{}  Memory-loc-class(f;init;X)(pred(e))))))

Date html generated: 2015_07_22-PM-00_12_02
Last ObjectModification: 2015_02_04-PM-04_43_04

Home Index