Nuprl Lemma : Memory-loc-class-mem

[Info,B,A:Type].
  R:A  B  B  . f:Id  A  B  B. init:Id  bag(B). X:EClass(A). es:EO+(Info). e1,e2:E. v1,v2:B. a:A.
    ((a:A. s:B. e:E.
        (e1 loc e   (e <loc e2)  a  X(e)  s  Memory-loc-class(f;init;X)(e)  R[a;s;f loc(e) a s]))
     (a1,a2:A. s1,s2:B. e,e':E.
          (e1 loc e 
           (e <loc e')
           (e' <loc e2)
           a1  X(e)
           s1  Memory-loc-class(f;init;X)(e)
           a2  X(e')
           s2  Memory-loc-class(f;init;X)(e')
           R[a1;s1;s2]
           R[a1;s1;f loc(e2) a2 s2]))
     (s1,s2:B. a:A.  SqStable(R[a;s1;s2]))
     single-valued-classrel(es;X;A)
     single-valued-bag(init loc(e1);B)
     (e1 <loc e2)
     a  X(e1)
     v1  Memory-loc-class(f;init;X)(e1)
     v2  Memory-loc-class(f;init;X)(e2)
     R[a;v1;v2])


Proof not projected



Definitions occuring in Statement :  Memory-loc-class: Memory-loc-class(f;init;X),  single-valued-classrel: single-valued-classrel(es;X;T),  classrel: v  X(e),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-le: e loc e' ,  es-locl: (e <loc e'),  es-loc: loc(e),  es-E: E,  Id: Id,  sq_stable: SqStable(P),  uall: [x:A]. B[x],  prop: ,  so_apply: x[s1;s2;s3],  all: x:A. B[x],  implies: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type,  single-valued-bag: single-valued-bag(b;T),  bag: bag(T)
Definitions :  rev_implies: P  Q,  and: P  Q,  guard: {T},  iff: P  Q,  so_lambda: x y.t[x; y],  so_lambda: x.t[x],  member: t  T,  so_apply: x[s1;s2;s3],  implies: P  Q,  prop: ,  all: x:A. B[x],  uall: [x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  uiff: uiff(P;Q),  uimplies: b supposing a,  es-locl: (e <loc e'),  subtype: S  T
Lemmas :  equal_wf,  and_wf,  iff_weakening_uiff,  implies_functionality_wrt_iff,  all_functionality_wrt_iff,  es-le-loc,  Memory-class-mem,  Memory-class_wf,  bag_wf,  Id_wf,  eclass_wf,  event-ordering+_wf,  es-le_wf,  es-E_wf,  sq_stable_wf,  all_wf,  single-valued-classrel_wf,  es-loc_wf,  single-valued-bag_wf,  event-ordering+_inc,  es-locl_wf,  Memory-loc-class_wf,  classrel_wf,  Memory-classrel-loc
\mforall{}[Info,B,A:Type].
    \mforall{}R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B.  \mforall{}init:Id  {}\mrightarrow{}  bag(B).  \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).
    \mforall{}e1,e2:E.  \mforall{}v1,v2:B.  \mforall{}a:A.
        ((\mforall{}a:A.  \mforall{}s:B.  \mforall{}e:E.
                (e1  \mleq{}loc  e 
                {}\mRightarrow{}  (e  <loc  e2)
                {}\mRightarrow{}  a  \mmember{}  X(e)
                {}\mRightarrow{}  s  \mmember{}  Memory-loc-class(f;init;X)(e)
                {}\mRightarrow{}  R[a;s;f  loc(e)  a  s]))
        {}\mRightarrow{}  (\mforall{}a1,a2:A.  \mforall{}s1,s2:B.  \mforall{}e,e':E.
                    (e1  \mleq{}loc  e 
                    {}\mRightarrow{}  (e  <loc  e')
                    {}\mRightarrow{}  (e'  <loc  e2)
                    {}\mRightarrow{}  a1  \mmember{}  X(e)
                    {}\mRightarrow{}  s1  \mmember{}  Memory-loc-class(f;init;X)(e)
                    {}\mRightarrow{}  a2  \mmember{}  X(e')
                    {}\mRightarrow{}  s2  \mmember{}  Memory-loc-class(f;init;X)(e')
                    {}\mRightarrow{}  R[a1;s1;s2]
                    {}\mRightarrow{}  R[a1;s1;f  loc(e2)  a2  s2]))
        {}\mRightarrow{}  (\mforall{}s1,s2:B.  \mforall{}a:A.    SqStable(R[a;s1;s2]))
        {}\mRightarrow{}  single-valued-classrel(es;X;A)
        {}\mRightarrow{}  single-valued-bag(init  loc(e1);B)
        {}\mRightarrow{}  (e1  <loc  e2)
        {}\mRightarrow{}  a  \mmember{}  X(e1)
        {}\mRightarrow{}  v1  \mmember{}  Memory-loc-class(f;init;X)(e1)
        {}\mRightarrow{}  v2  \mmember{}  Memory-loc-class(f;init;X)(e2)
        {}\mRightarrow{}  R[a;v1;v2])


Date html generated: 2012_02_20-PM-02_55_40
Last ObjectModification: 2012_01_24-AM-10_30_22

Home Index