Nuprl Lemma : Memory-classrel

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


Proof




Definitions occuring in Statement :  Memory-class: Memory-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-first: first(e) es-pred: pred(e) es-loc: loc(e) es-E: E Id: Id assert: b uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A or: P ∨ Q and: P ∧ Q apply: a function: x:A ─→ B[x] universe: Type bag-member: x ↓∈ bs bag: bag(T)
Lemmas :  sq_stable__iff classrel_wf Memory-class_wf or_wf assert_wf es-first_wf2 bag-member_wf es-loc_wf not_wf iterated_classrel_wf es-pred_wf sq_stable__classrel bool_wf eqtt_to_assert sq_stable__bag-member true_wf squash_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot false_wf sq_stable__iterated_classrel es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf Id_wf bag_wf Memory-classrel1 iff_wf exists_wf all_wf iterated-classrel-Memory-classrel

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]
            (v  \mmember{}  Memory-class(f;init;X)(e)
            \mLeftarrow{}{}\mRightarrow{}  ((\muparrow{}first(e))  \mwedge{}  v  \mdownarrow{}\mmember{}  init  loc(e))
                    \mvee{}  ((\mneg{}\muparrow{}first(e))  \mwedge{}  iterated\_classrel(es;B;A;f;init;X;pred(e);v)))



Date html generated: 2015_07_22-PM-00_12_33
Last ObjectModification: 2015_01_28-AM-11_42_40

Home Index