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)
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  member: t ∈ T,  subtype_rel: A ⊆r B,  so_lambda: λ2x.t[x],  prop: ℙ,  and: P ∧ Q,  so_apply: x[s],  implies: P ⇒ Q,  sq_stable: SqStable(P),  strongwellfounded: SWellFounded(R[x; y]),  exists: ∃x:A. B[x],  guard: {T},  int_seg: {i..j-},  lelt: i ≤ j < k,  uimplies: b supposing a,  satisfiable_int_formula: satisfiable_int_formula(fmla),  false: False,  not: ¬A,  top: Top,  decidable: Dec(P),  or: P ∨ Q,  le: A ≤ B,  less_than': less_than'(a;b),  nat: ℕ,  ge: i ≥ j ,  less_than: a < b,  squash: ↓T,  iterated_classrel: iterated_classrel(es;S;A;f;init;X;e;v),  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  ifthenelse: if b then t else f fi ,  bfalse: ff,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  cand: A c∧ B,  rev_uimplies: rev_uimplies(P;Q),  Id: Id,  es-E: E,  es-base-E: es-base-E(es),  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  sq_type: SQType(T),  assert: ↑b
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: 2016_05_17-AM-09_22_42
Last ObjectModification: 2016_01_17-PM-11_15_36

Theory : classrel!lemmas


Home Index