Nuprl Lemma : CLK_main_wf

[MsgType:ValueAllType]. ∀[locs:bag(Id)]. ∀[reply:Id ─→ MsgType ─→ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
  (CLK_main(MsgType;locs;reply;f) ∈ EClass(Interface))


Proof




Definitions occuring in Statement :  CLK_main: CLK_main(MsgType;locs;reply;f) CLK_headers_type: CLK_headers_type{i:l}(MsgType) msg-interface: Interface Message: Message(f) eclass: EClass(A[eo; e]) Id: Id vatype: ValueAllType uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] product: x:A × B[x] bag: bag(T)
Lemmas :  int_seg_wf length_wf name_wf CLK_headers_wf l_all_iff l_member_wf equal_wf CLK_headers_fun_wf cons_wf_listp cons_wf nil_wf listp_wf cons_member iff_weakening_equal subtype_rel_dep_function vatype_wf class-at_wf Message_wf msg-interface_wf CLK_Reply_wf CLK_headers_type_wf bag_wf Id_wf set_wf valueall-type_wf

Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[locs:bag(Id)].  \mforall{}[reply:Id  {}\mrightarrow{}  MsgType  {}\mrightarrow{}  (MsgType  \mtimes{}  Id)].
\mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].
    (CLK\_main(MsgType;locs;reply;f)  \mmember{}  EClass(Interface))



Date html generated: 2015_07_23-PM-04_10_05
Last ObjectModification: 2015_02_04-PM-02_01_49

Home Index