---

Step * 2 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. ¬↑has-header-and-in-locs(info(e);hdr;locs)
12. LocalClass(X)
13. v : T
14. i : Id
15. i ↓∈ locs
16. v ↓∈ if test-msg-header-and-loc(info(e);hdr;i)
then let Infos = base-process-inputs(i;hdr;es;e) in
         X list-eo(Infos;i) (||Infos|| - 1)
else {}
fi 
⊢ False
BY
{ BagMemberD (-1) }

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. ↑test-msg-header-and-loc(info(e);hdr;i)
17. v ↓∈ let Infos = base-process-inputs(i;hdr;es;e) in
             X list-eo(Infos;i) (||Infos|| - 1)
⊢ False

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. LocalClass(X)
13. v : T
14. i : Id
15. i ↓∈ locs
16. ¬↑test-msg-header-and-loc(info(e);hdr;i)
17. v ↓∈ {}
⊢ 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.  LocalClass(X)
13.  v  :  T
14.  i  :  Id
15.  i  \mdownarrow{}\mmember{}  locs
16.  v  \mdownarrow{}\mmember{}  if  test-msg-header-and-loc(info(e);hdr;i)
then  let  Infos  =  base-process-inputs(i;hdr;es;e)  in
                  X  list-eo(Infos;i)  (||Infos||  -  1)
else  \{\}
fi 
\mvdash{}  False


By

---

Latex:
BagMemberD  (-1)

---

Home Index