| | 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 |
|
| 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-pre-init | Def (with ds: ds
Def (init: init
Def action a:T
Def aprecondition a(v) is
Def aP)
Def == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; ) |
|
| fpf-single | Def x : v == <[x], x.v> |
|
| id-deq | Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq) |
|
| locl | Def locl(a) == inr(a) |
| | | Thm* a:Id. locl(a) Knd |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
