### Nuprl Lemma : iterated-classrel-Memory-loc-classrel

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

Proof

Definitions occuring in Statement :  Memory-loc-class: `Memory-loc-class(f;init;X)` iterated_classrel: `iterated_classrel(es;S;A;f;init;X;e;v)` classrel: `v ∈ X(e)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-loc: `loc(e)` es-E: `E` Id: `Id` 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: `bag(T)`
Lemmas :  squash_wf exists_wf bag-member_wf es-loc_wf event-ordering+_subtype or_wf classrel_wf all_wf not_wf Memory-loc-class_wf Memory-loc-classrel1 assert_wf es-first_wf2 es-pred_wf and_wf equal_wf member_wf es-pred-locl es-causl_weakening subtype_base_sq Id_wf atom2_subtype_base es-pred-loc-base es-E_wf iff_weakening_equal iterated_classrel_wf uiff_wf bool_wf eqtt_to_assert uiff_transitivity equal-wf-T-base bnot_wf eqff_to_assert assert_of_bnot

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(iterated\_classrel(es;B;A;f  loc(e);init;X;e;v);\mdownarrow{}(\mexists{}a:A
\mexists{}b:B
(a  \mmember{}  X(e)
\mwedge{}  b  \mmember{}  Memory-loc-class(f;init;X)(e)
\mwedge{}  (v  =  (f  loc(e)  a  b))))
\mvee{}  ((\mforall{}a:A.  (\mneg{}a  \mmember{}  X(e)))
\mwedge{}  v  \mmember{}  Memory-loc-class(f;init;X)(e)))

Date html generated: 2015_07_22-PM-00_12_28
Last ObjectModification: 2015_02_04-PM-04_43_11

Home Index