Nuprl Lemma : max_initseg_sum_wf
[i:
]. [L: List]. (max_initseg_sum(i;L) 
)
Proof
Definitions occuring in Statement :
max_initseg_sum: max_initseg_sum(i;L),
list: T List,
uall: [x:A]. B[x],
prop: ,
member: t T,
int:
Definitions :
max_initseg_sum: max_initseg_sum(i;L),
member: t T,
prop: ,
and: P 
Q,
so_lambda: 
x.t[x],
exists: 
x:A. B[x],
ge: i 
j ,
all: x:A. B[x],
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s],
int_seg: {i..j
},
subtype_rel: A 
r B
Lemmas :
or_wf,
equal-wf-base,
list_wf,
list_subtype_base,
int_subtype_base,
exists_wf,
all_wf,
int_seg_wf,
length_wf,
ge_wf,
initseg_sum_wf,
equal-wf-base-T
\mforall{}[i:\mBbbZ{}]. \mforall{}[L:\mBbbZ{} List]. (max\_initseg\_sum(i;L) \mmember{} \mBbbP{})
Date html generated:
2014_03_27-PM-01_47_16
Last ObjectModification:
2013_10_25-AM-09_18_08
Home
Index