Nuprl Lemma : SM1-class-classrel

[es:EO']. [e:E]. [A,B:']. [init:Id  bag(B)]. [trX:Id  A  B  B  EClass'(A)]. [v:B].
  uiff(v  SM1-class(init;trX)(e);L:(A  E) List
                                    (classrel-list(es;A;snd(trX);L;e)
                                     (null(L))
                                     (e = last(map(p.(snd(p));L)))
                                     (x:B
                                        (x  init loc(e)  (v = list_accum(b,a.(fst(trX)) loc(e) (fst(a)) b;x;L))))))


Proof not projected



Definitions occuring in Statement :  classrel-list: classrel-list(es;A;X;L;e),  SM1-class: SM1-class(init;trX),  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),  null: null(as),  assert: b,  uiff: uiff(P;Q),  uall: [x:A]. B[x],  pi1: fst(t),  pi2: snd(t),  exists: x:A. B[x],  not: A,  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),  last: last(L),  bag-member: x  bs,  bag: bag(T)
Definitions :  so_lambda: x y.t[x; y],  top: Top,  cand: A c B,  so_lambda: x.t[x],  prop: ,  true: True,  uimplies: b supposing a,  subtype: S  T,  all: x:A. B[x],  member: t  T,  pi1: fst(t),  bag-member: x  bs,  pi2: snd(t),  and: P  Q,  exists: x:A. B[x],  squash: T,  classrel: v  X(e),  uiff: uiff(P;Q),  eclass: EClass(A[eo; e]),  compose: f o g,  false: False,  implies: P  Q,  le: A  B,  lelt: i  j < k,  int_seg: {i..j},  nat_plus: ,  not: A,  label: ...$L... t,  rev_implies: P  Q,  iff: P  Q,  classrel-list: classrel-list(es;A;X;L;e),  l_all: (xL.P[x]),  sorted-by: sorted-by(R;L),  or: P  Q,  ycomb: Y,  map: map(f;as),  list_accum: list_accum(x,a.f[x; a];y;l),  Id: Id,  ge: i  j ,  SM1-class: SM1-class(init;trX),  classrel-multi-list: classrel-multi-list(es;A;Xs;L;e;n1;n2),  last: last(L),  so_apply: x[s],  so_apply: x[s1;s2],  uall: [x:A]. B[x],  guard: {T},  sq_type: SQType(T),  nat: ,  l_member: (x  l),  es-locl: (e <loc e')
Lemmas :  bag_wf,  event-ordering+_wf,  Id_wf,  pi1_wf_top,  es-loc_wf,  bag-member_wf,  null-map,  pi2_wf,  map_wf,  last_wf,  top_wf,  null_wf3,  assert_wf,  not_wf,  classrel-list_wf,  exists_wf,  squash_wf,  SM1-class_wf,  Message_wf,  classrel_wf,  event-ordering+_inc,  es-E_wf,  list_accum_wf,  map-map,  int_seg_wf,  lelt_wf,  SM-gen-class-classrel,  l_member_wf,  eclass_wf2,  es-le_wf,  and_wf,  pair-eta,  int_subtype_base,  subtype_base_sq,  member_map,  select-map,  length_wf,  length-map,  all_wf,  last-map,  equal_wf,  atom2_subtype_base,  l_all-cons,  l_all_wf2,  ge_wf,  classrel-multi-list_wf,  select_member,  select_wf
\mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[A,B:\mBbbU{}'].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[trX:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B  \mtimes{}  EClass'(A)].  \mforall{}[v:B].
    uiff(v  \mmember{}  SM1-class(init;trX)(e);\mdownarrow{}\mexists{}L:(A  \mtimes{}  E)  List
                                                                        (classrel-list(es;A;snd(trX);L;e)
                                                                        \mwedge{}  (\mneg{}\muparrow{}null(L))
                                                                        \mwedge{}  (e  =  last(map(\mlambda{}p.(snd(p));L)))
                                                                        \mwedge{}  (\mexists{}x:B
                                                                                (x  \mdownarrow{}\mmember{}  init  loc(e)
                                                                                \mwedge{}  (v  =  list\_accum(b,a.(fst(trX))  loc(e)  (fst(a))  b;x;L))))))


Date html generated: 2012_01_23-PM-01_23_04
Last ObjectModification: 2011_12_13-PM-05_07_15

Home Index