Nuprl Lemma : alle-between3_wf

`∀[es:EO]. ∀[e1,e2:E]. ∀[P:{e:E| (loc(e) = loc(e1) ∈ Id) ∧ (¬↑first(e))}  ─→ ℙ].`
`  ∀e∈(e1,e2].P[e] ∈ ℙ supposing loc(e2) = loc(e1) ∈ Id`

Proof

Definitions occuring in Statement :  alle-between3: `∀e∈(e1,e2].P[e]` es-first: `first(e)` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` not: `¬A` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  all_wf es-E_wf es-locl_wf es-le_wf es-locl-first assert_elim btrue_neq_bfalse assert_wf es-first_wf2 Id_wf es-loc_wf not_wf equal_wf
\mforall{}[es:EO].  \mforall{}[e1,e2:E].  \mforall{}[P:\{e:E|  (loc(e)  =  loc(e1))  \mwedge{}  (\mneg{}\muparrow{}first(e))\}    {}\mrightarrow{}  \mBbbP{}].
\mforall{}e\mmember{}(e1,e2].P[e]  \mmember{}  \mBbbP{}  supposing  loc(e2)  =  loc(e1)

Date html generated: 2015_07_17-AM-08_48_32
Last ObjectModification: 2015_01_27-PM-02_25_14

Home Index