Nuprl Lemma : Memory3-locally-programmable

A1,A2,A3,B:{T:'| valueall-type(T)} . init:Id  bag(B). tr1:Id  A1  B  B.
  [X1:EClass'(A1)]
    tr2:Id  A2  B  B
      [X2:EClass'(A2)]
        tr3:Id  A3  B  B
          [X3:EClass'(A3)]
            (NormalLProgrammable'(A1;X1)
             NormalLProgrammable'(A2;X2)
             NormalLProgrammable'(A3;X3)
             NormalLProgrammable'(B;Memory3(init;tr1;X1;tr2;X2;tr3;X3)))


Proof not projected



Definitions occuring in Statement :  Memory3: Memory3(init;tr1;X1;tr2;X2;tr3;X3),  Message: Message,  normal-locally-programmable: NormalLProgrammable(A;X),  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  function: x:A  B[x],  universe: Type,  bag: bag(T),  valueall-type: valueall-type(T)
Definitions :  all: x:A. B[x],  uall: [x:A]. B[x],  eclass: EClass(A[eo; e]),  implies: P  Q,  Memory3: Memory3(init;tr1;X1;tr2;X2;tr3;X3),  Memory-loc-class: Memory-loc-class(f;init;X),  Accum-loc-class: Accum-loc-class(f;init;X),  member: t  T,  lifting-loc-2: lifting-loc-2(f),  empty-bag: {},  lifting-gen-list-rev: lifting-gen-list-rev(n;bags),  select: l[i],  lifting2-loc: lifting2-loc(f;loc;abag;bbag),  lifting-loc-gen-rev: lifting-loc-gen-rev(n;bags;loc;f),  lifting-gen-rev: lifting-gen-rev(n;f;bags),  ifthenelse: if b then t else f fi ,  eq_int: (i = j),  bag-combine: xbs.f[x],  ycomb: Y,  map: map(f;as),  bfalse: ff,  bag-union: bag-union(bbs),  concat: concat(ll),  reduce: reduce(f;k;as),  bag-map: bag-map(f;bs),  le_int: i z j,  bnot: b,  lt_int: i <z j,  btrue: tt,  squash: T,  true: True,  uimplies: b supposing a,  sq_stable: SqStable(P),  prop: ,  subtype: S  T
Lemmas :  primed-class-opt-nlp,  Accum-loc-class_wf,  Message_wf,  disjoint-union-tr_wf,  disjoint-union-comb_wf,  rec-combined-loc-class-opt-1-nlp,  lifting-loc-2_wf,  empty-bag_wf,  bag_wf,  Id_wf,  disjoint-union-comb-nlp,  union-valueall-type,  sq_stable__valueall-type,  valueall-type_wf,  normal-locally-programmable_wf,  event-ordering+_wf,  es-E_wf,  event-ordering+_inc
\mforall{}A1,A2,A3,B:\{T:\mBbbU{}'|  valueall-type(T)\}  .  \mforall{}init:Id  {}\mrightarrow{}  bag(B).  \mforall{}tr1:Id  {}\mrightarrow{}  A1  {}\mrightarrow{}  B  {}\mrightarrow{}  B.
    \mforall{}[X1:EClass'(A1)]
        \mforall{}tr2:Id  {}\mrightarrow{}  A2  {}\mrightarrow{}  B  {}\mrightarrow{}  B
            \mforall{}[X2:EClass'(A2)]
                \mforall{}tr3:Id  {}\mrightarrow{}  A3  {}\mrightarrow{}  B  {}\mrightarrow{}  B
                    \mforall{}[X3:EClass'(A3)]
                        (NormalLProgrammable'(A1;X1)
                        {}\mRightarrow{}  NormalLProgrammable'(A2;X2)
                        {}\mRightarrow{}  NormalLProgrammable'(A3;X3)
                        {}\mRightarrow{}  NormalLProgrammable'(B;Memory3(init;tr1;X1;tr2;X2;tr3;X3)))


Date html generated: 2012_01_23-PM-01_30_06
Last ObjectModification: 2012_01_12-AM-11_02_07

Home Index