Nuprl Lemma : Accum-loc-classrel

[B,A:']. [f:Id  A  B  B]. [init:Id  bag(B)]. [X:EClass'(A)]. [es:EO']. [e:E]. [v:B].
  uiff(v  Accum-loc-class(f;init;X)(e);L:(A  E) List
                                          (prior-classrel-list(es;A;X;L;e)
                                           (a:A
                                              (a  X(e)
                                               (x:B
                                                  (bag-member(B;x;init loc(e))
                                                   (v
                                                    = (f loc(e) a 
                                                       list_accum(b,a.f loc(e) a b;x;map(p.(fst(p));L))))))))))


Proof not projected



Definitions occuring in Statement :  prior-classrel-list: prior-classrel-list(es;A;X;L;e),  Accum-loc-class: Accum-loc-class(f;init;X),  Message: Message,  classrel: v  X(e),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-loc: loc(e),  es-E: E,  Id: Id,  map: map(f;as),  uiff: uiff(P;Q),  uall: [x:A]. B[x],  pi1: fst(t),  exists: x:A. B[x],  squash: T,  and: P  Q,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  product: x:A  B[x],  list: type List,  universe: Type,  equal: s = t,  list_accum: list_accum(x,a.f[x; a];y;l),  bag-member: bag-member(T;x;bs),  bag: bag(T)
Definitions :  eclass: EClass(A[eo; e]),  exists: x:A. B[x],  and: P  Q,  member: t  T,  prop: ,  all: x:A. B[x],  cand: A c B,  top: Top,  so_lambda: x y.t[x; y],  uiff: uiff(P;Q),  classrel: v  X(e),  squash: T,  bag-member: bag-member(T;x;bs),  uimplies: b supposing a,  true: True,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  rev_uimplies: rev_uimplies(P;Q),  subtype: S  T
Lemmas :  classrel_wf,  Message_wf,  Accum-loc-class_wf,  squash_wf,  es-E_wf,  event-ordering+_inc,  prior-classrel-list_wf,  bag-member_wf,  es-loc_wf,  Id_wf,  map_wf,  pi1_wf_top,  list_accum_wf,  event-ordering+_wf,  bag_wf,  Accum-classrel,  Accum-loc-Accum-classrel
\mforall{}[B,A:\mBbbU{}'].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass'(A)].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[v:B].
    uiff(v  \mmember{}  Accum-loc-class(f;init;X)(e);\mdownarrow{}\mexists{}L:(A  \mtimes{}  E)  List
                                                                                    (prior-classrel-list(es;A;X;L;e)
                                                                                    \mwedge{}  (\mexists{}a:A
                                                                                            (a  \mmember{}  X(e)
                                                                                            \mwedge{}  (\mexists{}x:B
                                                                                                    (bag-member(B;x;init  loc(e))
                                                                                                    \mwedge{}  (v
                                                                                                        =  (f  loc(e)  a 
                                                                                                              list\_accum(b,a.f  loc(e)  a  b;
                                                                                                                                    x;
                                                                                                                                    map(\mlambda{}p.(fst(p));L))))))))))


Date html generated: 2011_10_20-PM-03_47_02
Last ObjectModification: 2011_09_23-PM-08_44_29

Home Index