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
Latex:
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:
2016_05_16-PM-10_16_33
Last ObjectModification:
2012_02_25-PM-01_31_44
Theory : event-ordering
Home
Index