---

Step * 1 1 1 1 1 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. 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. msg-body(info(e)) ∈ Id × Info
⊢ (X local-simulation-eo(es;e;hdr;locs) local-simulation-event(es;e;hdr;locs))
= let Infos = base-process-inputs(fst(msg-body(info(e)));hdr;es;e) in
      X list-eo(Infos;fst(msg-body(info(e)))) (||Infos|| - 1)
∈ bag(T)
BY
{ ((InstLemma `base-process-inputs_wf` [⌈f⌉;⌈Info⌉;⌈T⌉;⌈X⌉;⌈fst(msg-body(info(e)))⌉;⌈hdr⌉;⌈es⌉;⌈e⌉]⋅ THENA Auto)
   THEN (InstLemma `base-process-inputs-non-null` [⌈f⌉;⌈Info⌉;⌈T⌉;⌈X⌉;⌈fst(msg-body(info(e)))⌉;⌈hdr⌉;⌈es⌉;⌈e⌉]⋅
         THENA (Auto THEN RWO "assert-test-msg-header-and-loc" 0 THEN Auto)
         )
   THEN RepUR ``let`` 0
   THEN Fold `class-ap` 0
   THEN BLemma `local-class-output-agree2`
   THEN Try (BLemma `list-eo-E`)
   THEN Try (CompleteAuto)) }

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. 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. msg-body(info(e)) ∈ Id × Info
18. base-process-inputs(fst(msg-body(info(e)));hdr;es;e) ∈ Info List
19. 0 < ||base-process-inputs(fst(msg-body(info(e)));hdr;es;e)||
⊢ loc(local-simulation-event(es;e;hdr;locs)) = loc(||base-process-inputs(fst(msg-body(info(e)));hdr;es;e)|| - 1) ∈ Id

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. 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. msg-body(info(e)) ∈ Id × Info
18. base-process-inputs(fst(msg-body(info(e)));hdr;es;e) ∈ Info List
19. 0 < ||base-process-inputs(fst(msg-body(info(e)));hdr;es;e)||
⊢ eo-local-agree(Info;local-simulation-eo(es;e;hdr;locs);list-eo(base-process-inputs(fst(...);hdr;es;e);...);...;... 
- 1)

---

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.  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.  msg-body(info(e))  \mmember{}  Id  \mtimes{}  Info
\mvdash{}  (X  local-simulation-eo(es;e;hdr;locs)  local-simulation-event(es;e;hdr;locs))
=  let  Infos  =  base-process-inputs(fst(msg-body(info(e)));hdr;es;e)  in
            X  list-eo(Infos;fst(msg-body(info(e))))  (||Infos||  -  1)


By

---

Latex:
((InstLemma  `base-process-inputs\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}fst(msg-body(info(e)))\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (InstLemma  `base-process-inputs-non-null`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}fst(msg-body(info(e)))\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};
              \mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RWO  "assert-test-msg-header-and-loc"  0  THEN  Auto)
              )
  THEN  RepUR  ``let``  0
  THEN  Fold  `class-ap`  0
  THEN  BLemma  `local-class-output-agree2`
  THEN  Try  (BLemma  `list-eo-E`)
  THEN  Try  (CompleteAuto))

---

Home Index