Nuprl Lemma : es-interface-predecessors_wf

[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].  (≤(X)(e) ∈ {a:E(X)| loc(a) loc(e) ∈ Id}  List)


Proof




Definitions occuring in Statement :  es-interface-predecessors: (X)(e) es-E-interface: E(X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-loc: loc(e) es-E: E Id: Id list: List uall: [x:A]. B[x] top: Top member: t ∈ T set: {x:A| B[x]}  universe: Type equal: t ∈ T
Lemmas :  es-E_wf event-ordering+_subtype eclass_wf top_wf event-ordering+_wf filter_type Id_wf es-loc_wf in-eclass_wf es-le-before_wf subtype_rel_list_set es-E-interface_wf assert_wf subtype_rel_nested_set2 equal_wf subtype_rel_sets set_wf

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].    (\mleq{}(X)(e)  \mmember{}  \{a:E(X)|  loc(a)  =  loc(e)\}    List\000C)



Date html generated: 2015_07_20-PM-03_41_51
Last ObjectModification: 2015_01_27-PM-10_13_13

Home Index