---

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


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. reliable-env(env; pRun(S;env;n2m;l2m))@i
8. ∀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)
9. t : {1...}
10. x : Id@i
11. [%12] : ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
12. P : Process(P.M[P])@i
13. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
14. 0 < t
15. v1 : ℤ × Id@i
16. ms : pMsg(P.M[P])@i
17. v2 : Process(P.M[P])@i
18. G : LabeledDAG(Id × pCom(P.M[P]))@i
19. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
20. n : ℕlg-size(G)@i
21. v3 : Id@i
22. v4 : pCom(P.M[P])@i
23. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
24. (com-kind(v4) ∈ ``msg choose new``)@i
25. v5 : ℤ × Id × Id × pMsg(P.M[P])?@i
26. v7 : component(P.M[P]) List@i
27. v8 : LabeledDAG(pInTransit(P.M[P]))@i
28. (pRun(S;env;n2m;l2m) (t - 1)) = <v5, v7, v8> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
29. v9 : ℕ@i
30. ¬↑lg-is-source(v8;v9)
31. v11 : ℕ@i
32. v12 : Id@i
33. (env t pRun(S;env;n2m;l2m)) = <v9, v11, v12> ∈ (ℕ × ℕ × Id)@i
⊢ (P ∈ mapfilter(λc.(snd(c));λc.fst(c) = x;v7))
⇒ False
⇒ (let ev,z,m = ⊥ in <ev, m> = <v1, ms> ∈ (ℤ × Id × pMsg(P.M[P])))
⇒ add-cause(<t, x>;G) ⊆ v8
BY
{ ((Assert λc.fst(c) = x ∈ component(P.M[P]) ⟶ 𝔹 BY Auto) THEN Auto)⋅ }

---

Latex:

---

Latex:

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.  reliable-env(env;  pRun(S;env;n2m;l2m))@i
8.  \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)))))
9.  t  :  \{1...\}
10.  x  :  Id@i
11.  [\%12]  :  \muparrow{}is-run-event(pRun(S;env;n2m;l2m);t;x)@i
12.  P  :  Process(P.M[P])@i
13.  (P  \mmember{}  run-event-state-when(pRun(S;env;n2m;l2m);<t,  x>))@i
14.  0  <  t
15.  v1  :  \mBbbZ{}  \mtimes{}  Id@i
16.  ms  :  pMsg(P.M[P])@i
17.  v2  :  Process(P.M[P])@i
18.  G  :  LabeledDAG(Id  \mtimes{}  pCom(P.M[P]))@i
19.  Process-apply(P;ms)  =  <v2,  G>@i
20.  n  :  \mBbbN{}lg-size(G)@i
21.  v3  :  Id@i
22.  v4  :  pCom(P.M[P])@i
23.  lg-label(G;n)  =  <v3,  v4>@i
24.  (com-kind(v4)  \mmember{}  ``msg  choose  new``)@i
25.  v5  :  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P])?@i
26.  v7  :  component(P.M[P])  List@i
27.  v8  :  LabeledDAG(pInTransit(P.M[P]))@i
28.  (pRun(S;env;n2m;l2m)  (t  -  1))  =  <v5,  v7,  v8>@i
29.  v9  :  \mBbbN{}@i
30.  \mneg{}\muparrow{}lg-is-source(v8;v9)
31.  v11  :  \mBbbN{}@i
32.  v12  :  Id@i
33.  (env  t  pRun(S;env;n2m;l2m))  =  <v9,  v11,  v12>@i
\mvdash{}  (P  \mmember{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;v7))  {}\mRightarrow{}  False  {}\mRightarrow{}  (let  ev,z,m  =  \mbot{}  in  <ev,  m>  =  <v1,  ms>)  {}\000C\mRightarrow{}  add-cause(<t,  x>G)  \msubseteq{}  v8


By

---

Latex:
((Assert  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}  BY  Auto)  THEN  Auto)\mcdot{}

---

Home Index