Nuprl Lemma : first-choosable-property

{

[M:Type

Type].

[r:pRunType(P.M[P])].

[t:

].

[n:

].
first-choosable(r;t)

n supposing

lg-is-source(run-intransit(r;t);n) }

{ Proof }

Definitions occuring in Statement : first-choosable: first-choosable(r;t), run-intransit: run-intransit(r;t), pRunType: pRunType(T.M[T]), lg-is-source: lg-is-source(g;i), assert:

b, nat_plus:

, nat:

, uimplies: b supposing a, uall:

[x:A]. B[x], so_apply: x[s], le: A

B, function: x:A

B[x], universe: Type
Definitions : pair: <a, b>, 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), 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', 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), es-r-immediate-pred: es-r-immediate-pred(es;R;e';e), same-thread: same-thread(es;p;e;e'), 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), decidable: Dec(P), minus: -n, subtract: n - m, bfalse: ff, add: n + m, limited-type: LimitedType, btrue: tt, le_int: i

z j, eq_int: (i =

j), eq_atom: x =a y, null: null(as), set_blt: a <

b, grp_blt: a <

b, infix_ap: x f y, dcdr-to-bool: [d]

, bl-all: (

x

L.P[x])_b, bl-exists: (

x

L.P[x])_b, b-exists: (

i<n.P[i])_b, eq_type: eq_type(T;T'), eq_atom: eq_atom$n(x;y), qeq: qeq(r;s), q_less: q_less(r;s), q_le: q_le(r;s), deq-member: deq-member(eq;x;L), deq-disjoint: deq-disjoint(eq;as;bs), deq-all-disjoint: deq-all-disjoint(eq;ass;bs), eq_str: Error :eq_str, eq_id: a = b, eq_lnk: a = b, es-eq-E: e = e', es-bless: e <loc e', es-ble: e

loc e', bimplies: p

q, band: p

q, bor: p

q, search: search(k;P), lt_int: i <z j, bnot:

b, unit: Unit, exists:

x:A. B[x], is-dag: is-dag(g), rev_implies: P

Q, iff: P

Q, lelt: i

j < k, rationals:

, bool:

, int_seg: {i..j

}, let: let, real:

, grp_car: |g|, intensional-universe: IType, fpf: a:A fp-> B[a], subtype: S

T, es-E-interface: E(X), eclass: EClass(A[eo; e]), imax: imax(a;b), or: P

Q, length: ||as||, strong-subtype: strong-subtype(A;B), decide: case b of inl(x) => s[x] | inr(y) => t[y], ifthenelse: if b then t else f fi , natural_number: $n, ge: i

j , and: P

Q, uiff: uiff(P;Q), subtype_rel: A

r B, int:

, first-choosable: first-choosable(r;t), less_than: a < b, void: Void, false: False, implies: P

Q, le: A

B, prop:

, uimplies: b supposing a, set: {x:A| B[x]} , nat:

, top: Top, union: left + right, product: x:A

B[x], nat_plus:

, apply: f a, isect:

x:A. B[x], uall:

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

x.t[x], universe: Type, function: x:A

B[x], member: t

T, pRunType: pRunType(T.M[T]), all:

x:A. B[x], Auto: Error :Auto, lg-is-source: lg-is-source(g;i), assert:

b, not:

A, AssertBY: Error :AssertBY, CollapseTHEN: Error :CollapseTHEN, SplitOn: Error :SplitOn, MaAuto: Error :MaAuto, CollapseTHENA: Error :CollapseTHENA, lambda:

x.A[x], lg-size: lg-size(g), D: Error :D, run-intransit: run-intransit(r;t), so_apply: x[s], pInTransit: pInTransit(P.M[P]), ldag: LabeledDAG(T), equal: s = t, RepUR: Error :RepUR, tactic: Error :tactic
Lemmas : lg-is-source_wf, first-choosable_wf, member_wf, subtype_rel_wf, nat_wf, nat_properties, intensional-universe_wf, false_wf, not_wf, le_wf, run-intransit_wf, pInTransit_wf, lg-is-source_wf_dag, assert_wf, nat_plus_wf, pRunType_wf, ldag_wf, search_property, lg-size_wf_dag, int_seg_wf, bool_wf, iff_weakening_uiff, uiff_transitivity, eqtt_to_assert, assert_of_lt_int, search_wf, eqff_to_assert, assert_functionality_wrt_uiff, bnot_of_lt_int, assert_of_le_int, le_int_wf, bnot_wf, lt_int_wf, decidable__le, add_wf, lg-size_wf, int_seg_properties, btrue_neq_bfalse, assert_elim, not_assert_elim, ifthenelse_wf

\mforall{}[M:Type {}\mrightarrow{} Type]. \mforall{}[r:pRunType(P.M[P])]. \mforall{}[t:\mBbbN{}\msupplus{}]. \mforall{}[n:\mBbbN{}]. first-choosable(r;t) \mleq{} n supposing \muparrow{}lg-is-source(run-intransit(r;t);n) Date html generated: 2011_08_17-PM-03_43_04 Last ObjectModification: 2011_06_18-AM-11_24_10 Home Index