Nuprl Lemma : reliable-env-property1

∀[M:Type ─→ Type]
  ∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]).
    let r = pRun(S0;env;n2m;l2m) in
        reliable-env(env; r)
        ⇒ (∀tn:run-msg-commands(r)
              let t,n = tn 
              in ∃t':ℕ
                  ((t < t'
                  c∧ (((fst((env t' r))) ≤ n)
                     ∧ ↑lg-is-source(run-intransit(r;t');fst((env t' r))) supposing 0 < lg-size(run-intransit(r;t'))))
                  ∧ (∀i:ℕ
                       ¬(t < i
                       c∧ (((fst((env i r))) ≤ n)
                          ∧ ↑lg-is-source(run-intransit(r;i);fst((env i r))) 
                            supposing 0 < lg-size(run-intransit(r;i)))) 
                       supposing i < t'))) 
  supposing Continuous+(P.M[P])


Proof



Definitions occuring in Statement :  run-msg-commands: run-msg-commands(r),  reliable-env: reliable-env(env; r),  InitialSystem: InitialSystem(P.M[P]),  run-intransit: run-intransit(r;t),  pRun: pRun(S0;env;nat2msg;loc2msg),  pEnvType: pEnvType(T.M[T]),  pMsg: pMsg(P.M[P]),  lg-is-source: lg-is-source(g;i),  lg-size: lg-size(g),  Id: Id,  strong-type-continuous: Continuous+(T.F[T]),  nat: ℕ,  assert: ↑b,  less_than: a < b,  let: let,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  cand: A c∧ B,  so_apply: x[s],  pi1: fst(t),  le: A ≤ B,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q,  apply: f a,  function: x:A ─→ B[x],  spread: spread def,  natural_number: $n,  universe: Type
Lemmas :  run-intransit_wf,  ldag_wf,  pInTransit_wf,  lg-size_wf,  nat_wf,  lg-is-source_wf,  decidable__cand,  less_than_wf,  le_wf,  less_than_transitivity2,  subtype_rel_dep_function,  Id_wf,  pMsg_wf,  unit_wf2,  top_wf,  int_seg_wf,  int_seg_subtype-nat,  false_wf,  subtype_rel_self,  assert_wf,  decidable__lt,  isect_wf,  decidable__le,  decidable__uimplies,  member-less_than,  decidable__assert,  sq_stable__le,  le_transitivity,  le_weakening,  assert_witness,  subtype_base_sq,  int_subtype_base,  sq_stable__all,  sq_stable__assert,  squash_wf,  assert-lg-is-source,  lelt_wf,  less_than_transitivity1,  less_than_irreflexivity,  lg-edge_wf,  mu-wf2,  mu-property2,  all_wf,  not_wf
Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}S0:InitialSystem(P.M[P]).  \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).
        let  r  =  pRun(S0;env;n2m;l2m)  in
                reliable-env(env;  r)
                {}\mRightarrow{}  (\mforall{}tn:run-msg-commands(r)
                            let  t,n  =  tn 
                            in  \mexists{}t':\mBbbN{}
                                    ((t  <  t'
                                    c\mwedge{}  (((fst((env  t'  r)))  \mleq{}  n)
                                          \mwedge{}  \muparrow{}lg-is-source(run-intransit(r;t');fst((env  t'  r))) 
                                              supposing  0  <  lg-size(run-intransit(r;t'))))
                                    \mwedge{}  (\mforall{}i:\mBbbN{}
                                              \mneg{}(t  <  i
                                              c\mwedge{}  (((fst((env  i  r)))  \mleq{}  n)
                                                    \mwedge{}  \muparrow{}lg-is-source(run-intransit(r;i);fst((env  i  r))) 
                                                        supposing  0  <  lg-size(run-intransit(r;i)))) 
                                              supposing  i  <  t'))) 
    supposing  Continuous+(P.M[P])


Date html generated: 2015_07_23-AM-11_17_42
Last ObjectModification: 2015_01_28-PM-11_20_14

Home Index