Nuprl Definition : path-goes-thru-last
x-f*-y goes thru i last == ∃e:E(Sys). (((loc(e) = i ∈ Id) ∧ (¬(loc(f e) = loc(e) ∈ Id))) ∧ e is f*(y) ∧ x is f*(e))
Definitions occuring in Statement :
es-E-interface: E(X),
es-loc: loc(e),
Id: Id,
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T,
fun-connected: y is f*(x)
FDL editor aliases :
path-goes-thru-last
Latex:
x-f*-y goes thru i last ==
\mexists{}e:E(Sys). (((loc(e) = i) \mwedge{} (\mneg{}(loc(f e) = loc(e)))) \mwedge{} e is f*(y) \mwedge{} x is f*(e))
Date html generated:
2015_07_21-PM-04_17_15
Last ObjectModification:
2012_02_25-PM-03_09_31
Home
Index