Nuprl Lemma : decidable__exists-last-classrel-between3

`∀[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))`
`         ∧ (∀e'':E. ((e <loc e'') `` e'' ≤loc e2  `` (∀x:T. (¬x ∈ 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]` not: `¬A` squash: `↓T` implies: `P `` Q` and: `P ∧ Q` universe: `Type`
Lemmas :  event-ordering+_subtype es-locl-trichotomy add-zero zero-mul add-mul-special le_wf zero-le-nat primrec-wf2 set_wf not_wf classrel_wf squash_wf es-le_wf exists_wf decidable_wf nat_wf all_wf es-loc_wf Id_wf equal_wf es-locl_wf decidable__exists_classrel es-causl_wf le-add-cancel add-associates add_functionality_wrt_le less-iff-le add-commutes add-swap minus-one-mul minus-minus minus-add condition-implies-le false_wf subtract_wf decidable__lt es-E_wf less_than_wf es-causl-swellfnd es-locl_irreflexivity es-locl_transitivity2 es-le-self iff_weakening_equal es-pred-loc-base es-first_wf2 assert_wf btrue_neq_bfalse assert_elim es-locl-first es-pred_wf es-pred-causl and_wf es-le-pred es-locl_transitivity1 es-pred-locl bool_subtype_base subtype_base_sq es-causl_irreflexivity es-causle_wf es-causle_weakening_eq es-causle_weakening es-causl_transitivity2 es-le_weakening_eq es-causl_weakening es-loc-pred es-pred_property es-le_weakening es-le-loc
\mforall{}[Info,T:Type].
\mforall{}X:EClass(T).  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.
Dec(\mexists{}e:E
((e1  <loc  e)
\mwedge{}  e  \mleq{}loc  e2
\mwedge{}  (\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e))
\mwedge{}  (\mforall{}e'':E.  ((e  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e2    {}\mRightarrow{}  (\mforall{}x:T.  (\mneg{}x  \mmember{}  X(e'')))))))

Date html generated: 2015_07_17-PM-00_18_29
Last ObjectModification: 2015_07_16-AM-09_44_08

Home Index