| | Some definitions of interest. |
|
| ma-compat | Def A ||+ B == A || B & ma-frame-compatible(A; B) & ma-sframe-compatible(A; B) |
|
| Id | Def Id == Atom  |
| | | Thm* Id  Type |
|
| fpf-compatible | Def f || g ==  x:A.  x dom(f) & x dom(g)   f(x) = g(x) B(x) |
|
| ma-single-frame | Def only members of L affect x :t == mk-ma(x : t; ; ; ; ; ; x : L; ) |
|
| ma-single-init | Def x : t initially x = v == mk-ma(x : t; ; x : v; ; ; ; ; ) |
|
| fpf-single | Def x : v == <[x], x.v> |
|
| id-deq | Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq) |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
