Step
*
1
3
of Lemma
member-local-simulation-inputs
1. f : Name ─→ Type@i'
2. [Info] : Type
3. es : EO+(Message(f))@i'
4. hdr : Name@i
5. locs : bag(Id)@i
6. hdr encodes Id × Info
7. e : E@i
8. v : Id × Info@i
9. ∃e':E. (e' ≤loc e ∧ (msg-header(info(e')) = hdr ∈ Name) ∧ fst(v) ↓∈ locs ∧ (v = msg-body(info(e')) ∈ (Id × Info)))@i
⊢ ∃y:Message(f)
((y ∈ map(λe.info(e);≤loc(e))) ∧ ((↑has-header-and-in-locs(y;hdr;locs)) c∧ (v = msg-body(y) ∈ (Id × Info))))
BY
{ ExRepD }
1
1. f : Name ─→ Type@i'
2. [Info] : Type
3. es : EO+(Message(f))@i'
4. hdr : Name@i
5. locs : bag(Id)@i
6. hdr encodes Id × Info
7. e : E@i
8. v : Id × Info@i
9. e' : E@i
10. e' ≤loc e @i
11. msg-header(info(e')) = hdr ∈ Name@i
12. fst(v) ↓∈ locs@i
13. v = msg-body(info(e')) ∈ (Id × Info)@i
⊢ ∃y:Message(f)
((y ∈ map(λe.info(e);≤loc(e))) ∧ ((↑has-header-and-in-locs(y;hdr;locs)) c∧ (v = msg-body(y) ∈ (Id × Info))))
Latex:
Latex:
1. f : Name {}\mrightarrow{} Type@i'
2. [Info] : Type
3. es : EO+(Message(f))@i'
4. hdr : Name@i
5. locs : bag(Id)@i
6. hdr encodes Id \mtimes{} Info
7. e : E@i
8. v : Id \mtimes{} Info@i
9. \mexists{}e':E. (e' \mleq{}loc e \mwedge{} (msg-header(info(e')) = hdr) \mwedge{} fst(v) \mdownarrow{}\mmember{} locs \mwedge{} (v = msg-body(info(e'))))@i
\mvdash{} \mexists{}y:Message(f)
((y \mmember{} map(\mlambda{}e.info(e);\mleq{}loc(e))) \mwedge{} ((\muparrow{}has-header-and-in-locs(y;hdr;locs)) c\mwedge{} (v = msg-body(y))))
By
Latex:
ExRepD
Home
Index