---

Step * 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)
⊢ uiff(v ∈ local-simulation-class(X;locs;hdr)(e);True ∧ v ∈ X(local-simulation-event(es;e;hdr;locs)))
BY
{ ((InstLemma `local-simulation-eo_wf` [⌈f⌉;⌈Info⌉;⌈es⌉;⌈hdr⌉;⌈locs⌉;⌈e⌉]⋅ THENA Auto)
   THEN (InstLemma `local-simulation-event_wf` [⌈f⌉;⌈Info⌉;⌈es⌉;⌈hdr⌉;⌈locs⌉;⌈e⌉]⋅ THENA Auto)
   THEN (GenConclTerm ⌈local-simulation-event(es;e;hdr;locs)⌉⋅ THENA Auto)
   THEN RenameVar `e1' (-2)
   THEN Unfold `local-simulation-class` 0
   THEN (RWO "parallel-bag-classrel" 0 THENA 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. [%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))

---

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)
\mvdash{}  uiff(v  \mmember{}  local-simulation-class(X;locs;hdr)(e);True
\mwedge{}  v  \mmember{}  X(local-simulation-event(es;e;hdr;locs)))


By

---

Latex:
((InstLemma  `local-simulation-eo\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `local-simulation-event\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}local-simulation-event(es;e;hdr;locs)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RenameVar  `e1'  (-2)
  THEN  Unfold  `local-simulation-class`  0
  THEN  (RWO  "parallel-bag-classrel"  0  THENA  Auto))

---

Home Index