Nuprl - mb_event_system_7 Citations of ma-compat

mb event system 7 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def A ||+ B == A || B & ma-frame-compatible(A; B) & ma-sframe-compatible(A; B)

is mentioned by

Thm* loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm*
Thm* Inj(|R|; ; uid)  (A,Bring-leader1(loc;R;uid;out;in).A ||+ B) [ring-leader1__compatible]

Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id.
Thm* A
Thm*
Thm* T
Thm*
Thm* x = "trigger"
Thm*
Thm* locl(a) = k  (A,Btrigger1(loc;T;A;P;i;k;a;x).A ||+ B) [trigger1__compatible]

Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id.
Thm* A  T  x = r  (A,Brecognizer1(loc;T;A;P;k;i;r;x).A ||+ B) [recognizer1__compatible]

Thm* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id.
Thm* "done" = x  A  T  (A,Bsend-once(loc;T;A;a;f;tg;l;x).A ||+ B) [send-once__compatible]

Thm* loc,a,i:Id. (A,Bonce(loc;a;i).A ||+ B) [once__compatible]

Thm* loc:Id, T:Type, c:T, x,i:Id. (A,BDconstant(loc;T;c;x;i).A ||+ B) [Dconstant__compatible]

Thm* x:Id, t,v:Top, x1:Id, t1,v1:Top.
Thm* x = x1  x : t initially x = v ||+ x1 : t1 initially x1 = v1 [ma-single-init-ma-single-init-compatible]

