---

Step * of Lemma single-valued-base-loc-classrel

∀[f:Name ⟶ Type]. ∀[T:Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v1,v2:T]. ∀[hdr:Name].
  ∀[locs:bag(Id)]. (v1 ∈ Base(hdr;locs)(e) ⇒ v2 ∈ Base(hdr;locs)(e) ⇒ (v1 = v2 ∈ T)) supposing T = (f hdr) ∈ Type
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 (MaUseClassRel (-2)) THEN RepeatFor 2 (MaUseClassRel (-1))) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[T:Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[v1,v2:T].  \mforall{}[hdr:Name].
    \mforall{}[locs:bag(Id)].  (v1  \mmember{}  Base(hdr;locs)(e)  {}\mRightarrow{}  v2  \mmember{}  Base(hdr;locs)(e)  {}\mRightarrow{}  (v1  =  v2)) 
    supposing  T  =  (f  hdr)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  (MaUseClassRel  (-2))  THEN  RepeatFor  2  (MaUseClassRel  (-1)))

---

Home Index