---

Step * of Lemma local-simulation-classrel

∀[f:Name ─→ Type]. ∀[Info,T:Type]. ∀[X:EClass(T)].
  ∀locs:bag(Id). ∀hdr:Name.
    ∀es:EO+(Message(f)). ∀e:E.
      ∀[v:T]
        uiff(v ∈ local-simulation-class(X;locs;hdr)(e);(↑has-header-and-in-locs(info(e);hdr;locs))
        ∧ v ∈ X(local-simulation-event(es;e;hdr;locs))) 
      supposing LocalClass(X) 
    supposing hdr encodes Id × Info
BY
{ (InstLemma `local-simulation-class_wf` []
   THEN RepeatFor 6 (ParallelLast')
   THEN Intro
   THEN (D -2 THENA Auto)
   THEN Intros
   THEN (BoolCase ⌈has-header-and-in-locs(info(e);hdr;locs)⌉⋅ 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)
⊢ uiff(v ∈ local-simulation-class(X;locs;hdr)(e);True ∧ v ∈ X(local-simulation-event(es;e;hdr;locs)))

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. ¬↑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)))

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].
    \mforall{}locs:bag(Id).  \mforall{}hdr:Name.
        \mforall{}es:EO+(Message(f)).  \mforall{}e:E.
            \mforall{}[v:T]
                uiff(v  \mmember{}  local-simulation-class(X;locs;hdr)(e);(\muparrow{}has-header-and-in-locs(info(e);hdr;locs))
                \mwedge{}  v  \mmember{}  X(local-simulation-event(es;e;hdr;locs))) 
            supposing  LocalClass(X) 
        supposing  hdr  encodes  Id  \mtimes{}  Info


By

---

Latex:
(InstLemma  `local-simulation-class\_wf`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  Intro
  THEN  (D  -2  THENA  Auto)
  THEN  Intros
  THEN  (BoolCase  \mkleeneopen{}has-header-and-in-locs(info(e);hdr;locs)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index