Nuprl Lemma : SM2-class_wf2

[A,B,C:']. [init:Id  bag(C)]. [tr1:Id  A  C  C]. [X1:EClass'(A)]. [tr2:Id  B  C  C].
[X2:EClass'(B)].
  (SM2-class(init;<tr1, X1>;<tr2, X2>)  EClass'(C))


Proof not projected



Definitions occuring in Statement :  SM2-class: SM2-class(init;trX1;trX2),  Message: Message,  eclass: EClass(A[eo; e]),  Id: Id,  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  pair: <a, b>,  universe: Type,  bag: bag(T)
Definitions :  uall: [x:A]. B[x],  member: t  T,  label: ...$L... t
Lemmas :  SM2-class_wf,  eclass_wf2,  Id_wf,  bag_wf
\mforall{}[A,B,C:\mBbbU{}'].  \mforall{}[init:Id  {}\mrightarrow{}  bag(C)].  \mforall{}[tr1:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  C  {}\mrightarrow{}  C].  \mforall{}[X1:EClass'(A)].  \mforall{}[tr2:Id
                                                                                                                                                                          {}\mrightarrow{}  B
                                                                                                                                                                          {}\mrightarrow{}  C
                                                                                                                                                                          {}\mrightarrow{}  C].
\mforall{}[X2:EClass'(B)].
    (SM2-class(init;<tr1,  X1><tr2,  X2>)  \mmember{}  EClass'(C))


Date html generated: 2011_10_20-PM-03_36_49
Last ObjectModification: 2011_08_22-PM-02_03_44

Home Index