---

Step * 1 1 of Lemma local-simulation-inputs_wf


1. f : Name ─→ Type
2. Info : Type
3. es : EO+(Message(f))
4. hdr : Name
5. locs : bag(Id)
6. hdr encodes Id × Info
7. e : E
8. m : Message(f)@i
9. (msg-header(m) = hdr ∈ Name) ∧ fst(msg-body(m)) ↓∈ locs
⊢ msg-body(m) ∈ {i:Id| i ↓∈ locs}  × Info
BY
{ ((D -1 THEN MoveToConcl (-1))
   THEN (GenConcl ⌈msg-body(m) = p ∈ (Id × Info)⌉⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  Info  :  Type
3.  es  :  EO+(Message(f))
4.  hdr  :  Name
5.  locs  :  bag(Id)
6.  hdr  encodes  Id  \mtimes{}  Info
7.  e  :  E
8.  m  :  Message(f)@i
9.  (msg-header(m)  =  hdr)  \mwedge{}  fst(msg-body(m))  \mdownarrow{}\mmember{}  locs
\mvdash{}  msg-body(m)  \mmember{}  \{i:Id|  i  \mdownarrow{}\mmember{}  locs\}    \mtimes{}  Info


By

---

Latex:
((D  -1  THEN  MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}msg-body(m)  =  p\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index