Nuprl Definition : flow-graph

flow-graph(S;T;F;G) ==
∀i,j:Id. ((i ∈ S) ⇒ (j ∈ S) ⇒ (∀s:{s:T List| 0 < ||s||} . ((↑can-apply(F i j;s)) ⇒ (i⟶j)∈G)))

Definitions occuring in Statement : id-graph-edge: (i⟶j)∈G, Id: Id, l_member: (x ∈ l), length: ||as||, list: T List, assert: ↑b, less_than: a < b, all: ∀x:A. B[x], implies: P ⇒ Q, set: {x:A| B[x]} , apply: f a, natural_number: $n, can-apply: can-apply(f;x)
FDL editor aliases : flow-graph flow-graph

Latex:
flow-graph(S;T;F;G) == \mforall{}i,j:Id. ((i \mmember{} S) {}\mRightarrow{} (j \mmember{} S) {}\mRightarrow{} (\mforall{}s:\{s:T List| 0 < ||s||\} . ((\muparrow{}can-apply(F i j;s)) {}\mRightarrow{} (i{}\mrightarrow{}j)\mmember{}G))) Date html generated: 2016_05_16-AM-10_06_11 Last ObjectModification: 2013_03_25-PM-01_54_17 Theory : new!event-ordering Home Index