| Some definitions of interest. |
|
da-outlinks | Def da-outlinks(da;i)
Def == mapfilter( k.da-outlink-f(da;k); k.has-src(i;k);fpf-dom-list(da)) |
|
IdLnk | Def IdLnk == Id Id  |
| | Thm* IdLnk Type |
|
Id | Def Id == Atom  |
| | Thm* Id Type |
|
fpf-empty | Def == <nil, x. > |
|
l_member | Def (x l) == i: . i<||l|| & x = l[i] T |
| | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
mapfilter | Def mapfilter(f;P;L) == map(f;filter(P;L)) |
| | Thm* T:Type, P:(T  ), T':Type, f:({x:T| P(x) } T'), L:T List.
Thm* mapfilter(f;P;L) T' List |