| | Some definitions of interest. |
|
| Knd | Def Knd == (IdLnk Id)+Id |
| | | Thm* Knd  Type |
|
| ma-state | Def State(ds) == x:Id  ds(x)?Top |
|
| ma-valtype | Def ma-valtype(da; k) == da(k)?Top |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| kindcase | Def kindcase(k;a.f(a);l,t.g(l;t))
Def == if islocal(k) f(act(k)) else g(lnk(k);tag(k)) fi |
| | | Thm*  B:Type, k:Knd, f:(IdB), g:(IdLnkIdB).
Thm* kindcase(k;a.f(a);l,t.g(l,t)) B |
|
| actof | Def act(k) == outr(k) |
| | | Thm* k:Knd. islocal(k)   act(k) Id |
|
| 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-join | Def f  g == <1of(f) @ filter( a.  a dom(f);1of(g)),a.f(a)?g(a)> |
|
| fpf-cap | Def f(x)?z == if x dom(f) f(x) else z fi |
|
| fpf-single | Def x : v == <[x],x.v> |
|
| id-deq | Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq) |
|
| islocal | Def islocal(k) == isl(k) |
| | | Thm* k:Knd. islocal(k)  |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
