---

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

∀[f:Name ⟶ Type]. ∀[locs:Id List]. ∀[hdrs:Name List].
  valueall-type(Interface(to locs, with hdrs)) supposing (∀h∈hdrs.valueall-type(f h))
BY
{ (Intros⋅
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (GenConcl ⌜x = mi ∈ Interface(to locs, with hdrs)⌝⋅ THENA Auto)
   THEN ThinVar `x'
   THEN D -1
   THEN RepeatFor 4 (D -2)
   THEN RepUR ``msg-interface-message msg-header msg-msg`` -1
   THEN (Assert valueall-type(f h) BY
               (Unhide THEN Auto THEN D -1 THEN With ⌜i⌝ (D 4)⋅ 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)
⊢ (evalall(<m1, m3, m5, h, m7>))↓

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[locs:Id  List].  \mforall{}[hdrs:Name  List].
    valueall-type(Interface(to  locs,  with  hdrs))  supposing  (\mforall{}h\mmember{}hdrs.valueall-type(f  h))


By

---

Latex:
(Intros\mcdot{}
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}x  =  mi\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `x'
  THEN  D  -1
  THEN  RepeatFor  4  (D  -2)
  THEN  RepUR  ``msg-interface-message  msg-header  msg-msg``  -1
  THEN  (Assert  valueall-type(f  h)  BY
                          (Unhide  THEN  Auto  THEN  D  -1  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  4)\mcdot{}  THEN  Auto)))

---

Home Index