| 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)) |
|
Kind-deq | Def KindDeq == union-deq(IdLnk Id;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq) |
|
Knd | Def Knd == (IdLnk Id)+Id |
| | Thm* Knd Type |
|
IdLnk | Def IdLnk == Id Id  |
| | Thm* IdLnk Type |
|
Id | Def Id == Atom  |
| | Thm* Id Type |
|
has-src | Def has-src(i;k) == isrcv(k) source(lnk(k)) = i |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
fpf | Def a:A fp-> B(a) == d:A List a:{a:A| (a d) } B(a) |
| | Thm* A:Type, B:(A Type). a:A fp-> B(a) Type |
|
fpf-dom | Def x dom(f) == deq-member(eq;x;1of(f)) |
|
isrcv | Def isrcv(k) == isl(k) |
| | Thm* k:Knd. isrcv(k)  |
|
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 |