---

Step * of Lemma base-headers-msg-val-es-sv

∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name].  es-sv-class(es;Base(hdr))
BY
{ (Auto
   THEN RepUR ``es-sv-class base-headers-msg-val`` 0
   THEN Try ((Using [`C',⌜f hdr⌝] (BLemma `bag-size_wf`)⋅ THEN Auto THEN D 0 THEN Auto))
   THEN Auto
   THEN RepUR ``cond-msg-body`` 0
   THEN GenConclAtAddr [1;1;1]
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[hdr:Name].    es-sv-class(es;Base(hdr))


By

---

Latex:
(Auto
  THEN  RepUR  ``es-sv-class  base-headers-msg-val``  0
  THEN  Try  ((Using  [`C',\mkleeneopen{}f  hdr\mkleeneclose{}]  (BLemma  `bag-size\_wf`)\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto))
  THEN  Auto
  THEN  RepUR  ``cond-msg-body``  0
  THEN  GenConclAtAddr  [1;1;1]
  THEN  AutoSplit)

---

Home Index