Nuprl Definition : causal-weak-predecessor

causal-weak-predecessor(es;p) ==  ∀e:E. ((↑can-apply(p;e)) ⇒ do-apply(p;e) c≤ e)


Definitions occuring in Statement :  es-causle: e c≤ e',  es-E: E,  assert: ↑b,  all: ∀x:A. B[x],  implies: P ⇒ Q,  do-apply: do-apply(f;x),  can-apply: can-apply(f;x)
FDL editor aliases :  causal-weak-predecessor causal-weak-predecessor
Latex:
causal-weak-predecessor(es;p)  ==    \mforall{}e:E.  ((\muparrow{}can-apply(p;e))  {}\mRightarrow{}  do-apply(p;e)  c\mleq{}  e)


Date html generated: 2016_05_16-AM-10_29_15
Last ObjectModification: 2013_03_25-PM-01_58_15

Theory : new!event-ordering


Home Index