D:Dsys, L:Id List.
Thm* (
i:Id. (i 
L) 
ma-is-empty(M(i)))
Thm*
Thm* (
i:Id. Feasible(M(i)))
Thm*
Thm* (
iL.(ltgma-outlinks(M(i);i).(destination(1of(ltg)) L)
Thm* (
iL.(ltgma-outlinks(M(i);i).
Thm* interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg)))))
Thm*
Thm* d-feasible(D)
P:(T
), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'.
Thm* (x
mapfilter(f;P;L)) 
(
y:T. (y L) & P(y) & x = f(y))i:Id, k:Knd. has-src(i;k) isrcv(k) & source(lnk(k)) = iP:(TProp).
Thm* (
x:T. Dec(P(x)))
Thm*
Thm* (finite-type({x:T| P(x) })
(L:T List. x:T. P(x) (x L)))ll:(T List) List, x:T. (x concat(ll)) (l:T List. (l ll) & (x l))a:T List, x:T', f:(TT'). (x map(f;a)) (y:T. (y a) & x = f(y))eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L)M:MsgA. ma-is-empty(M) M = MsgA