---

Step * 1 1 of Lemma local-simulation-classrel


1. [f] : Name ─→ Type
2. [Info] : Type
3. [T] : Type
4. [X] : EClass(T)
5. locs : bag(Id)@i
6. hdr : Name@i
7. [%] : hdr encodes Id × Info
8. local-simulation-class(X;locs;hdr) ∈ EClass(T)
9. es : EO+(Message(f))@i'
10. e : E@i
11. [%4] : LocalClass(X)
12. [v] : T
13. ↑has-header-and-in-locs(info(e);hdr;locs)
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Info)
15. local-simulation-event(es;e;hdr;locs) ∈ E
16. e1 : E@i
17. local-simulation-event(es;e;hdr;locs) = e1 ∈ E@i
⊢ uiff(↓∃i:Id. (i ↓∈ locs ∧ v ∈ base-process-class(X;i;hdr)(e));True ∧ v ∈ X(e1))
BY
{ (RWO "assert-has-header-and-in-locs" (-5) THEN Auto) }

1
1. f : Name ─→ Type
2. Info : Type
3. T : Type
4. X : EClass(T)
5. locs : bag(Id)@i
6. hdr : Name@i
7. hdr encodes Id × Info
8. local-simulation-class(X;locs;hdr) ∈ EClass(T)
9. es : EO+(Message(f))@i'
10. e : E@i
11. LocalClass(X)
12. v : T
13. msg-header(info(e)) = hdr ∈ Name
14. fst(msg-body(info(e))) ↓∈ locs
15. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Info)
16. local-simulation-event(es;e;hdr;locs) ∈ E
17. e1 : E@i
18. local-simulation-event(es;e;hdr;locs) = e1 ∈ E@i
19. ↓∃i:Id. (i ↓∈ locs ∧ v ∈ base-process-class(X;i;hdr)(e))
⊢ v ∈ X(e1)

2
1. f : Name ─→ Type
2. Info : Type
3. T : Type
4. X : EClass(T)
5. locs : bag(Id)@i
6. hdr : Name@i
7. hdr encodes Id × Info
8. local-simulation-class(X;locs;hdr) ∈ EClass(T)
9. es : EO+(Message(f))@i'
10. e : E@i
11. LocalClass(X)
12. v : T
13. msg-header(info(e)) = hdr ∈ Name
14. fst(msg-body(info(e))) ↓∈ locs
15. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Info)
16. local-simulation-event(es;e;hdr;locs) ∈ E
17. e1 : E@i
18. local-simulation-event(es;e;hdr;locs) = e1 ∈ E@i
19. True
20. v ∈ X(e1)
⊢ ↓∃i:Id. (i ↓∈ locs ∧ v ∈ base-process-class(X;i;hdr)(e))

---

Latex:

---

Latex:

1.  [f]  :  Name  {}\mrightarrow{}  Type
2.  [Info]  :  Type
3.  [T]  :  Type
4.  [X]  :  EClass(T)
5.  locs  :  bag(Id)@i
6.  hdr  :  Name@i
7.  [\%]  :  hdr  encodes  Id  \mtimes{}  Info
8.  local-simulation-class(X;locs;hdr)  \mmember{}  EClass(T)
9.  es  :  EO+(Message(f))@i'
10.  e  :  E@i
11.  [\%4]  :  LocalClass(X)
12.  [v]  :  T
13.  \muparrow{}has-header-and-in-locs(info(e);hdr;locs)
14.  local-simulation-eo(es;e;hdr;locs)  \mmember{}  EO+(Info)
15.  local-simulation-event(es;e;hdr;locs)  \mmember{}  E
16.  e1  :  E@i
17.  local-simulation-event(es;e;hdr;locs)  =  e1@i
\mvdash{}  uiff(\mdownarrow{}\mexists{}i:Id.  (i  \mdownarrow{}\mmember{}  locs  \mwedge{}  v  \mmember{}  base-process-class(X;i;hdr)(e));True  \mwedge{}  v  \mmember{}  X(e1))


By

---

Latex:
(RWO  "assert-has-header-and-in-locs"  (-5)  THEN  Auto)

---

Home Index