---

Step * 1 1 1 of Lemma reliable-env-property2

.....assertion..... 
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
     ∃e:runEvents(pRun(S;env;n2m;l2m))
      let t,n = tn 
      in (run-info(pRun(S;env;n2m;l2m);e)
         = intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))
         ∈ (ℤ × Id × pMsg(P.M[P])))
         ∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
10. t : ℕ@i
11. x : Id@i
12. \\%12 : ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
13. P : Process(P.M[P])@i
14. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
15. 0 < t
16. v1 : ℤ × Id@i
17. ms : pMsg(P.M[P])@i
18. let info,S = pRun(S;env;n2m;l2m) t in let ev,z,m = outl(info) in <ev, m> = <v1, ms> ∈ (ℤ × Id × pMsg(P.M[P]))@i
19. v2 : Process(P.M[P])@i
20. G : LabeledDAG(Id × pCom(P.M[P]))@i
21. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
22. n : ℕlg-size(G)@i
23. v3 : Id@i
24. v4 : pCom(P.M[P])@i
25. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
26. (com-kind(v4) ∈ ``msg choose new``)@i
⊢ add-cause(<t, x>;G) ⊆ snd(snd((pRun(S;env;n2m;l2m) t)))
BY
{ ((Assert ↑is-run-event(pRun(S;env;n2m;l2m);t;x) BY
          (Unhide THEN Auto))
   THEN MoveToConcl (-10)
   THEN MoveToConcl(-1)
   THEN RepUR ``is-run-event`` 0
   THEN RecUnfold `pRun` 0
   THEN Reduce 0
   THEN AutoSplit
   THEN (Assert (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>)) BY
               Trivial)
   THEN MoveToConcl (-1)
   THEN RepUR ``run-event-state-when`` 0) }

1
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
     ∃e:runEvents(pRun(S;env;n2m;l2m))
      let t,n = tn 
      in (run-info(pRun(S;env;n2m;l2m);e)
         = intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))
         ∈ (ℤ × Id × pMsg(P.M[P])))
         ∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
10. t : {1...}
11. x : Id@i
12. \\%12 : ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
13. P : Process(P.M[P])@i
14. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
15. 0 < t
16. v1 : ℤ × Id@i
17. ms : pMsg(P.M[P])@i
18. v2 : Process(P.M[P])@i
19. G : LabeledDAG(Id × pCom(P.M[P]))@i
20. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
21. n : ℕlg-size(G)@i
22. v3 : Id@i
23. v4 : pCom(P.M[P])@i
24. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
25. (com-kind(v4) ∈ ``msg choose new``)@i
⊢ (P ∈ let info,Cs,G = pRun(S;env;n2m;l2m) (t - 1) in 
   mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))
⇒ (↑let info,S = let n,m,nm = env t pRun(S;env;n2m;l2m) in 
     do-chosen-command(n2m;l2m;t;snd((pRun(S;env;n2m;l2m) (t - 1)));n;m;nm) 
     in isl(info) ∧b let ev,z,m = outl(info) in x = z)
⇒ (let info,S = let n,m,nm = env t pRun(S;env;n2m;l2m) in 
    do-chosen-command(n2m;l2m;t;snd((pRun(S;env;n2m;l2m) (t - 1)));n;m;nm) 
    in let ev,z,m = outl(info) in 
       <ev, m>
   = <v1, ms>
   ∈ (ℤ × Id × pMsg(P.M[P])))
⇒ add-cause(<t, x>;G) ⊆ snd(snd(let n,m,nm = env t pRun(S;env;n2m;l2m) in 
   do-chosen-command(n2m;l2m;t;snd((pRun(S;env;n2m;l2m) (t - 1)));n;m;nm)))

---

Latex:

---

Latex:
.....assertion..... 
1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  S  :  InitialSystem(P.M[P])@i
4.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
6.  env  :  pEnvType(P.M[P])@i
7.  pRun(S;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])
8.  reliable-env(env;  pRun(S;env;n2m;l2m))@i
9.  \mforall{}tn:run-msg-commands(pRun(S;env;n2m;l2m))
          \mexists{}e:runEvents(pRun(S;env;n2m;l2m))
            let  t,n  =  tn 
            in  ...
                  \mwedge{}  (run-event-loc(e)  =  (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))))
10.  t  :  \mBbbN{}@i
11.  x  :  Id@i
12.  \mbackslash{}\mbackslash{}\%12  :  \muparrow{}is-run-event(pRun(S;env;n2m;l2m);t;x)@i
13.  P  :  Process(P.M[P])@i
14.  (P  \mmember{}  run-event-state-when(pRun(S;env;n2m;l2m);<t,  x>))@i
15.  0  <  t
16.  v1  :  \mBbbZ{}  \mtimes{}  Id@i
17.  ms  :  pMsg(P.M[P])@i
18.  let  info,S  =  pRun(S;env;n2m;l2m)  t  in  let  ev,z,m  =  outl(info)  in  <ev,  m>  =  <v1,  ms>@i
19.  v2  :  Process(P.M[P])@i
20.  G  :  LabeledDAG(Id  \mtimes{}  pCom(P.M[P]))@i
21.  Process-apply(P;ms)  =  <v2,  G>@i
22.  n  :  \mBbbN{}lg-size(G)@i
23.  v3  :  Id@i
24.  v4  :  pCom(P.M[P])@i
25.  lg-label(G;n)  =  <v3,  v4>@i
26.  (com-kind(v4)  \mmember{}  ``msg  choose  new``)@i
\mvdash{}  add-cause(<t,  x>G)  \msubseteq{}  snd(snd((pRun(S;env;n2m;l2m)  t)))


By

---

Latex:
((Assert  \muparrow{}is-run-event(pRun(S;env;n2m;l2m);t;x)  BY
                (Unhide  THEN  Auto))
  THEN  MoveToConcl  (-10)
  THEN  MoveToConcl(-1)
  THEN  RepUR  ``is-run-event``  0
  THEN  RecUnfold  `pRun`  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  (Assert  (P  \mmember{}  run-event-state-when(pRun(S;env;n2m;l2m);<t,  x>))  BY
                          Trivial)
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``run-event-state-when``  0)

---

Home Index