Nuprl Lemma : SM1-class-gen-classrel

[es:EO']. [e:E]. [S,A:']. [init:Id  bag(S)]. [tr:Id  A  S  S]. [X:EClass'(A)]. [s:S].
  uiff(s  SM1-class(init;<tr, X>)(e);L:({1..2}  A  E) List
                                        (classrel-multi-list(es;n.A;n.X;L;e;1;2)
                                         (null(L))
                                         (e = (snd(snd(last(L)))))
                                         (x:S
                                            (bag-member(S;x;init loc(e))
                                             (s = list_accum(a,b.tr loc(snd(snd(b))) (fst(snd(b))) a;x;L))))))


Proof not projected



Definitions occuring in Statement :  SM1-class: SM1-class(init;trX),  classrel-multi-list: classrel-multi-list(es;A;Xs;L;e;n1;n2),  Message: Message,  classrel: v  X(e),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-loc: loc(e),  es-E: E,  Id: Id,  null: null(as),  assert: b,  int_seg: {i..j},  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],  pair: <a, b>,  product: x:A  B[x],  list: type List,  natural_number: $n,  universe: Type,  equal: s = t,  list_accum: list_accum(x,a.f[x; a];y;l),  last: last(L),  bag-member: bag-member(T;x;bs),  bag: bag(T)
Definitions :  eclass: EClass(A[eo; e]),  exists: x:A. B[x],  int_seg: {i..j},  and: P  Q,  not: A,  nat_plus: ,  member: t  T,  lelt: i  j < k,  le: A  B,  implies: P  Q,  false: False,  prop: ,  all: x:A. B[x],  subtype: S  T,  cand: A c B,  ge: i  j ,  top: Top,  so_lambda: x.t[x],  so_lambda: x y.t[x; y],  pi2: snd(t),  pi1: fst(t),  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s],  so_apply: x[s1;s2],  SM1-class: SM1-class(init;trX)
Lemmas :  SM-gen-class-classrel,  le_wf,  int_seg_wf,  classrel_wf,  Message_wf,  SM1-class_wf2,  squash_wf,  es-E_wf,  event-ordering+_inc,  classrel-multi-list_wf,  ge_wf,  not_wf,  assert_wf,  null_wf3,  top_wf,  pi2_wf,  last_wf,  bag-member_wf,  es-loc_wf,  list_accum_wf,  pi1_wf_top,  event-ordering+_wf,  bag_wf,  Id_wf
\mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[S,A:\mBbbU{}'].  \mforall{}[init:Id  {}\mrightarrow{}  bag(S)].  \mforall{}[tr:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[X:EClass'(A)].
\mforall{}[s:S].
    uiff(s  \mmember{}  SM1-class(init;<tr,  X>)(e);\mdownarrow{}\mexists{}L:(\{1..2\msupminus{}\}  \mtimes{}  A  \mtimes{}  E)  List
                                                                                (classrel-multi-list(es;\mlambda{}n.A;\mlambda{}n.X;L;e;1;2)
                                                                                \mwedge{}  (\mneg{}\muparrow{}null(L))
                                                                                \mwedge{}  (e  =  (snd(snd(last(L)))))
                                                                                \mwedge{}  (\mexists{}x:S
                                                                                        (bag-member(S;x;init  loc(e))
                                                                                        \mwedge{}  (s
                                                                                            =  list\_accum(a,b.tr  loc(snd(snd(b)))  (fst(snd(b)))  a;
                                                                                                                      x;
                                                                                                                      L))))))


Date html generated: 2011_10_20-PM-03_48_00
Last ObjectModification: 2011_09_22-PM-12_43_05

Home Index