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