Nuprl Lemma : SM4-class_wf2
[A,B,C,D,E:
']. [init:Id 
bag(E)]. [tr1:Id A E E]. [X1:EClass'(A)]. [tr2:Id B E E].
[X2:EClass'(B)]. [tr3:Id C E E]. [X3:EClass'(C)]. [tr4:Id D E E]. [X4:EClass'(D)].
(SM4-class(init;<tr1, X1>;<tr2, X2>;<tr3, X3>;<tr4, X4>) 
EClass'(E))
Proof not projected
Definitions occuring in Statement :
SM4-class: SM4-class(init;trX1;trX2;trX3;trX4),
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 :
label: ...$L... t,
member: t T,
uall: [x:A]. B[x]
Lemmas :
bag_wf,
Id_wf,
eclass_wf2,
SM4-class_wf
\mforall{}[A,B,C,D,E:\mBbbU{}']. \mforall{}[init:Id {}\mrightarrow{} bag(E)]. \mforall{}[tr1:Id {}\mrightarrow{} A {}\mrightarrow{} E {}\mrightarrow{} E]. \mforall{}[X1:EClass'(A)]. \mforall{}[tr2:Id
{}\mrightarrow{} B
{}\mrightarrow{} E
{}\mrightarrow{} E].
\mforall{}[X2:EClass'(B)]. \mforall{}[tr3:Id {}\mrightarrow{} C {}\mrightarrow{} E {}\mrightarrow{} E]. \mforall{}[X3:EClass'(C)]. \mforall{}[tr4:Id {}\mrightarrow{} D {}\mrightarrow{} E {}\mrightarrow{} E].
\mforall{}[X4:EClass'(D)].
(SM4-class(init;<tr1, X1><tr2, X2><tr3, X3><tr4, X4>) \mmember{} EClass'(E))
Date html generated:
2011_10_20-PM-03_37_45
Last ObjectModification:
2011_09_12-AM-10_38_53
Home
Index