---

{ [M:Type  Type]. [t:]. [r:t  (  Id  Id  pMsg(P.M[P])?
                                         System(P.M[P]))].
    (first-choosable(r;t)  ) }

{ Proof }

---

Definitions occuring in Statement :  first-choosable: first-choosable(r;t),  System: System(P.M[P]),  pMsg: pMsg(P.M[P]),  Id: Id,  int_seg: {i..j},  nat_plus: ,  nat: ,  uall: [x:A]. B[x],  so_apply: x[s],  unit: Unit,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  union: left + right,  natural_number: $n,  int: ,  universe: Type
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  first-choosable: first-choosable(r;t),  let: let,  so_lambda: x.t[x],  all: x:A. B[x],  implies: P  Q,  int_seg: {i..j},  pi2: snd(t),  run-system: run-system(r;t),  lelt: i  j < k,  and: P  Q,  le: A  B,  not: A,  false: False,  nat: ,  ifthenelse: if b then t else f fi ,  prop: ,  btrue: tt,  bfalse: ff,  nat_plus: ,  System: System(P.M[P]),  ldag: LabeledDAG(T),  unit: Unit,  bool: ,  iff: P  Q,  uimplies: b supposing a,  it:
Lemmas :  int_seg_wf,  Id_wf,  pMsg_wf,  unit_wf,  System_wf,  nat_plus_wf,  labeled-graph_wf,  pInTransit_wf,  le_wf,  lt_int_wf,  search_wf,  lg-size_wf,  lg-is-source_wf,  nat_wf,  bool_wf,  iff_weakening_uiff,  uiff_transitivity,  assert_wf,  eqtt_to_assert,  assert_of_lt_int,  le_int_wf,  bnot_wf,  eqff_to_assert,  assert_functionality_wrt_uiff,  bnot_of_lt_int,  assert_of_le_int

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[t:\mBbbN{}\msupplus{}].  \mforall{}[r:\mBbbN{}t  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?  \mtimes{}  System(P.M[P]))].
    (first-choosable(r;t)  \mmember{}  \mBbbN{})


Date html generated: 2011_08_17-PM-03_42_43
Last ObjectModification: 2011_06_18-AM-11_23_58

Home Index