Step
*
of Lemma
eclass1-base-classrel
∀[T,C:Type]. ∀[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[v:C]. ∀[hdr:Name]. ∀[g:Id ─→ T ─→ C].
uiff(v ∈ (g o Base(hdr))(e);(header(e) = hdr ∈ Name) ∧ has-es-info-type(es;e;f;T) ∧ (v = (g loc(e) msgval(e)) ∈ C))
supposing hdr encodes T
BY
{ (Intros
THEN (Unhide THENA Auto)
THEN (RWO "eclass1-classrel" 0 THENA Auto)
THEN RepeatFor 6 ((RW (HigherC ClassRelStepC) 0 THENA Auto))
THEN Auto) }
Latex:
Latex:
\mforall{}[T,C:Type]. \mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[es:EO+(Message(f))]. \mforall{}[e:E]. \mforall{}[v:C]. \mforall{}[hdr:Name].
\mforall{}[g:Id {}\mrightarrow{} T {}\mrightarrow{} C].
uiff(v \mmember{} (g o Base(hdr))(e);(header(e) = hdr)
\mwedge{} has-es-info-type(es;e;f;T)
\mwedge{} (v = (g loc(e) msgval(e))))
supposing hdr encodes T
By
Latex:
(Intros
THEN (Unhide THENA Auto)
THEN (RWO "eclass1-classrel" 0 THENA Auto)
THEN RepeatFor 6 ((RW (HigherC ClassRelStepC) 0 THENA Auto))
THEN Auto)
Home
Index