Nuprl Definition : rel-path-between
rel-path-between(T;R;x;y;L) == rel-path(R;L) ∧ 0 < ||L|| ∧ (x = hd(L) ∈ T) ∧ (y = last(L) ∈ T)
Definitions occuring in Statement :
rel-path: rel-path(R;L),
last: last(L),
hd: hd(l),
length: ||as||,
less_than: a < b,
and: P ∧ Q,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
rel-path: rel-path(R;L),
less_than: a < b,
natural_number: $n,
length: ||as||,
and: P ∧ Q,
hd: hd(l),
equal: s = t ∈ T,
last: last(L)
FDL editor aliases :
rel-path-between
Latex:
rel-path-between(T;R;x;y;L) == rel-path(R;L) \mwedge{} 0 < ||L|| \mwedge{} (x = hd(L)) \mwedge{} (y = last(L))
Date html generated:
2016_05_14-PM-03_52_50
Last ObjectModification:
2015_09_22-PM-06_01_48
Theory : relations2
Home
Index