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
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  uimplies: b supposing a,  member: t ∈ T,  strong-type-continuous: Continuous+(T.F[T]),  ext-eq: A ≡ B,  and: P ∧ Q,  subtype_rel: A ⊆r B,  all: ∀x:A. B[x],  so_lambda: λ2x.t[x],  so_apply: x[s],  InitialSystem: InitialSystem(P.M[P]),  implies: P ⇒ Q,  let: let,  reliable-env: reliable-env(env; r),  run-msg-commands: run-msg-commands(r),  cand: A c∧ B,  run-command-node: run-command-node(r;t;n),  prop: ℙ,  pInTransit: pInTransit(P.M[P]),  pi2: snd(t),  sq_stable: SqStable(P),  squash: ↓T,  ldag: LabeledDAG(T),  nat: ℕ,  pEnvType: pEnvType(T.M[T]),  nat_plus: ℕ+,  le: A ≤ B,  guard: {T},  pRunType: pRunType(T.M[T]),  less_than': less_than'(a;b),  false: False,  not: ¬A,  exists: ∃x:A. B[x],  ge: i ≥ j ,  decidable: Dec(P),  or: P ∨ Q,  satisfiable_int_formula: satisfiable_int_formula(fmla),  top: Top,  sq_type: SQType(T),  int_seg: {i..j-},  lelt: i ≤ j < k,  uiff: uiff(P;Q),  rev_uimplies: rev_uimplies(P;Q),  is-dag: is-dag(g)
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: 2016_05_17-AM-10_57_10
Last ObjectModification: 2016_01_18-AM-00_13_36

Theory : process-model


Home Index