Nuprl Definition : causal-invariant
causal-invariant(i,L.P[i; L];a,b,L1,L2.R[a; b; L1; L2]) ==
λes.∀e:E
(es-local-property(i,L.P[i; L];es;e)
⇒ (∃e':E. ((e' < e) ∧ es-local-relation(i,j,L1,L2.R[i; j; L1; L2];es;e';e))))
Definitions occuring in Statement :
es-local-relation: es-local-relation(i,j,L1,L2.R[i; j; L1; L2];es;e1;e2),
es-local-property: es-local-property(i,L.P[i; L];es;e),
es-causl: (e < e'),
es-E: E,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
lambda: λx.A[x]
FDL editor aliases :
causal-invariant
causal-invariant(i,L.P[i; L];a,b,L1,L2.R[a; b; L1; L2]) ==
\mlambda{}es.\mforall{}e:E
(es-local-property(i,L.P[i; L];es;e)
{}\mRightarrow{} (\mexists{}e':E. ((e' < e) \mwedge{} es-local-relation(i,j,L1,L2.R[i; j; L1; L2];es;e';e))))
Date html generated:
2015_07_17-PM-00_12_47
Last ObjectModification:
2014_08_07-PM-06_44_26
Home
Index