---

Step * 1 of Lemma constrained-msg-interface-valueall-type


1. f : Name ─→ Type
2. locs : Id List
3. hdrs : Name List
4. (∀h∈hdrs.valueall-type(f h))
5. m1 : ℤ@i
6. m3 : Id@i
7. m5 : 𝔹@i
8. h : Name@i
9. m7 : f h@i
10. \\%2 : (<m1, m3, m5, h, m7>.dst ∈ locs) ∧ (h ∈ hdrs)@i
11. valueall-type(f h)
⊢ (evalall(<m1, m3, m5, h, m7>))↓
BY
{ ((RWW "evalall-pair" 0 THENA Auto)
   THEN (CallByValueReduce 0 THENA (Fold `has-valueall` 0 THEN Auto))
   THEN (CallByValueReduceOn ⌈evalall(m3)⌉ 0⋅ THENA (Fold `has-valueall` 0 THEN Auto))
   THEN (CallByValueReduceOn ⌈evalall(m5)⌉ 0⋅ THENA (Fold `has-valueall` 0 THEN Auto))) }

1
1. f : Name ─→ Type
2. locs : Id List
3. hdrs : Name List
4. (∀h∈hdrs.valueall-type(f h))
5. m1 : ℤ@i
6. m3 : Id@i
7. m5 : 𝔹@i
8. h : Name@i
9. m7 : f h@i
10. \\%2 : (<m1, m3, m5, h, m7>.dst ∈ locs) ∧ (h ∈ hdrs)@i
11. valueall-type(f h)
⊢ (eval y' = eval y' = eval y' = eval x' = evalall(h) in
                                 eval y' = evalall(m7) in
                                   <x', y'> in
                       <evalall(m5), y'> in
             <evalall(m3), y'> in
   <evalall(m1), y'>)↓

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  locs  :  Id  List
3.  hdrs  :  Name  List
4.  (\mforall{}h\mmember{}hdrs.valueall-type(f  h))
5.  m1  :  \mBbbZ{}@i
6.  m3  :  Id@i
7.  m5  :  \mBbbB{}@i
8.  h  :  Name@i
9.  m7  :  f  h@i
10.  \mbackslash{}\mbackslash{}\%2  :  (<m1,  m3,  m5,  h,  m7>.dst  \mmember{}  locs)  \mwedge{}  (h  \mmember{}  hdrs)@i
11.  valueall-type(f  h)
\mvdash{}  (evalall(<m1,  m3,  m5,  h,  m7>))\mdownarrow{}


By

---

Latex:
((RWW  "evalall-pair"  0  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  (Fold  `has-valueall`  0  THEN  Auto))
  THEN  (CallByValueReduceOn  \mkleeneopen{}evalall(m3)\mkleeneclose{}  0\mcdot{}  THENA  (Fold  `has-valueall`  0  THEN  Auto))
  THEN  (CallByValueReduceOn  \mkleeneopen{}evalall(m5)\mkleeneclose{}  0\mcdot{}  THENA  (Fold  `has-valueall`  0  THEN  Auto)))

---

Home Index