Nuprl - mb_event_system_7 Citations of ma-single-pre

mb event system 7 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def (with ds: ds
Def (action a:T
Def (precondition a(v) is
Def (P s v)
Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )

is mentioned by

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-> 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 mb event system 4 mb event system 5

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* 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-> 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]