| | Some definitions of interest. |
|
| ma-compat | Def A ||+ B == A || B & ma-frame-compatible(A; B) & ma-sframe-compatible(A; B) |
|
| 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 |
|
| 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-compatible | Def f || g == x:A.  x dom(f) & x dom(g)   f(x) = g(x) B(x) |
|
| id-deq | Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq) |
|
| ma-single-sends | Def ma-single-sends(ds; da; k; l; f) == mk-ma(ds; da; ; ; ; <k,l> : f; ; ) |
|
| not | Def  A == A False |
| | | Thm* A:Prop. (A) Prop |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
