Step
*
of Lemma
base-class-program_wf
∀[f:Name ─→ Type]. ∀[hdr:Name]. ∀[T:Type]. base-class-program(hdr) ∈ LocalClass(Base(hdr)) supposing hdr encodes T
BY
{ (Auto
THEN RepUR ``base-class-program`` 0
THEN MemTypeCD
THEN Auto
THEN Reduce 0
THEN (Assert ⌈hdf-base(v.cond-msg-body(hdr;v))*(map(λx.info(x);before(e)))
= hdf-base(v.cond-msg-body(hdr;v))
∈ hdataflow(Message(f);T)⌉⋅
THENM ((HypSubst' (-1) 0 THENA Auto) THEN RepUR ``hdf-base hdf-ap base-headers-msg-val class-ap`` 0 THEN Auto)
)
THEN GenConclAtAddr [2;2]
THEN Thin (-1)⋅
THEN ListInd (-1)
THEN Reduce 0
THEN Auto
THEN (InstLemma `hdf-base-ap` [⌈Message(f)⌉;⌈T⌉;⌈λ2v.cond-msg-body(hdr;v)⌉;⌈u⌉]⋅ THENA Auto)
THEN HypSubst (-1) 0
THEN Reduce 0
THEN Auto) }
Latex:
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[hdr:Name]. \mforall{}[T:Type].
base-class-program(hdr) \mmember{} LocalClass(Base(hdr)) supposing hdr encodes T
By
Latex:
(Auto
THEN RepUR ``base-class-program`` 0
THEN MemTypeCD
THEN Auto
THEN Reduce 0
THEN (Assert \mkleeneopen{}hdf-base(v.cond-msg-body(hdr;v))*(map(\mlambda{}x.info(x);before(e)))
= hdf-base(v.cond-msg-body(hdr;v))\mkleeneclose{}\mcdot{}
THENM ((HypSubst' (-1) 0 THENA Auto)
THEN RepUR ``hdf-base hdf-ap base-headers-msg-val class-ap`` 0
THEN Auto)
)
THEN GenConclAtAddr [2;2]
THEN Thin (-1)\mcdot{}
THEN ListInd (-1)
THEN Reduce 0
THEN Auto
THEN (InstLemma `hdf-base-ap` [\mkleeneopen{}Message(f)\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}v.cond-msg-body(hdr;v)\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{} THENA Auto)
THEN HypSubst (-1) 0
THEN Reduce 0
THEN Auto)
Home
Index