Nuprl Lemma : debug2

{

m:

. Dec(

i:

m. (0 < i)) }

{ Proof }

Definitions occuring in Statement : int_seg: {i..j

}, decidable: Dec(P), all:

x:A. B[x], less_than: a < b, natural_number: $n, int:

Definitions : real:

, rationals:

, subtype: S

T, lambda:

x.A[x], natural_number: $n, member: t

T, le: A

B, assert:

b, so_lambda:

x.t[x], divides: b | a, assoced: a ~ b, set_leq: a

b, set_lt: a <p b, grp_lt: a < b, cand: A c

B, l_member: (x

l), l_contains: A

B, inject: Inj(A;B;f), reducible: reducible(a), prime: prime(a), squash:

T, l_exists: (

x

L. P[x]), l_all: (

x

L.P[x]), fun-connected: y is f*(x), qle: r

s, qless: r < s, q-rel: q-rel(r;x), i-finite: i-finite(I), i-closed: i-closed(I), p-outcome: Outcome, fset-member: a

s, f-subset: xs

ys, fset-closed: (s closed under fs), set: {x:A| B[x]} , l_disjoint: l_disjoint(T;l1;l2), cs-not-completed: in state s, a has not completed inning i, cs-archived: by state s, a archived v in inning i, cs-passed: by state s, a passed inning i without archiving a value, cs-inning-committed: in state s, inning i has committed v, cs-inning-committable: in state s, inning i could commit v , cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i, cs-precondition: state s may consider v in inning i, es-causl: (e < e'), es-locl: (e <loc e'), es-le: e

loc e' , es-causle: e c

e', es-E: E, existse-before:

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

e

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

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

e

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

e

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

e

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

e

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

e

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

e

(e1,e2].P[e], es-fset-loc: i

locs(s), product: x:A

B[x], exists:

x:A. B[x], es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), same-thread: same-thread(es;p;e;e'), implies: P

Q, collect-event: collect-event(es;X;n;v.num[v];L.P[L];e), cut-order: a

(X;f) b, path-goes-thru: x-f*-y thru i, lg-edge: lg-edge(g;a;b), equal: s = t, int:

, less_than: a < b, int_seg: {i..j

}, prop:

, universe: Type, ses-legal-sequence: Legal(pas) given prvt, ses-action: Action(e), uimplies: b supposing a, decidable: Dec(P), infix_ap: x f y, apply: f a, function: x:A

B[x], uall:

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

x:A. B[x], all:

x:A. B[x]
Lemmas : decidable_wf, decidable__all_int_seg, decidable__lt, int_seg_wf

\mforall{}m:\mBbbZ{}. Dec(\mforall{}i:\mBbbN{}m. (0 < i)) Date html generated: 2011_08_17-PM-07_39_39 Last ObjectModification: 2010_12_23-AM-00_50_17 Home Index