Nuprl Definition : rel-path
rel-path(R;L) == ∀i:ℕ||L|| - 1. (L[i] R L[i + 1])
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
infix_ap: x f y,
all: ∀x:A. B[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
subtract: n - m,
length: ||as||,
infix_ap: x f y,
select: L[n],
add: n + m,
natural_number: $n
FDL editor aliases :
rel-path
Latex:
rel-path(R;L) == \mforall{}i:\mBbbN{}||L|| - 1. (L[i] R L[i + 1])
Date html generated:
2016_05_14-PM-03_52_48
Last ObjectModification:
2015_09_22-PM-06_01_47
Theory : relations2
Home
Index