Nuprl Definition : tree-flow

tree-flow{i:l}(es;X;f) ==
  (∀x,y:E(X).  ((¬((f x) = x ∈ E(X))) ⇒ (¬((f y) = y ∈ E(X))) ⇒ (loc(f x) = loc(f y) ∈ Id) ⇒ (loc(x) = loc(y) ∈ Id)))
  ∧ (∃R:Id ─→ Id ─→ ℙ
      (Trans(Id;i,j.R[i;j]) ∧ Irrefl(Id;i,j.R[i;j]) ∧ (∀x:E(X). ((¬((f x) = x ∈ E)) ⇒ R[loc(f x);loc(x)]))))


Definitions occuring in Statement :  es-E-interface: E(X),  es-loc: loc(e),  es-E: E,  Id: Id,  irrefl: Irrefl(T;x,y.E[x; y]),  trans: Trans(T;x,y.E[x; y]),  prop: ℙ,  so_apply: x[s1;s2],  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q,  apply: f a,  function: x:A ─→ B[x],  equal: s = t ∈ T
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: 2015_07_17-PM-00_59_20
Last ObjectModification: 2012_02_25-PM-01_31_44

Home Index