Nuprl Lemma : vr_baseK

Nuprl Lemma : vr_baseK

n:

.

k:{i:

| 2

i} .

L:

k List. (n =

(k^i * L[i] | i < ||L||))

Proof not projected

Definitions occuring in Statement : select: l[i], length: ||as||, int_seg: {i..j

}, nat:

, le: A

B, all:

x:A. B[x], exists:

x:A. B[x], set: {x:A| B[x]} , list: type List, multiply: n * m, natural_number: $n, int:

, equal: s = t, sum:

(f[x] | x < k), exp: i^n
Definitions : tactic: Error :tactic, THENA: Error :THENA, Auto: Error :Auto, equal: s = t, member: t

T, isect:

x:A. B[x], uall:

[x:A]. B[x], universe: Type, prop:

, le: A

B, int:

, set: {x:A| B[x]} , nat:

, product: x:A

B[x], exists:

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

B[x], all:

x:A. B[x], natural_number: $n, void: Void, less_than: a < b, subtract: n - m, add: n + m, minus: -n, not:

A, false: False, list: type List, int_seg: {i..j

}, implies: P

Q, ge: i

j , THEN: Error :THEN, nil: [], limited-type: LimitedType, sum:

(f[x] | x < k), so_lambda:

x.t[x], lambda:

x.A[x], length: ||as||, top: Top, subtype: S

T, rationals:

, real:

, multiply: n * m, exp: i^n, nat_plus:

, int_nzero:

, lelt: i

j < k, and: P

Q, select: l[i], uimplies: b supposing a, subtype_rel: A

r B, sq_type: SQType(T), guard: {T}, cons: [car / cdr], Unfold: Error :Unfold, uiff: uiff(P;Q), strong-subtype: strong-subtype(A;B), p-outcome: Outcome, exp0: exp0{exp0_compseq_tag_def:o}(i), fpf: a:A fp-> B[a], pair: <a, b>, eclass: EClass(A[eo; e]), iff: P

Q, rev_implies: P

Q, hd: hd(l), tl: tl(l), lg-edge: lg-edge(g;a;b), decidable: Dec(P), apply: f a, infix_ap: x f y, ses-action: Action(e), ses-legal-sequence: Legal(pas) given prvt, path-goes-thru: x-f*-y thru i, cut-order: a

(X;f) b, collect-event: collect-event(es;X;n;v.num[v];L.P[L];e), same-thread: same-thread(es;p;e;e'), es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), es-fset-loc: i

locs(s), existse-between3:

e

(e1,e2].P[e], existse-between2:

e

[e1,e2].P[e], alle-between2:

e

[e1,e2].P[e], existse-between1:

e

[e1,e2).P[e], alle-between1:

e

[e1,e2).P[e], alle-le:

e

e'.P[e], alle-lt:

e<e'.P[e], existse-le:

e

e'.P[e], existse-before:

e<e'.P[e], es-causle: e c

e', es-le: e

loc e' , es-locl: (e <loc e'), es-causl: (e < e'), cs-precondition: state s may consider v in inning i, cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i, cs-inning-committable: in state s, inning i could commit v , cs-inning-committed: in state s, inning i has committed v, cs-passed: by state s, a passed inning i without archiving a value, cs-archived: by state s, a archived v in inning i, cs-not-completed: in state s, a has not completed inning i, l_disjoint: l_disjoint(T;l1;l2), fset-closed: (s closed under fs), f-subset: xs

ys, fset-member: a

s, i-closed: i-closed(I), i-finite: i-finite(I), sq_exists:

x:{A| B[x]}, q-rel: q-rel(r;x), qless: r < s, qle: r

s, fun-connected: y is f*(x), l_all: (

x

L.P[x]), l_exists: (

x

L. P[x]), squash:

T, prime: prime(a), reducible: reducible(a), inject: Inj(A;B;f), cmp-le: cmp-le(cmp;x;y), l_contains: A

B, l_member: (x

l), cand: A c

B, grp_lt: a < b, set_lt: a <p b, set_leq: a

b, assoced: a ~ b, divides: b | a, assert:

b, or: P

Q, union: left + right
Lemmas : decidable__lt, add_functionality_wrt_eq, exp1, exp_add, sum_scalar_mult, iff_wf, rev_implies_wf, sum_functionality, int_seg_properties, select_cons_tl, sum_split, length_cons, non_neg_length, not_wf, false_wf, int_subtype_base, set_subtype_base, subtype_base_sq, length_wf, member_wf, select_wf, exp_wf2, top_wf, length_wf_nat, sum_wf, nat_ind_tp, nat_properties, ge_wf, int_seg_wf, nat_wf, le_wf

\mforall{}n:\mBbbN{}. \mforall{}k:\{i:\mBbbZ{}| 2 \mleq{} i\} . \mexists{}L:\mBbbN{}k List. (n = \mSigma{}(k\^{}i * L[i] | i < ||L||)) Date html generated: 2012_02_20-PM-03_31_45 Last ObjectModification: 2012_02_02-PM-01_55_02 Home Index