Nuprl Lemma : cond_equiv_to_causl
∀es:EO
∀[R:E ⟶ E ⟶ ℙ]. ∀[P:E ⟶ ℙ].
(R => λe,e'. (e < e')
⇒ (∀x,y:E. (((P x) ∧ (P y)) ⇒ (((R x y) ∨ (x = y ∈ E)) ∨ (R y x))))
⇒ (∀x,y:E. (((P x) ∧ (P y)) ⇒ (R x y ⇐⇒ (x < y)))))
Proof
Definitions occuring in Statement :
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
rel_implies: R1 => R2,
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
and: P ∧ Q,
iff: P ⇐⇒ Q,
cand: A c∧ B,
es-causl: (e < e'),
squash: ↓T,
rev_implies: P ⇐ Q,
trans: Trans(T;x,y.E[x; y]),
guard: {T},
not: ¬A,
false: False
Latex:
\mforall{}es:EO
\mforall{}[R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}]. \mforall{}[P:E {}\mrightarrow{} \mBbbP{}].
(R => \mlambda{}e,e'. (e < e')
{}\mRightarrow{} (\mforall{}x,y:E. (((P x) \mwedge{} (P y)) {}\mRightarrow{} (((R x y) \mvee{} (x = y)) \mvee{} (R y x))))
{}\mRightarrow{} (\mforall{}x,y:E. (((P x) \mwedge{} (P y)) {}\mRightarrow{} (R x y \mLeftarrow{}{}\mRightarrow{} (x < y)))))
Date html generated:
2016_05_16-AM-10_34_28
Last ObjectModification:
2016_01_17-PM-01_21_52
Theory : new!event-ordering
Home
Index