Step
*
of Lemma
CLK_msg'base-program_wf
∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)].
  (CLK_msg'base-program(MsgType;f) ∈ LocalClass(CLK_msg'base(MsgType;f)))
BY
{ ProveEmlWfLemma }
Latex:
Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].
    (CLK\_msg'base-program(MsgType;f)  \mmember{}  LocalClass(CLK\_msg'base(MsgType;f)))
By
Latex:
ProveEmlWfLemma
Home
Index