| | Some definitions of interest. |
|
| da-outlink-f | Def da-outlink-f(da;k) == <lnk(k),tag(k),da(k)> |
|
| Kind-deq | Def KindDeq == union-deq(IdLnk Id;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq) |
|
| Knd | Def Knd == (IdLnkId)+Id |
| | | Thm* Knd  Type |
|
| IdLnk | Def IdLnk == IdId |
| | | Thm* IdLnk Type |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| assert | Def  b == if b True else False fi |
| | | Thm*  b: . b Prop |
|
| fpf | Def a:A fp-> B(a) == d:A Lista:{a:A| (a d) }  B(a) |
| | | Thm* A:Type, B:(AType). 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) |
