Nuprl Definition : in-all-states+

in-all-states+{i:l}(es;T;A;l.init[l];t.P[t]) ==

[es:EO'].

[e:E(A)]. ((

[t:T]. (bag-member(T;t;A es e)

P[t]))

(es-initial-event(es;e;A)

P[init[loc(e)]]))

Proof not projected

Definitions occuring in Statement : es-initial-event: es-initial-event(es;e;A), Message: Message, es-E-interface: E(X), event-ordering+: EO+(Info), es-loc: loc(e), uall:

[x:A]. B[x], implies: P

Q, and: P

Q, apply: f a, bag-member: bag-member(T;x;bs)
Definitions : event-ordering+: EO+(Info), Message: Message, es-E-interface: E(X), and: P

Q, uall:

[x:A]. B[x], bag-member: bag-member(T;x;bs), apply: f a, implies: P

Q, es-initial-event: es-initial-event(es;e;A), es-loc: loc(e)
FDL editor aliases : in-all-states+

in-all-states+\{i:l\}(es;T;A;l.init[l];t.P[t]) == \mforall{}[es:EO']. \mforall{}[e:E(A)]. ((\mforall{}[t:T]. (bag-member(T;t;A es e) {}\mRightarrow{} P[t])) \mwedge{} (es-initial-event(es;e;A) {}\mRightarrow{} P[init[loc(e)]])) Date html generated: 2011_10_21-AM-00_01_47 Last ObjectModification: 2011_05_11-PM-12_00_30 Home Index