Nuprl Lemma : maxsegsum

x:

. (max_seg_sum(x;[x])

max_initseg_sum(x;[x]))

Proof

Definitions occuring in Statement : max_initseg_sum: max_initseg_sum(i;L), max_seg_sum: max_seg_sum(m;L), nil: [], cons: [a / b], all:

x:A. B[x], and: P

Q, int:

Definitions : max_seg_sum: max_seg_sum(m;L), and: P

Q, prop:

, member: t

T, or: P

Q, guard: {T}, so_lambda:

x.t[x], exists:

x:A. B[x], all:

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

j , le: A

B, not:

A, false: False, implies: P

Q, lelt: i

j < k, int_seg: {i..j

}, max_initseg_sum: max_initseg_sum(i;L), uall:

[x:A]. B[x], so_apply: x[s], uimplies: b supposing a, subtype_rel: A

r B
Lemmas : int_subtype_base, list_wf, equal-wf-base, exists_wf, list_subtype_base, cons_wf, nil_wf, length_wf, int_seg_wf, seg_sum_wf, ge_wf, seg_sum0, initseg_sum0, equal-wf-base-T, lelt_wf, initseg_sum_wf
\mforall{}x:\mBbbZ{}. (max\_seg\_sum(x;[x]) \mwedge{} max\_initseg\_sum(x;[x])) Date html generated: 2014_03_27-PM-01_47_55 Last ObjectModification: 2013_11_04-AM-10_16_44 Home Index