---

tree-flow{i:l}(es;X;f) ==
  (x,y:E(X).
     ((((f x) = x))
      (((f y) = y))
      (loc(f x) = loc(f y))
      (loc(x) = loc(y))))
   (R:Id  Id  
      (Trans(Id;i,j.R[i;j])
       Irrefl(Id;i,j.R[i;j])
       (x:E(X). ((((f x) = x))  R[loc(f x);loc(x)]))))

---

Definitions :  exists: x:A. B[x],  function: x:A  B[x],  prop: ,  trans: Trans(T;x,y.E[x; y]),  and: P  Q,  irrefl: Irrefl(T;x,y.E[x; y]),  Id: Id,  all: x:A. B[x],  es-E-interface: E(X),  implies: P  Q,  not: A,  equal: s = t,  es-E: E,  so_apply: x[s1;s2],  apply: f a,  es-loc: loc(e)
FDL editor aliases :  tree-flow

---

tree-flow\{i:l\}(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{}  (\mexists{}R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  \mBbbP{}
            (Trans(Id;i,j.R[i;j])
            \mwedge{}  Irrefl(Id;i,j.R[i;j])
            \mwedge{}  (\mforall{}x:E(X).  ((\mneg{}((f  x)  =  x))  {}\mRightarrow{}  R[loc(f  x);loc(x)]))))


Date html generated: 2010_08_27-PM-02_09_11
Last ObjectModification: 2009_12_16-AM-01_32_41

Home Index