---

Step * 1 of Lemma verify-classrel


1. T : Type
2. f : Name ─→ Type
3. es : EO+(Message(f))
4. e : E
5. v : T
6. hdr : Name
7. hdr encodes T
8. v ∈ Verify(hdr)(e)
⊢ (↑es-info-auth(es;e)) ∧ (header(e) = hdr ∈ Name) ∧ v = body(e)
BY
{ (RepUR ``classrel verify-class cond-verify-msg-body cond-msg-body`` (-1)
   THEN (SplitOnHypITE (-1) THENA Auto)
   THEN Try (Complete (BagMemberD (-2)))
   THEN (SplitOnHypITE (-2) THENA Auto)
   THEN BagMemberD (-3)
   THEN Try (Complete ((RWO "msg-has-type-encodes" 0 THEN Auto)))
   THEN All(Folds ``es-header es-info-body``)
   THEN Auto
   THEN (D 0 THEN Auto)
   THEN (RWO "has-es-info-type-is-msg-has-type" 0 THEN Auto)
   THEN (RWO "msg-has-type-encodes" 0 THEN Auto)
   THEN Fold `es-header` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  Name  {}\mrightarrow{}  Type
3.  es  :  EO+(Message(f))
4.  e  :  E
5.  v  :  T
6.  hdr  :  Name
7.  hdr  encodes  T
8.  v  \mmember{}  Verify(hdr)(e)
\mvdash{}  (\muparrow{}es-info-auth(es;e))  \mwedge{}  (header(e)  =  hdr)  \mwedge{}  v  =  body(e)


By

---

Latex:
(RepUR  ``classrel  verify-class  cond-verify-msg-body  cond-msg-body``  (-1)
  THEN  (SplitOnHypITE  (-1)  THENA  Auto)
  THEN  Try  (Complete  (BagMemberD  (-2)))
  THEN  (SplitOnHypITE  (-2)  THENA  Auto)
  THEN  BagMemberD  (-3)
  THEN  Try  (Complete  ((RWO  "msg-has-type-encodes"  0  THEN  Auto)))
  THEN  All(Folds  ``es-header  es-info-body``)
  THEN  Auto
  THEN  (D  0  THEN  Auto)
  THEN  (RWO  "has-es-info-type-is-msg-has-type"  0  THEN  Auto)
  THEN  (RWO  "msg-has-type-encodes"  0  THEN  Auto)
  THEN  Fold  `es-header`  0
  THEN  Auto)

---

Home Index