Thm* x:Id, L:Top, t:Type, x1:Id, L1:Top, t1:Type.
Thm* x = x1
Thm*
Thm* only members of L affect x :t ||+ only members of L1 affect x1 :t1 [ma-single-frame-ma-single-frame-compatible]

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top, x1:Id, k1:Knd,
Thm* d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top.
Thm* ds || d1
Thm*
Thm* da || d2
Thm*
Thm* <k,x> = <k1,x1>
Thm*
Thm* ma-single-effect(ds; da; k; x; f) ||+ ma-single-effect(d1; d2; k1; x1; f1) [ma-single-effect-ma-single-effect-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* k1:Knd, l1:IdLnk, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:(IdTop) List.
Thm* ds || d1
Thm*
Thm* da || d2
Thm*
Thm* <k,l> = <k1,l1>
Thm*
Thm* ma-single-sends(ds; da; k; l; f) ||+ ma-single-sends(d1; d2; k1; l1; f1) [ma-single-sends-ma-single-sends-compatible]

Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top.
Thm* x : t || x1 : t1
Thm*
Thm* x1 : t1 initially x1 = v ||+ only members of L affect x :t [ma-single-init-ma-single-frame-compatible]

Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top.
Thm* x : t || x1 : t1
Thm*
Thm* only members of L affect x :t ||+ x1 : t1 initially x1 = v [ma-single-frame-ma-single-init-compatible]

Thm* l:IdLnk, tg:Id, L:Top, x:Id, t,v:Top.
Thm* x : t initially x = v ||+ only L sends on (l with tg) [ma-single-init-ma-single-sframe-compatible]

Thm* l:IdLnk, tg:Id, L:Top, x:Id, L1,t:Top.
Thm* only members of L1 affect x :t ||+ only L sends on (l with tg) [ma-single-frame-ma-single-sframe-compatible]

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type,
Thm* v:t.
Thm* ds || x1 : t
Thm*
Thm* x1 : t initially x1 = v ||+ ma-single-effect(ds; da; k; x; f) [ma-single-init-ma-single-effect-compatible]

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type,
Thm* v:t.
Thm* ds || x1 : t
Thm*
Thm* ma-single-effect(ds; da; k; x; f) ||+ x1 : t initially x1 = v [ma-single-effect-ma-single-init-compatible]

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id,
Thm* L:Knd List, t:Type.
Thm* ds || x1 : t
Thm*
Thm* (x = x1  (k  L))
Thm*
Thm* only members of L affect x1 :t ||+ ma-single-effect(ds; da; k; x; f) [ma-single-frame-ma-single-effect-compatible]

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id,
Thm* L:Knd List, t:Type.
Thm* ds || x1 : t
Thm*
Thm* (x = x1  (k  L))
Thm*
Thm* ma-single-effect(ds; da; k; x; f) ||+ only members of L affect x1 :t [ma-single-effect-ma-single-frame-compatible]

Thm* x:Id, k:Knd, ds:x:Id fp-> Top, da:a:Knd fp-> Top, f:Top, l:IdLnk, tg:Id,
Thm* L:Top. ma-single-effect(ds; da; k; x; f) ||+ only L sends on (l with tg) [ma-single-effect-ma-single-sframe-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List,
Thm* x:Id, t:Type, v:t.
Thm* ds || x : t  x : t initially x = v ||+ ma-single-sends(ds; da; k; l; f) [ma-single-init-ma-single-sends-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List,
Thm* x:Id, t:Type, v:t.
Thm* ds || x : t  ma-single-sends(ds; da; k; l; f) ||+ x : t initially x = v [ma-single-sends-ma-single-init-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List,
Thm* x:Id, L:Top, t:Type.
Thm* ds || x : t
Thm*
Thm* only members of L affect x :t ||+ ma-single-sends(ds; da; k; l; f) [ma-single-frame-ma-single-sends-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List,
Thm* x:Id, L:Top, t:Type.
Thm* ds || x : t
Thm*
Thm* ma-single-sends(ds; da; k; l; f) ||+ only members of L affect x :t [ma-single-sends-ma-single-frame-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* l1:IdLnk, tg:Id, L:Knd List.
Thm* (l = l1  (tg  map(p.1of(p);f))  (k  L))
Thm*
Thm* ma-single-sends(ds; da; k; l; f) ||+ only L sends on (l1 with tg) [ma-single-sends-ma-single-sframe-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top.
Thm* ds || d1
Thm*
Thm* da || d2
Thm*
Thm* ma-single-effect(d1; d2; k1; x; f1) ||+ ma-single-sends(ds; da; k; l; f) [ma-single-effect-ma-single-sends-compatible]

Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top.
Thm* ds || d1
Thm*
Thm* da || d2
Thm*
Thm* ma-single-sends(ds; da; k; l; f) ||+ ma-single-effect(d1; d2; k1; x; f1) [ma-single-sends-ma-single-effect-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t.
Thm* ds || x : t
Thm*
Thm* x : t initially x = v ||+ (with ds: ds
Thm* xaction a:T
Thm* xprecondition a(v) is
Thm* xP s v) [ma-single-init-ma-single-pre-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t.
Thm* ds || x : t
Thm*
Thm* (with ds: ds
Thm* (action a:T
Thm* (precondition a(v) is
Thm* (P s v) ||+ x : t initially x = v [ma-single-pre-ma-single-init-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type.
Thm* ds || x : t
Thm*
Thm* only members of L affect x :t ||+ (with ds: ds
Thm* oaction a:T
Thm* oprecondition a(v) is
Thm* oP s v) [ma-single-frame-ma-single-pre-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type.
Thm* ds || x : t
Thm*
Thm* (with ds: ds
Thm* (action a:T
Thm* (precondition a(v) is
Thm* (P s v) ||+ only members of L affect x :t [ma-single-pre-ma-single-frame-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Top, P:Top, l:IdLnk, tg:Id, L:Top.
Thm* (with ds: ds
Thm* (action a:T
Thm* (precondition a(v) is
Thm* (P s v) ||+ only L sends on (l with tg) [ma-single-pre-ma-single-sframe-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, k:Knd, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:Top.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* ma-single-effect(d1; da; k; x; f) ||+ (with ds: ds
Thm* maction a:T
Thm* mprecondition a(v) is
Thm* mP s v) [ma-single-effect-ma-single-pre-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* ma-single-sends(d1; da; k; l; f) ||+ (with ds: ds
Thm* maction a:T
Thm* mprecondition a(v) is
Thm* mP s v) [ma-single-sends-ma-single-pre-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* (with ds: ds
Thm* (action a:T
Thm* (precondition a(v) is
Thm* (P s v) ||+ ma-single-sends(d1; da; k; l; f) [ma-single-pre-ma-single-sends-compatible]

Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> ds(x)?Void, x:Id,
Thm* t:Type, v:t.
Thm* ds || x : t
Thm*
Thm* (x  dom(init)  init(x) = v  t)
Thm*
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ x : t initially x = v [ma-single-pre-init-ma-single-init-compatible]

Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id,
Thm* L:Knd List, t:Type.
Thm* ds || x : t
Thm*
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ only members of L affect x :t [ma-single-pre-init-ma-single-frame-compatible]

Thm* a:Id, T:Top, ds:x:Id fp-> Top, P:Top, init:x:Id fp-> Top, l:IdLnk, tg:Id,
Thm* L:Knd List.
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ only L sends on (l with tg) [ma-single-pre-init-ma-single-sframe-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, k:Knd,
Thm* d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ ma-single-effect(d1; da; k; x; f) [ma-single-pre-init-ma-single-effect-compatible]

Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, k:Knd,
Thm* l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm*
Thm* locl(a) : T || da
Thm*
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ ma-single-sends(d1; da; k; l; f) [ma-single-pre-init-ma-single-sends-compatible]

Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, a1:Id, T1:Top,
Thm* d1:x:Id fp-> Type, P1:Top.
Thm* ds || d1
Thm*
Thm* a = a1
Thm*
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ (with ds: d1
Thm* aaction a1:T1
Thm* aprecondition a1(v) is
Thm* aP1 s v) [ma-single-pre-init-ma-single-pre-compatible]

In prior sections: mb event system 6

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 7 Sections EventSystems Doc

Thm* loc:Id, R:(Id), uid:(\|R\|), out,in:(\|R\|IdLnk). Thm* ring(R;in;out) Thm* Thm* Inj(\|R\|; ; uid) (A,Bring-leader1(loc;R;uid;out;in).A \|\|+ B)	[ring-leader1__compatible]
Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm* Thm* T Thm* Thm* x = "trigger" Thm* Thm* locl(a) = k (A,Btrigger1(loc;T;A;P;i;k;a;x).A \|\|+ B)	[trigger1__compatible]
Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id. Thm* A T x = r (A,Brecognizer1(loc;T;A;P;k;i;r;x).A \|\|+ B)	[recognizer1__compatible]
Thm* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x A T (A,Bsend-once(loc;T;A;a;f;tg;l;x).A \|\|+ B)	[send-once__compatible]
Thm* loc,a,i:Id. (A,Bonce(loc;a;i).A \|\|+ B)	[once__compatible]
Thm* loc:Id, T:Type, c:T, x,i:Id. (A,BDconstant(loc;T;c;x;i).A \|\|+ B)	[Dconstant__compatible]
Thm* x:Id, t,v:Top, x1:Id, t1,v1:Top. Thm* x = x1 x : t initially x = v \|\|+ x1 : t1 initially x1 = v1	[ma-single-init-ma-single-init-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, L1:Top, t1:Type. Thm* x = x1 Thm* Thm* only members of L affect x :t \|\|+ only members of L1 affect x1 :t1	[ma-single-frame-ma-single-frame-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top, x1:Id, k1:Knd, Thm* d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. Thm* ds \|\| d1 Thm* Thm* da \|\| d2 Thm* Thm* <k,x> = <k1,x1> Thm* Thm* ma-single-effect(ds; da; k; x; f) \|\|+ ma-single-effect(d1; d2; k1; x1; f1)	[ma-single-effect-ma-single-effect-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, Thm* k1:Knd, l1:IdLnk, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:(IdTop) List. Thm* ds \|\| d1 Thm* Thm* da \|\| d2 Thm* Thm* <k,l> = <k1,l1> Thm* Thm* ma-single-sends(ds; da; k; l; f) \|\|+ ma-single-sends(d1; d2; k1; l1; f1)	[ma-single-sends-ma-single-sends-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top. Thm* x : t \|\| x1 : t1 Thm* Thm* x1 : t1 initially x1 = v \|\|+ only members of L affect x :t	[ma-single-init-ma-single-frame-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top. Thm* x : t \|\| x1 : t1 Thm* Thm* only members of L affect x :t \|\|+ x1 : t1 initially x1 = v	[ma-single-frame-ma-single-init-compatible]
Thm* l:IdLnk, tg:Id, L:Top, x:Id, t,v:Top. Thm* x : t initially x = v \|\|+ only L sends on (l with tg)	[ma-single-init-ma-single-sframe-compatible]
Thm* l:IdLnk, tg:Id, L:Top, x:Id, L1,t:Top. Thm* only members of L1 affect x :t \|\|+ only L sends on (l with tg)	[ma-single-frame-ma-single-sframe-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type, Thm* v:t. Thm* ds \|\| x1 : t Thm* Thm* x1 : t initially x1 = v \|\|+ ma-single-effect(ds; da; k; x; f)	[ma-single-init-ma-single-effect-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, t:Type, Thm* v:t. Thm* ds \|\| x1 : t Thm* Thm* ma-single-effect(ds; da; k; x; f) \|\|+ x1 : t initially x1 = v	[ma-single-effect-ma-single-init-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, Thm* L:Knd List, t:Type. Thm* ds \|\| x1 : t Thm* Thm* (x = x1 (k L)) Thm* Thm* only members of L affect x1 :t \|\|+ ma-single-effect(ds; da; k; x; f)	[ma-single-frame-ma-single-effect-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, Thm* L:Knd List, t:Type. Thm* ds \|\| x1 : t Thm* Thm* (x = x1 (k L)) Thm* Thm* ma-single-effect(ds; da; k; x; f) \|\|+ only members of L affect x1 :t	[ma-single-effect-ma-single-frame-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Top, da:a:Knd fp-> Top, f:Top, l:IdLnk, tg:Id, Thm* L:Top. ma-single-effect(ds; da; k; x; f) \|\|+ only L sends on (l with tg)	[ma-single-effect-ma-single-sframe-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, t:Type, v:t. Thm* ds \|\| x : t x : t initially x = v \|\|+ ma-single-sends(ds; da; k; l; f)	[ma-single-init-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, t:Type, v:t. Thm* ds \|\| x : t ma-single-sends(ds; da; k; l; f) \|\|+ x : t initially x = v	[ma-single-sends-ma-single-init-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, L:Top, t:Type. Thm* ds \|\| x : t Thm* Thm* only members of L affect x :t \|\|+ ma-single-sends(ds; da; k; l; f)	[ma-single-frame-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, L:Top, t:Type. Thm* ds \|\| x : t Thm* Thm* ma-single-sends(ds; da; k; l; f) \|\|+ only members of L affect x :t	[ma-single-sends-ma-single-frame-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, Thm* l1:IdLnk, tg:Id, L:Knd List. Thm* (l = l1 (tg map(p.1of(p);f)) (k L)) Thm* Thm* ma-single-sends(ds; da; k; l; f) \|\|+ only L sends on (l1 with tg)	[ma-single-sends-ma-single-sframe-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, Thm* x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. Thm* ds \|\| d1 Thm* Thm* da \|\| d2 Thm* Thm* ma-single-effect(d1; d2; k1; x; f1) \|\|+ ma-single-sends(ds; da; k; l; f)	[ma-single-effect-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List, Thm* x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top. Thm* ds \|\| d1 Thm* Thm* da \|\| d2 Thm* Thm* ma-single-sends(ds; da; k; l; f) \|\|+ ma-single-effect(d1; d2; k1; x; f1)	[ma-single-sends-ma-single-effect-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t. Thm* ds \|\| x : t Thm* Thm* x : t initially x = v \|\|+ (with ds: ds Thm* xaction a:T Thm* xprecondition a(v) is Thm* xP s v)	[ma-single-init-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, t:Type, v:t. Thm* ds \|\| x : t Thm* Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) \|\|+ x : t initially x = v	[ma-single-pre-ma-single-init-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type. Thm* ds \|\| x : t Thm* Thm* only members of L affect x :t \|\|+ (with ds: ds Thm* oaction a:T Thm* oprecondition a(v) is Thm* oP s v)	[ma-single-frame-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type. Thm* ds \|\| x : t Thm* Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) \|\|+ only members of L affect x :t	[ma-single-pre-ma-single-frame-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Top, P:Top, l:IdLnk, tg:Id, L:Top. Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) \|\|+ only L sends on (l with tg)	[ma-single-pre-ma-single-sframe-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, k:Knd, d1:x:Id fp-> Type, Thm* da:a:Knd fp-> Type, f:Top. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* ma-single-effect(d1; da; k; x; f) \|\|+ (with ds: ds Thm* maction a:T Thm* mprecondition a(v) is Thm* mP s v)	[ma-single-effect-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type, Thm* da:a:Knd fp-> Type, f:(IdTop) List. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* ma-single-sends(d1; da; k; l; f) \|\|+ (with ds: ds Thm* maction a:T Thm* mprecondition a(v) is Thm* mP s v)	[ma-single-sends-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type, Thm* da:a:Knd fp-> Type, f:(IdTop) List. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) \|\|+ ma-single-sends(d1; da; k; l; f)	[ma-single-pre-ma-single-sends-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> ds(x)?Void, x:Id, Thm* t:Type, v:t. Thm* ds \|\| x : t Thm* Thm* (x dom(init) init(x) = v t) Thm* Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ x : t initially x = v	[ma-single-pre-init-ma-single-init-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, Thm* L:Knd List, t:Type. Thm* ds \|\| x : t Thm* Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ only members of L affect x :t	[ma-single-pre-init-ma-single-frame-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Top, P:Top, init:x:Id fp-> Top, l:IdLnk, tg:Id, Thm* L:Knd List. Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ only L sends on (l with tg)	[ma-single-pre-init-ma-single-sframe-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, k:Knd, Thm* d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ ma-single-effect(d1; da; k; x; f)	[ma-single-pre-init-ma-single-effect-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, k:Knd, Thm* l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List. Thm* ds \|\| d1 Thm* Thm* locl(a) : T \|\| da Thm* Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ ma-single-sends(d1; da; k; l; f)	[ma-single-pre-init-ma-single-sends-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, a1:Id, T1:Top, Thm* d1:x:Id fp-> Type, P1:Top. Thm* ds \|\| d1 Thm* Thm* a = a1 Thm* Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) \|\|+ (with ds: d1 Thm* aaction a1:T1 Thm* aprecondition a1(v) is Thm* aP1 s v)	[ma-single-pre-init-ma-single-pre-compatible]