Nuprl Definition : lpath
lpath(p) == ∀i:ℕ||p|| - 1. ((destination(p[i]) = source(p[i + 1]) ∈ Id) ∧ (¬(p[i + 1] = lnk-inv(p[i]) ∈ IdLnk)))
Definitions occuring in Statement :
ldst: destination(l),
lsrc: source(l),
lnk-inv: lnk-inv(l),
IdLnk: IdLnk,
Id: Id,
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
subtract: n - m,
add: n + m,
natural_number: $n,
equal: s = t ∈ T
FDL editor aliases :
lpath
lpath(p) == \mforall{}i:\mBbbN{}||p|| - 1. ((destination(p[i]) = source(p[i + 1])) \mwedge{} (\mneg{}(p[i + 1] = lnk-inv(p[i]))))
Date html generated:
2015_07_17-AM-09_12_30
Last ObjectModification:
2012_02_25-AM-10_53_06
Home
Index