---

convergent-flow(es;X;f) ==
  (x,y:E(X).
     ((((f x) = x))
      (((f y) = y))
      (loc(f x) = loc(f y))
      (loc(x) = loc(y))))
   (x,y:E(X).  (x is f*(y)  ((x = y))  ((loc(x) = loc(y)))))

---

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

---

convergent-flow(es;X;f)  ==
    (\mforall{}x,y:E(X).    ((\mneg{}((f  x)  =  x))  {}\mRightarrow{}  (\mneg{}((f  y)  =  y))  {}\mRightarrow{}  (loc(f  x)  =  loc(f  y))  {}\mRightarrow{}  (loc(x)  =  loc(y))))
    \mwedge{}  (\mforall{}x,y:E(X).    (x  is  f*(y)  {}\mRightarrow{}  (\mneg{}(x  =  y))  {}\mRightarrow{}  (\mneg{}(loc(x)  =  loc(y)))))


Date html generated: 2010_08_27-PM-02_09_00
Last ObjectModification: 2009_12_16-AM-01_32_30

Home Index