Nuprl Lemma : decidable__exists-classrel-between1

`∀[Info,T:Type].  ∀X:EClass(T). ∀es:EO+(Info). ∀e1,e2:E.  Dec(∃e:E. (e1 ≤loc e  ∧ (e <loc e2) ∧ (↓∃v:T. v ∈ X(e))))`

Proof

Definitions occuring in Statement :  classrel: `v ∈ X(e)` eclass: `EClass(A[eo; e])` event-ordering+: `EO+(Info)` es-le: `e ≤loc e' ` es-locl: `(e <loc e')` es-E: `E` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` squash: `↓T` and: `P ∧ Q` universe: `Type`
Lemmas :  decidable__equal_Id es-loc_wf es-E_wf event-ordering+_subtype event-ordering+_wf eclass_wf equal_wf decidable__exists_classrel classrel_wf exists_wf squash_wf Id_wf decidable__existse-between1 not_wf es-locl_wf es-le_wf es-le-loc
\mforall{}[Info,T:Type].
\mforall{}X:EClass(T).  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.    Dec(\mexists{}e:E.  (e1  \mleq{}loc  e    \mwedge{}  (e  <loc  e2)  \mwedge{}  (\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))))

Date html generated: 2015_07_17-PM-00_18_09
Last ObjectModification: 2015_07_16-AM-09_44_25

Home Index