---

Step * 2 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. ¬↑has-header-and-in-locs(info(e);hdr;locs)
12. [%4] : LocalClass(X)
13. [v] : T
⊢ uiff(v ∈ local-simulation-class(X;locs;hdr)(e);False ∧ v ∈ X(local-simulation-event(es;e;hdr;locs)))
BY
{ (D 0
   THEN D 0
   THEN Auto
   THEN Unfold `local-simulation-class` -1
   THEN (RWO "parallel-bag-classrel" (-1) THENA Auto)
   THEN SqExRepD) }

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. ¬↑has-header-and-in-locs(info(e);hdr;locs)
12. LocalClass(X)
13. v : T
14. i : Id
15. i ↓∈ locs
16. v ∈ base-process-class(X;i;hdr)(e)
⊢ False

---

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.  \mneg{}\muparrow{}has-header-and-in-locs(info(e);hdr;locs)
12.  [\%4]  :  LocalClass(X)
13.  [v]  :  T
\mvdash{}  uiff(v  \mmember{}  local-simulation-class(X;locs;hdr)(e);False
\mwedge{}  v  \mmember{}  X(local-simulation-event(es;e;hdr;locs)))


By

---

Latex:
(D  0
  THEN  D  0
  THEN  Auto
  THEN  Unfold  `local-simulation-class`  -1
  THEN  (RWO  "parallel-bag-classrel"  (-1)  THENA  Auto)
  THEN  SqExRepD)

---

Home Index