Nuprl Lemma : loc-ordered-equality
∀es:EO. ∀as,bs:E List.
(loc-ordered(es;as) ⇒ loc-ordered(es;bs) ⇒ (as = bs ∈ (E List) ⇐⇒ ∀e:E. ((e ∈ as) ⇐⇒ (e ∈ bs))))
Proof
Definitions occuring in Statement :
loc-ordered: loc-ordered(es;L),
es-E: E,
event_ordering: EO,
l_member: (x ∈ l),
list: T List,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
equal: s = t ∈ T
Lemmas :
es-locl_wf,
pes-axioms,
es-locl_irreflexivity
\mforall{}es:EO. \mforall{}as,bs:E List.
(loc-ordered(es;as) {}\mRightarrow{} loc-ordered(es;bs) {}\mRightarrow{} (as = bs \mLeftarrow{}{}\mRightarrow{} \mforall{}e:E. ((e \mmember{} as) \mLeftarrow{}{}\mRightarrow{} (e \mmember{} bs))))
Date html generated:
2015_07_17-AM-08_36_34
Last ObjectModification:
2015_01_27-PM-02_58_07
Home
Index