Nuprl Lemma : loc-ordered-filter
∀es:EO. ∀as:E List. (loc-ordered(es;as) ⇒ (∀P:{e:E| (e ∈ as)} ─→ 𝔹. loc-ordered(es;filter(P;as))))
Proof
Definitions occuring in Statement :
loc-ordered: loc-ordered(es;L),
es-E: E,
event_ordering: EO,
l_member: (x ∈ l),
filter: filter(P;l),
list: T List,
bool: 𝔹,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ─→ B[x]
Lemmas :
list-subtype,
l_before_wf,
filter_wf5,
es-E_wf,
l_member_wf,
bool_wf,
loc-ordered_wf,
list_wf,
event_ordering_wf,
l_before-filter
\mforall{}es:EO. \mforall{}as:E List. (loc-ordered(es;as) {}\mRightarrow{} (\mforall{}P:\{e:E| (e \mmember{} as)\} {}\mrightarrow{} \mBbbB{}. loc-ordered(es;filter(P;as)))\000C)
Date html generated:
2015_07_17-AM-08_36_36
Last ObjectModification:
2015_01_27-PM-02_58_16
Home
Index