Nuprl Lemma : no-classrel-in-interval_wf

[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[start,e:E].  ((no between start and e) ∈ ℙ)


Definitions occuring in Statement :  no-classrel-in-interval: (no between start and e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E uall: [x:A]. B[x] prop: member: t ∈ T universe: Type
Lemmas :  alle-lt_wf Id_wf es-loc_wf es-le_wf all_wf not_wf classrel_wf eo-forward_wf member-eo-forward-E equal_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[start,e:E].    ((no  X  between  start  and  e)  \mmember{}  \mBbbP{})

Date html generated: 2015_07_17-PM-00_29_41
Last ObjectModification: 2015_01_27-PM-11_31_52

Home Index