lpath(p) ==
i:
||p|| - 1
((destination(p[i]) = source(p[i + 1])) 
(
(p[i + 1] = lnk-inv(p[i]))))
Definitions :
all: x:A. B[x],
int_seg: {i..j
},
subtract: n - m,
length: ||as||,
and: P Q,
Id: Id,
ldst: destination(l),
lsrc: source(l),
not: A,
equal: s = t,
IdLnk: IdLnk,
add: n + m,
natural_number: $n,
lnk-inv: lnk-inv(l),
select: l[i]
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:
2010_08_26-PM-11_34_29
Last ObjectModification:
2008_02_27-PM-09_24_18
Home
Index