---

x-f*-y goes thru i last ==
  e:E(Sys). (((loc(e) = i)  ((loc(f e) = loc(e))))  e is f*(y)  x is f*(e))

---

Definitions :  exists: x:A. B[x],  not: A,  equal: s = t,  Id: Id,  apply: f a,  es-loc: loc(e),  and: P  Q,  fun-connected: y is f*(x),  es-E-interface: E(X)
FDL editor aliases :  path-goes-thru-last

---

x-f*-y  goes  thru  i  last  ==
    \mexists{}e:E(Sys).  (((loc(e)  =  i)  \mwedge{}  (\mneg{}(loc(f  e)  =  loc(e))))  \mwedge{}  e  is  f*(y)  \mwedge{}  x  is  f*(e))


Date html generated: 2010_08_27-PM-03_22_39
Last ObjectModification: 2009_12_16-AM-08_58_22

Home Index