Nuprl Lemma : rec-comb-classrel

[Info,B:Type]. [n:]. [A:n  Type]. [Xs:k:n  EClass(A k)]. [f:Id  k:n  (A k)  B  B]. [F:Id
                                                                                                             k:n
                                                                                                                bag(A 
                                                                                                                      k)
                                                                                                             bag(B)
                                                                                                             bag(B)].
[init:Id  bag(B)]. [es:EO+(Info)]. [e:E]. [v:B].
  uiff(v  rec-comb(Xs;F;init)(e);vs:k:n  (A k)
                                    w:B
                                     ((k:n. vs[k]  Xs[k](e))
                                      w  Prior(rec-comb(Xs;F;init))?init(e)
                                      (v = (f loc(e) vs w)))) 
  supposing x:Id. v:B. bs:k:n  bag(A k). b:bag(B).
              (bag-member(B;v;F x bs b)
               vs:k:n  (A k). w:B. ((k:n. bag-member(A k;vs k;bs k))  bag-member(B;w;b)  (v = (f x vs w))))


Proof not projected



Definitions occuring in Statement :  rec-comb: rec-comb(X;f;init),  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: ,  uiff: uiff(P;Q),  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  squash: T,  and: P  Q,  apply: f a,  function: x:A  B[x],  natural_number: $n,  universe: Type,  equal: s = t,  bag-member: bag-member(T;x;bs),  bag: bag(T)
Definitions :  nat: ,  all: x:A. B[x],  bag-member: bag-member(T;x;bs),  squash: T,  exists: x:A. B[x],  and: P  Q,  uiff: uiff(P;Q),  classrel: v  X(e),  so_apply: x[s],  uimplies: b supposing a,  member: t  T,  true: True,  prop: ,  le: A  B,  not: A,  implies: P  Q,  false: False,  cand: A c B,  so_lambda: x y.t[x; y],  rec-comb: rec-comb(X;f;init),  ycomb: Y,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  iff: P  Q,  sq_stable: SqStable(P),  rev_implies: P  Q,  subtype: S  T,  eclass: EClass(A[eo; e])
Lemmas :  classrel_wf,  rec-comb_wf2,  le_wf,  squash_wf,  int_seg_wf,  primed-class-opt_wf,  es-loc_wf,  event-ordering+_inc,  nat_properties,  Id_wf,  bag_wf,  iff_wf,  bag-member_wf,  es-E_wf,  event-ordering+_wf,  eclass_wf,  nat_wf,  sq_stable__classrel
\mforall{}[Info,B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[Xs:k:\mBbbN{}n  {}\mrightarrow{}  EClass(A  k)].  \mforall{}[f:Id
                                                                                                                                                {}\mrightarrow{}  k:\mBbbN{}n  {}\mrightarrow{}  (A  k)
                                                                                                                                                {}\mrightarrow{}  B
                                                                                                                                                {}\mrightarrow{}  B].  \mforall{}[F:Id
                                                                                                                                                                      {}\mrightarrow{}  k:\mBbbN{}n  {}\mrightarrow{}  bag(A 
                                                                                                                                                                                                    k)
                                                                                                                                                                      {}\mrightarrow{}  bag(B)
                                                                                                                                                                      {}\mrightarrow{}  bag(B)].
\mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:B].
    uiff(v  \mmember{}  rec-comb(Xs;F;init)(e);\mdownarrow{}\mexists{}vs:k:\mBbbN{}n  {}\mrightarrow{}  (A  k)
                                                                        \mexists{}w:B
                                                                          ((\mforall{}k:\mBbbN{}n.  vs[k]  \mmember{}  Xs[k](e))
                                                                          \mwedge{}  w  \mmember{}  Prior(rec-comb(Xs;F;init))?init(e)
                                                                          \mwedge{}  (v  =  (f  loc(e)  vs  w)))) 
    supposing  \mforall{}x:Id.  \mforall{}v:B.  \mforall{}bs:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k).  \mforall{}b:bag(B).
                            (bag-member(B;v;F  x  bs  b)
                            \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}vs:k:\mBbbN{}n  {}\mrightarrow{}  (A  k)
                                        \mexists{}w:B
                                          ((\mforall{}k:\mBbbN{}n.  bag-member(A  k;vs  k;bs  k))  \mwedge{}  bag-member(B;w;b)  \mwedge{}  (v  =  (f  x  vs  w))))


Date html generated: 2011_10_20-PM-03_43_38
Last ObjectModification: 2011_09_30-PM-02_41_08

Home Index