| | Some definitions of interest. |
|
| ma-compat | Def A ||+ B == A || B & ma-frame-compatible(A; B) & ma-sframe-compatible(A; B) |
|
| Knd | Def Knd == (IdLnk Id)+Id |
| | | Thm* Knd  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) |
|
| ma-single-effect | Def ma-single-effect(ds; da; k; x; f) == mk-ma(ds; da; ; ; <k,x> : f; ; ; ) |
|
| ma-single-frame | Def only members of L affect x :t == mk-ma(x : t; ; ; ; ; ; x : L; ) |
|
| fpf-single | Def x : v == <[x], x.v> |
|
| id-deq | Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq) |
|
| l_member | Def (x l) ==  i:. i<||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
