Nuprl Lemma : seg_sum

p,q:

.

L:

List. (seg_sum(p;q;L) = seg_sum(p - 1;q - 1;tl(L)))

Proof

Definitions occuring in Statement : seg_sum: seg_sum(p;q;L), tl: tl(l), list: T List, nat_plus:

, all:

x:A. B[x], subtract: n - m, natural_number: $n, int:

, equal: s = t
Definitions : all:

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

T, exists:

x:A. B[x], segment: as[m..n

], seg_sum: seg_sum(p;q;L), nth_tl: nth_tl(n;as), implies: P

Q, btrue: tt, ifthenelse: if b then t else f fi , not:

A, bfalse: ff, subtype_rel: A

r B, uall:

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

, bool:

, unit: Unit, uiff: uiff(P;Q), and: P

Q, uimplies: b supposing a, le: A

B, false: False, or: P

Q, sq_type: SQType(T), guard: {T}, bnot:

b, assert:

b, prop:

, it:

Lemmas : list_wf, nat_plus_wf, seg_sum_wf, tl_wf, equal-wf-base-T, int_subtype_base, equal-wf-T-base, le_int_wf, bool_wf, eqtt_to_assert, assert_of_le_int, l_sum_wf, firstn_wf, eqff_to_assert, equal_wf, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, assert-bnot, le_wf, nth_tl_wf
\mforall{}p,q:\mBbbN{}\msupplus{}. \mforall{}L:\mBbbZ{} List. (seg\_sum(p;q;L) = seg\_sum(p - 1;q - 1;tl(L))) Date html generated: 2014_03_27-PM-01_47_21 Last ObjectModification: 2013_11_04-PM-01_11_58 Home Index