### Nuprl Lemma : last-decidable

`∀es:EO. ∀e:E.`
`  ∀[P:{a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ]`
`    ((∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a]))`
`    `` (∀e'≤e.P[e'] `⇐⇒` P[e] ∨ ∃e'≤e.(¬(P[e'] `⇐⇒` P[e])) ∧ ∀e''∈(e',e].P[e''] `⇐⇒` P[e]))`

Proof

Definitions occuring in Statement :  alle-between3: `∀e∈(e1,e2].P[e]` alle-le: `∀e≤e'.P[e]` existse-le: `∃e≤e'.P[e]` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  all_wf Id_wf es-loc_wf decidable_wf es-E_wf event_ordering_wf btrue_wf bfalse_wf equal_wf set_wf iff_wf bool_wf equal-wf-base btrue_neq_bfalse ppcc-problem unit_wf2 iff_imp_equal_bool true_wf false_wf iff_weakening_equal last-transition exists_wf es-le_wf not_wf es-le-loc es-locl_wf
\mforall{}es:EO.  \mforall{}e:E.
\mforall{}[P:\{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}]
((\mforall{}a:\{a:E|  loc(a)  =  loc(e)\}  .  Dec(P[a]))
{}\mRightarrow{}  (\mforall{}e'\mleq{}e.P[e']  \mLeftarrow{}{}\mRightarrow{}  P[e]  \mvee{}  \mexists{}e'\mleq{}e.(\mneg{}(P[e']  \mLeftarrow{}{}\mRightarrow{}  P[e]))  \mwedge{}  \mforall{}e''\mmember{}(e',e].P[e'']  \mLeftarrow{}{}\mRightarrow{}  P[e]))

Date html generated: 2015_07_17-AM-08_51_12
Last ObjectModification: 2015_02_04-PM-05_56_25

Home Index