Nuprl Lemma : initseg_sum

r:

.

u:

.

v:

List. (initseg_sum(r;[u / v]) = (u + initseg_sum(r - 1;v)))

Proof

Definitions occuring in Statement : initseg_sum: initseg_sum(r;L), cons: [a / b], list: T List, nat:

, all:

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

, equal: s = t
Definitions : exists:

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

T, initseg_sum: initseg_sum(r;L), firstn: firstn(n;as), all:

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

Q, btrue: tt, ifthenelse: if b then t else f fi , bfalse: ff, subtype_rel: A

r B, not:

A, l_sum: l_sum(L), uall:

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

, bool:

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

Q, uimplies: b supposing a, or: P

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

b, assert:

b, false: False, le: A

B, prop:

, it:

Lemmas : initseg_sum_wf, equal-wf-base-T, int_subtype_base, equal-wf-T-base, cons_wf, lt_int_wf, bool_wf, eqtt_to_assert, assert_of_lt_int, eqff_to_assert, equal_wf, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, assert-bnot, less_than_wf, l_sum_wf, nil_wf, equal-wf-base, list_subtype_base
\mforall{}r:\mBbbN{}. \mforall{}u:\mBbbZ{}. \mforall{}v:\mBbbZ{} List. (initseg\_sum(r;[u / v]) = (u + initseg\_sum(r - 1;v))) Date html generated: 2014_03_27-PM-01_47_26 Last ObjectModification: 2013_11_04-AM-09_59_19 Home Index