Nuprl Lemma : maxsegsum_singleton
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