Nuprl Lemma : SM3-class_wf2
[A,B,C,D:
']. [init:Id 
bag(D)]. [tr1:Id A D D]. [X1:EClass'(A)]. [tr2:Id B D D].
[X2:EClass'(B)]. [tr3:Id C D D]. [X3:EClass'(C)].
(SM3-class(init;<tr1, X1>;<tr2, X2>;<tr3, X3>) 
EClass'(D))
Proof not projected
Definitions occuring in Statement :
SM3-class: SM3-class(init;trX1;trX2;trX3),
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 :
SM3-class_wf,
eclass_wf2,
Id_wf,
bag_wf
\mforall{}[A,B,C,D:\mBbbU{}']. \mforall{}[init:Id {}\mrightarrow{} bag(D)]. \mforall{}[tr1:Id {}\mrightarrow{} A {}\mrightarrow{} D {}\mrightarrow{} D]. \mforall{}[X1:EClass'(A)]. \mforall{}[tr2:Id
{}\mrightarrow{} B
{}\mrightarrow{} D
{}\mrightarrow{} D].
\mforall{}[X2:EClass'(B)]. \mforall{}[tr3:Id {}\mrightarrow{} C {}\mrightarrow{} D {}\mrightarrow{} D]. \mforall{}[X3:EClass'(C)].
(SM3-class(init;<tr1, X1><tr2, X2><tr3, X3>) \mmember{} EClass'(D))
Date html generated:
2011_10_20-PM-03_37_17
Last ObjectModification:
2011_08_22-PM-02_06_06
Home
Index