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(v  X*(f loc(e),init,e);(a:A. b:B. (a  X(e)  b  Memory-loc-class(f;init;X)(e)  (v = (f loc(e) a b))))
                                     ((a:A. (a  X(e)))  v  Memory-loc-class(f;init;X)(e)))


Proof not projected



Definitions occuring in Statement :  Memory-loc-class: Memory-loc-class(f;init;X),  iterated_classrel: v  X*(f,init,e),  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,  bag: bag(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  iterated_classrel: v  X*(f,init,e),  squash: T,  or: P  Q,  and: P  Q,  not: A,  prop: ,  implies: P  Q,  member: t  T,  so_lambda: x.t[x],  cand: A c B,  true: True,  nat: ,  ge: i  j ,  le: A  B,  false: False,  ycomb: Y,  ifthenelse: if b then t else f fi ,  btrue: tt,  bfalse: ff,  so_lambda: x y.t[x; y],  uiff: uiff(P;Q),  exists: x:A. B[x],  uimplies: b supposing a,  guard: {T},  assert: b,  Id: Id,  rev_implies: P  Q,  iff: P  Q,  sq_stable: SqStable(P),  so_apply: x[s],  strongwellfounded: SWellFounded(R[x; y]),  bool: ,  unit: Unit,  so_apply: x[s1;s2],  rev_uimplies: rev_uimplies(P;Q),  sq_type: SQType(T),  subtype: S  T,  it:
Lemmas :  sq_stable__uiff,  iterated_classrel_wf,  es-loc_wf,  event-ordering+_inc,  squash_wf,  or_wf,  exists_wf,  classrel_wf,  Memory-loc-class_wf,  all_wf,  not_wf,  sq_stable__iterated_classrel,  sq_stable__squash,  es-causl-swellfnd,  nat_properties,  ge_wf,  less_than_wf,  nat_wf,  le_wf,  es-causl_wf,  es-first_wf,  bool_wf,  eqtt_to_assert,  uiff_transitivity,  equal_wf,  assert_wf,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  es-E_wf,  event-ordering+_wf,  eclass_wf,  Id_wf,  bag_wf,  bag-member_wf,  and_wf,  Memory-loc-classrel1,  true_wf,  es-pred_wf,  member_wf,  es-pred-causl,  subtype_base_sq,  atom2_subtype_base,  es-loc-pred,  uiff_functionality_wrt_uiff2,  iff_weakening_uiff,  squash_functionality_wrt_uiff,  exists_functionality_wrt_iff,  and_functionality_wrt_uiff2,  false_wf
\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{}  X*(f  loc(e),init,e);\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: 2012_01_23-PM-12_59_10
Last ObjectModification: 2012_01_11-PM-12_11_34

Home Index