Nuprl Lemma : SM1-class_wf
[A,B:
']. [init:Id 
bag(B)]. [trX:Id A B B 
EClass'(A)]. (SM1-class(init;trX) 
EClass'(B))
Proof not projected
Definitions occuring in Statement :
SM1-class: SM1-class(init;trX),
Message: Message,
eclass: EClass(A[eo; e]),
Id: Id,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
universe: Type,
bag: bag(T)
Definitions :
member: t T,
nat_plus: 
,
int_seg: {i..j
},
lelt: i 
j < k,
and: P 
Q,
le: A B,
not: 
A,
implies: P 
Q,
false: False,
label: ...$L... t,
uall: [x:A]. B[x],
SM1-class: SM1-class(init;trX),
prop: 
Lemmas :
SM-gen-class_wf,
Message_wf,
le_wf,
int_seg_wf,
Id_wf,
eclass_wf2,
bag_wf
\mforall{}[A,B:\mBbbU{}']. \mforall{}[init:Id {}\mrightarrow{} bag(B)]. \mforall{}[trX:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B \mtimes{} EClass'(A)].
(SM1-class(init;trX) \mmember{} EClass'(B))
Date html generated:
2011_10_20-PM-03_36_13
Last ObjectModification:
2011_08_17-AM-00_53_02
Home
Index