### Nuprl Lemma : decidable__exists-classrel-between3-sv

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

Proof

Definitions occuring in Statement :  single-valued-classrel: `single-valued-classrel(es;X;T)` 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]` implies: `P `` Q` and: `P ∧ Q` universe: `Type`
Lemmas :  decidable__exists-classrel-between3 es-E_wf event-ordering+_subtype single-valued-classrel_wf event-ordering+_wf eclass_wf decidable__exists-single-valued-classrel es-locl_wf es-le_wf exists_wf classrel_wf not_wf squash_wf
\mforall{}[Info,T:Type].
\mforall{}X:EClass(T).  \mforall{}es:EO+(Info).
(single-valued-classrel(es;X;T)
{}\mRightarrow{}  (\mforall{}e1,e2:E.    Dec(\mexists{}e:E.  ((e1  <loc  e)  \mwedge{}  e  \mleq{}loc  e2    \mwedge{}  (\mexists{}v:T.  v  \mmember{}  X(e))))))

Date html generated: 2015_07_17-PM-00_22_37
Last ObjectModification: 2015_01_27-PM-11_38_56

Home Index