Nuprl Definition : path-goes-thru
x-f*-y thru i == ∃e:E(Sys). ((loc(e) = i ∈ 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],
and: P ∧ Q,
equal: s = t ∈ T,
fun-connected: y is f*(x)
FDL editor aliases :
path-goes-thru
Latex:
x-f*-y thru i == \mexists{}e:E(Sys). ((loc(e) = i) \mwedge{} e is f*(y) \mwedge{} x is f*(e))
Date html generated:
2015_07_21-PM-04_16_35
Last ObjectModification:
2012_02_25-PM-03_09_02
Home
Index