Nuprl Definition : squash-causal-invariant
squash-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],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
lambda: λx.A[x]
FDL editor aliases :
squash-causal-invariant
squash-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{} (\mdownarrow{}\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_58
Last ObjectModification:
2014_08_12-AM-11_11_18
Home
Index