Nuprl Lemma : max_seg_sum

[m:

].

[L:

List]. (max_seg_sum(m;L)

)

Proof

Definitions occuring in Statement : max_seg_sum: max_seg_sum(m;L), list: T List, uall:

[x:A]. B[x], prop:

, member: t

T, int:

Definitions : uall:

[x:A]. B[x], member: t

T, max_seg_sum: max_seg_sum(m;L), prop:

, and: P

Q, so_lambda:

x.t[x], exists:

x:A. B[x], ge: i

j , all:

x:A. B[x], uimplies: b supposing a, so_apply: x[s], int_seg: {i..j

}, subtype_rel: A

r B
Lemmas : list_wf, or_wf, equal-wf-base, list_subtype_base, int_subtype_base, exists_wf, all_wf, int_seg_wf, length_wf, ge_wf, seg_sum_wf, equal-wf-base-T
\mforall{}[m:\mBbbZ{}]. \mforall{}[L:\mBbbZ{} List]. (max\_seg\_sum(m;L) \mmember{} \mBbbP{}) Date html generated: 2014_03_27-PM-01_47_14 Last ObjectModification: 2013_10_25-AM-09_13_12 Home Index