Nuprl Lemma : initseg_sum_wf
[r:
]. [L: List]. (initseg_sum(r;L) 
)
Proof
Definitions occuring in Statement :
initseg_sum: initseg_sum(r;L),
list: T List,
uall: [x:A]. B[x],
member: t T,
int:
Definitions :
uall: [x:A]. B[x],
member: t T,
initseg_sum: initseg_sum(r;L)
Lemmas :
l_sum_wf,
firstn_wf,
list_wf
\mforall{}[r:\mBbbZ{}]. \mforall{}[L:\mBbbZ{} List]. (initseg\_sum(r;L) \mmember{} \mBbbZ{})
Date html generated:
2014_03_27-PM-01_47_11
Last ObjectModification:
2013_10_24-PM-00_11_11
Home
Index