Nuprl Lemma : SM-gen-classrel-step

[es:EO']. [e:E]. [S:']. [n:]. [m:{1..n + 1}]. [A:{m..n + 1}  ']. [init:Id  bag(S)].
[trXs:k:{m..n + 1}  (Id  A k  S  S  EClass'(A k))]. [s:S].
  uiff(s  SM-gen-class(init;n;m;trXs)(e);p:{m..n + 1}
                                            v:A p
                                             s':S
                                              (v  snd((trXs p))(e)
                                               s'  Prior(SM-gen-class(init;n;m;trXs))?init(e)
                                               (s = ((fst((trXs p))) loc(e) v s'))
                                               (i:{m..p}. x:A i.  (x  snd((trXs i))(e)))))


Proof not projected



Definitions occuring in Statement :  SM-gen-class: SM-gen-class(init;n;m;trXs),  Message: Message,  primed-class-opt: Prior(X)?b,  classrel: v  X(e),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-loc: loc(e),  es-E: E,  Id: Id,  int_seg: {i..j},  nat_plus: ,  uiff: uiff(P;Q),  uall: [x:A]. B[x],  pi1: fst(t),  pi2: snd(t),  all: x:A. B[x],  exists: x:A. B[x],  not: A,  squash: T,  and: P  Q,  apply: f a,  function: x:A  B[x],  product: x:A  B[x],  add: n + m,  natural_number: $n,  universe: Type,  equal: s = t,  bag: bag(T)
Definitions :  uiff: uiff(P;Q),  classrel: v  X(e),  squash: T,  and: P  Q,  uimplies: b supposing a,  member: t  T,  true: True,  bag-member: x  bs,  label: ...$L... t,  int_seg: {i..j},  all: x:A. B[x],  so_lambda: x.t[x],  top: Top,  subtype: S  T,  lelt: i  j < k,  eclass: EClass(A[eo; e]),  exists: x:A. B[x],  not: A,  implies: P  Q,  iff: P  Q,  prop: ,  rev_implies: P  Q,  false: False,  SM-gen-class: SM-gen-class(init;n;m;trXs),  pi1: fst(t),  rec-comb: rec-comb(X;f;init),  ycomb: Y,  or: P  Q,  pi2: snd(t),  nat_plus: ,  uall: [x:A]. B[x],  so_apply: x[s],  le: A  B,  rev_uimplies: rev_uimplies(P;Q)
Lemmas :  classrel_wf,  SM-gen-class_wf,  Message_wf,  int_seg_wf,  Id_wf,  eclass_wf2,  bag_wf,  nat_plus_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  squash_wf,  exists_wf,  and_wf,  pi2_wf,  primed-class-opt_wf,  equal_wf,  pi1_wf_top,  es-loc_wf,  all_wf,  lelt_wf,  not_wf,  SM-gen-tr-exists2,  subtype_rel_simple_product,  top_wf,  subtype_rel_self,  bag-member_wf,  true_wf,  bag-member-lifting-loc-2,  bag-member-not-bag-null,  SM-gen-tr-if,  assert-bag-null,  empty-bag-iff-no-member,  assert_of_bor,  bnot_wf,  bag-null_wf,  eq_int_wf,  assert_of_bnot,  assert_wf
\mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[S:\mBbbU{}'].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[m:\{1..n  +  1\msupminus{}\}].  \mforall{}[A:\{m..n  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[init:Id  {}\mrightarrow{}  bag(S)].
\mforall{}[trXs:k:\{m..n  +  1\msupminus{}\}  {}\mrightarrow{}  (Id  {}\mrightarrow{}  A  k  {}\mrightarrow{}  S  {}\mrightarrow{}  S  \mtimes{}  EClass'(A  k))].  \mforall{}[s:S].
    uiff(s  \mmember{}  SM-gen-class(init;n;m;trXs)(e);\mdownarrow{}\mexists{}p:\{m..n  +  1\msupminus{}\}
                                                                                        \mexists{}v:A  p
                                                                                          \mexists{}s':S
                                                                                            (v  \mmember{}  snd((trXs  p))(e)
                                                                                            \mwedge{}  s'  \mmember{}  Prior(SM-gen-class(init;n;m;trXs))?init(e)
                                                                                            \mwedge{}  (s  =  ((fst((trXs  p)))  loc(e)  v  s'))
                                                                                            \mwedge{}  (\mforall{}i:\{m..p\msupminus{}\}.  \mforall{}x:A  i.    (\mneg{}x  \mmember{}  snd((trXs  i))(e)))))


Date html generated: 2012_01_23-PM-01_21_44
Last ObjectModification: 2011_12_30-PM-09_30_16

Home Index