Nuprl Definition : correct-causal-class-relation

for every in at location s.t. Correct[i] there is an earlier event with info=b  such that R[a; b] ==
  ∀e:E. (Correct[loc(e)]  (∀a:A. (a ∈ X(e)  (↓∃e':E. ((e' < e) ∧ R[a; info(e')])))))

Definitions occuring in Statement :  classrel: v ∈ X(e) es-info: info(e) es-causl: (e < e') es-loc: loc(e) es-E: E all: x:A. B[x] exists: x:A. B[x] squash: T implies:  Q and: P ∧ Q
FDL editor aliases :  correct-causal-class-relation
for  every  a  in  X  at  location  i  s.t.  Correct[i]  there  is  an  earlier  event  with  info=b
  such  that  R[a;  b]  ==
    \mforall{}e:E.  (Correct[loc(e)]  {}\mRightarrow{}  (\mforall{}a:A.  (a  \mmember{}  X(e)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  R[a;  info(e')])))))

Date html generated: 2015_07_17-PM-00_17_32
Last ObjectModification: 2014_08_15-PM-10_39_11

Home Index