Nuprl Lemma : std-component-property

∀[M:Type ─→ Type]
  ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀x:Id. ∀Q:Process(P.M[P]).
    assuming(env,r.reliable-env(env; r))
     <[<x, Q>], lg-nil()> |= es.∃cause:E ─→ (E?)
                               ∀e:E
                                 let G = last(data-stream(Q;map(λe.info(e);≤loc(e)))) in
                                     ∀p∈G.let y,c = p 
                                          in (com-kind(c) ∈ ``msg choose new``)
                                             ⇒ (∃e':E
                                                  ((loc(e') = y ∈ Id)
                                                  ∧ (e < e')
                                                  ∧ (∃n:ℕ
                                                      ∃nm:Id
                                                       (info(e') = command-to-msg(c;n2m n;l2m nm) ∈ pMsg(P.M[P])))
                                                  ∧ ((cause e') = (inl e) ∈ (E?)))) 
                                 supposing loc(e) = x ∈ Id 
  supposing Continuous+(P.M[P])


Proof



Definitions occuring in Statement :  system-strongly-realizes: system-strongly-realizes,  command-to-msg: command-to-msg(c;nmsg;lmsg),  reliable-env: reliable-env(env; r),  com-kind: com-kind(c),  pMsg: pMsg(P.M[P]),  Process: Process(P.M[P]),  data-stream: data-stream(P;L),  lg-all: ∀x∈G.P[x],  lg-nil: lg-nil(),  es-info: info(e),  es-le-before: ≤loc(e),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  Id: Id,  last: last(L),  l_member: (x ∈ l),  map: map(f;as),  cons: [a / b],  nil: [],  strong-type-continuous: Continuous+(T.F[T]),  nat: ℕ,  let: let,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  so_apply: x[s],  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  unit: Unit,  apply: f a,  lambda: λx.A[x],  function: x:A ─→ B[x],  spread: spread def,  pair: <a, b>,  inl: inl x,  union: left + right,  token: "$token",  atom: Atom,  universe: Type,  equal: s = t ∈ T
Lemmas :  std-components-property,  nat_wf,  cons_wf,  nil_wf,  reliable-env_wf,  pRun_wf2,  pEnvType_wf,  sub-system_wf,  component_wf,  Id_wf,  Process_wf,  lg-nil_wf_dag,  pInTransit_wf,  InitialSystem_wf,  pMsg_wf,  strong-type-continuous_wf,  length_of_cons_lemma,  length_of_nil_lemma,  false_wf,  lelt_wf,  all_wf,  es-E_wf,  stdEO_wf,  event-ordering+_subtype,  isect_wf,  es-loc_wf,  last_wf,  pExt_wf,  Process-stream_wf,  map_wf,  es-info_wf,  es-le-before_wf,  list_wf,  map_append_sq,  map_cons_lemma,  map_nil_lemma,  list-cases,  product_subtype_list,  append_is_nil,  null_nil_lemma,  btrue_wf,  null_cons_lemma,  bfalse_wf,  es-before_wf,  and_wf,  equal_wf,  null_wf3,  subtype_rel_list,  top_wf,  btrue_neq_bfalse,  list_ind_nil_lemma,  list_ind_cons_lemma,  not_wf,  less_than_wf,  data-stream-cons,  lg-all_wf,  pCom_wf,  l_member_wf,  com-kind_wf,  exists_wf,  es-causl_wf,  command-to-msg_wf,  unit_wf2
Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}x:Id.  \mforall{}Q:Process(P.M[P]).
        assuming(env,r.reliable-env(env;  r))
          <[<x,  Q>],  lg-nil()>  |=  es.\mexists{}cause:E  {}\mrightarrow{}  (E?)
                                                              \mforall{}e:E
                                                                  let  G  =  last(data-stream(Q;map(\mlambda{}e.info(e);\mleq{}loc(e))))  in
                                                                          \mforall{}p\mmember{}G.let  y,c  =  p 
                                                                                    in  (com-kind(c)  \mmember{}  ``msg  choose  new``)
                                                                                          {}\mRightarrow{}  (\mexists{}e':E
                                                                                                    ((loc(e')  =  y)
                                                                                                    \mwedge{}  (e  <  e')
                                                                                                    \mwedge{}  (\mexists{}n:\mBbbN{}
                                                                                                            \mexists{}nm:Id
                                                                                                              (info(e')  =  command-to-msg(c;n2m  n;l2m  nm)))
                                                                                                    \mwedge{}  ((cause  e')  =  (inl  e)))) 
                                                                  supposing  loc(e)  =  x 
    supposing  Continuous+(P.M[P])


Date html generated: 2015_07_23-AM-11_25_21
Last ObjectModification: 2015_01_28-PM-11_18_22

Home Index