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
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
not: ¬A,
implies: P ⇒ Q,
false: False,
prop: ℙ,
and: P ∧ Q,
trans: Trans(T;x,y.E[x; y]),
loc-ordered: loc-ordered(es;L)
Latex:
\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:
2016_05_16-AM-09_18_46
Last ObjectModification:
2015_12_28-PM-09_55_44
Theory : new!event-ordering
Home
Index