---

ds-agrees(ds;x.T[x]) ==  x:Id. ((x  dom(ds))  T[x]  ds(x))

---

Definitions :  all: x:A. B[x],  Id: Id,  implies: P  Q,  assert: b,  fpf-dom: x  dom(f),  ext-eq: A  B,  fpf-ap: f(x),  id-deq: IdDeq
FDL editor aliases :  ds-agrees

---

ds-agrees(ds;x.T[x])  ==    \mforall{}x:Id.  ((\muparrow{}x  \mmember{}  dom(ds))  {}\mRightarrow{}  T[x]  \mequiv{}  ds(x))


Date html generated: 2010_08_27-AM-12_04_01
Last ObjectModification: 2008_02_27-PM-09_50_20

Home Index