---

Step * of Lemma verify-classrel

∀[T:Type]. ∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:T]. ∀[hdr:Name].
  uiff(v ∈ Verify(hdr)(e);(↑es-info-auth(es;e)) ∧ (header(e) = hdr ∈ Name) ∧ v = body(e)) supposing hdr encodes T
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
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)

2
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. (↑es-info-auth(es;e)) ∧ (header(e) = hdr ∈ Name) ∧ v = body(e)
⊢ v ∈ Verify(hdr)(e)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[v:T].  \mforall{}[hdr:Name].
    uiff(v  \mmember{}  Verify(hdr)(e);(\muparrow{}es-info-auth(es;e))  \mwedge{}  (header(e)  =  hdr)  \mwedge{}  v  =  body(e)) 
    supposing  hdr  encodes  T


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index