Nuprl Lemma : seg_sum_wf
[p,q:
]. [L: List]. (seg_sum(p;q;L) 
)
Proof
Definitions occuring in Statement :
seg_sum: seg_sum(p;q;L),
list: T List,
uall: [x:A]. B[x],
member: t T,
int:
Definitions :
uall: [x:A]. B[x],
member: t T,
seg_sum: seg_sum(p;q;L)
Lemmas :
l_sum_wf,
segment_wf,
list_wf
\mforall{}[p,q:\mBbbZ{}]. \mforall{}[L:\mBbbZ{} List]. (seg\_sum(p;q;L) \mmember{} \mBbbZ{})
Date html generated:
2014_03_27-PM-01_47_10
Last ObjectModification:
2013_10_24-PM-00_27_49
Home
Index