Nuprl Definition : ds-agrees
ds-agrees(ds;x.T[x]) == ∀x:Id. ((↑x ∈ dom(ds)) ⇒ T[x] ≡ ds(x))
Definitions occuring in Statement :
fpf-ap: f(x),
fpf-dom: x ∈ dom(f),
id-deq: IdDeq,
Id: Id,
assert: ↑b,
ext-eq: A ≡ B,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
ds-agrees
Latex:
ds-agrees(ds;x.T[x]) == \mforall{}x:Id. ((\muparrow{}x \mmember{} dom(ds)) {}\mRightarrow{} T[x] \mequiv{} ds(x))
Date html generated:
2016_05_16-AM-11_41_39
Last ObjectModification:
2012_02_25-AM-11_15_52
Theory : event-ordering
Home
Index