Nuprl Lemma : maxsegsum_sqexists
L:
List. (
p:{ 
| let m,i = p in max_seg_sum(m;L) 
max_initseg_sum(i;L)})
Proof
Definitions occuring in Statement :
max_initseg_sum: max_initseg_sum(i;L),
max_seg_sum: max_seg_sum(m;L),
list: T List,
all: x:A. B[x],
sq_exists: x:{A| B[x]},
and: P Q,
spread: spread def,
product: x:A B[x],
int:
Definitions :
all: x:A. B[x],
member: t 
T,
implies: P 
Q,
sq_exists: x:{A| B[x]},
prop: 
,
and: P Q,
max_seg_sum: max_seg_sum(m;L),
or: P 
Q,
cand: A c B,
so_lambda: 
x.t[x],
exists: x:A. B[x],
ge: i 
j ,
max_initseg_sum: max_initseg_sum(i;L),
guard: {T},
subtype_rel: A 
r B,
int_seg: {i..j
},
nat: 
,
lelt: i 
j < k,
le: A B,
not: 
A,
false: False,
imax: imax(a;b),
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
nat_plus: 
,
squash: 
T,
true: True,
iff: P 
Q,
rev_implies: P Q,
uall: [x:A]. B[x],
uimplies: b supposing a,
unit: Unit,
bool: 
,
list: T List,
so_apply: x[s],
decidable: Dec(P),
uiff: uiff(P;Q),
sq_type: SQType(T),
bnot: 
b,
assert: 
b,
rev_uimplies: rev_uimplies(P;Q),
cons: [a / b],
nil: [],
it: 
,
has-value: (a)
Lemmas :
list_wf,
non-axiom-listunion,
subtype_rel_b-union-right,
axiom-listunion,
unit_wf2,
subtype_rel_b-union-left,
bool_wf,
isaxiom_wf_listunion,
max_seg_sum_wf,
nil_wf,
max_initseg_sum_wf,
exists_wf,
equal-wf-base,
list_subtype_base,
int_subtype_base,
all_wf,
int_seg_wf,
length_wf,
ge_wf,
seg_sum_wf,
equal-wf-base-T,
initseg_sum_wf,
isaxiom_wf_list,
unit_subtype_list,
axiom-list,
product_subtype_list,
non-axiom-list,
cons_wf,
maxsegsum_singleton,
imax_wf,
decidable__equal_int,
initseg_sum0,
imax_ge_left,
initseg_sum_shift,
subtype_rel_sets,
lelt_wf,
le_wf,
btrue_wf,
and_wf,
equal_wf,
null_wf,
bfalse_wf,
btrue_neq_bfalse,
length_cons,
non_neg_length,
length_wf_nat,
imax_ge_right,
decidable__le,
value-type-has-value,
int-value-type,
le_int_wf,
eqtt_to_assert,
assert_of_le_int,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
seg_sum0,
seg_sum_shift,
less_than_wf,
ite_rw_true,
squash_wf,
true_wf,
imax_unfold,
ite_rw_false,
not_wf,
assert_wf
\mforall{}L:\mBbbZ{} List. (\mexists{}p:\{\mBbbZ{} \mtimes{} \mBbbZ{}| let m,i = p in max\_seg\_sum(m;L) \mwedge{} max\_initseg\_sum(i;L)\})
Date html generated:
2014_01_21-PM-02_39_38
Last ObjectModification:
2013_11_07-PM-02_54_21
Home
Index