Nuprl Definition : causal_order
causal_order(L;R;P;Q) == ∀i:ℕ||L||. ((Q i) ⇒ (∃j:ℕ||L||. (((j ≤ i) ∧ (P j)) ∧ (R j i))))
Definitions occuring in Statement :
length: ||as||,
int_seg: {i..j-},
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
and: P ∧ Q,
le: A ≤ B,
apply: f a
FDL editor aliases :
causal_order
Latex:
causal\_order(L;R;P;Q) == \mforall{}i:\mBbbN{}||L||. ((Q i) {}\mRightarrow{} (\mexists{}j:\mBbbN{}||L||. (((j \mleq{} i) \mwedge{} (P j)) \mwedge{} (R j i))))
Date html generated:
2016_05_15-PM-02_03_23
Last ObjectModification:
2015_09_23-AM-07_37_39
Theory : list!
Home
Index