---

Step * of Lemma base-noloc-classrel2

∀[T:Type]. ∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:T]. ∀[hdr:Name].
  uiff(v ∈ Base(hdr)(e);(header(e) = hdr ∈ Name) ∧ (v = msgval(e) ∈ T)) supposing hdr encodes T
BY
{ (Auto
   THEN Try ((BLemma `es-info-type-implies` THEN Auto))
   THEN Try (((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))) }

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 ∈ Base(hdr)(e)
⊢ header(e) = hdr ∈ Name

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. v ∈ Base(hdr)(e)
⊢ v = msgval(e) ∈ T

3
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. header(e) = hdr ∈ Name
9. v = msgval(e) ∈ T
⊢ v ∈ Base(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{}  Base(hdr)(e);(header(e)  =  hdr)  \mwedge{}  (v  =  msgval(e)))  supposing  hdr  encodes  T


By

---

Latex:
(Auto
  THEN  Try  ((BLemma  `es-info-type-implies`  THEN  Auto))
  THEN  Try  (((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