---

Step * 1 1 1 1 of Lemma local-simulation-classrel

.....truecase..... 
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
20. i ↓∈ locs
21. v ↓∈ let Infos = base-process-inputs(i;hdr;es;e) in
             X list-eo(Infos;i) (||Infos|| - 1)
22. ↑test-msg-header-and-loc(info(e);hdr;i)
⊢ v ∈ X(e1)
BY
{ (RepUR ``classrel`` 0 THEN NthHypEq (-2) THEN EqCD THEN Auto) }

1
.....subterm..... T:t
3:n
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
20. i ↓∈ locs
21. v ↓∈ let Infos = base-process-inputs(i;hdr;es;e) in
             X list-eo(Infos;i) (||Infos|| - 1)
22. ↑test-msg-header-and-loc(info(e);hdr;i)
⊢ (X local-simulation-eo(es;e;hdr;locs) e1)
= let Infos = base-process-inputs(i;hdr;es;e) in
      X list-eo(Infos;i) (||Infos|| - 1)
∈ bag(T)

---

Latex:

---

Latex:
.....truecase..... 
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.  LocalClass(X)
12.  v  :  T
13.  msg-header(info(e))  =  hdr
14.  fst(msg-body(info(e)))  \mdownarrow{}\mmember{}  locs
15.  local-simulation-eo(es;e;hdr;locs)  \mmember{}  EO+(Info)
16.  local-simulation-event(es;e;hdr;locs)  \mmember{}  E
17.  e1  :  E@i
18.  local-simulation-event(es;e;hdr;locs)  =  e1@i
19.  i  :  Id
20.  i  \mdownarrow{}\mmember{}  locs
21.  v  \mdownarrow{}\mmember{}  let  Infos  =  base-process-inputs(i;hdr;es;e)  in
                          X  list-eo(Infos;i)  (||Infos||  -  1)
22.  \muparrow{}test-msg-header-and-loc(info(e);hdr;i)
\mvdash{}  v  \mmember{}  X(e1)


By

---

Latex:
(RepUR  ``classrel``  0  THEN  NthHypEq  (-2)  THEN  EqCD  THEN  Auto)

---

Home Index