Nuprl Definition : in-all-state-pairs+

in-all-state-pairs+{i:l}(es;T;A;l.init[l];t1,t2.Q[t1; t2]) ==

[es:EO'].

[e1,e2:E(A)].
((

t1,t2:T. (bag-member(T;t1;A es e1)

bag-member(T;t2;A es e2)

Q[t1; t2]))

(

t:T. (bag-member(T;t;A es e2)

Q[init[loc(e2)]; t]))

(

t:T. (bag-member(T;t;A es e2)

Q[t; init[loc(e2)]])))

Proof not projected

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

[x:A]. B[x], all:

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, uall:

[x:A]. B[x], es-E-interface: E(X), and: P

Q, all:

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

Q, bag-member: bag-member(T;x;bs), apply: f a, es-loc: loc(e)
FDL editor aliases : in-all-state-pairs+

in-all-state-pairs+\{i:l\}(es;T;A;l.init[l];t1,t2.Q[t1; t2]) == \mforall{}[es:EO']. \mforall{}[e1,e2:E(A)]. ((\mforall{}t1,t2:T. (bag-member(T;t1;A es e1) {}\mRightarrow{} bag-member(T;t2;A es e2) {}\mRightarrow{} Q[t1; t2])) \mwedge{} (\mforall{}t:T. (bag-member(T;t;A es e2) {}\mRightarrow{} Q[init[loc(e2)]; t])) \mwedge{} (\mforall{}t:T. (bag-member(T;t;A es e2) {}\mRightarrow{} Q[t; init[loc(e2)]]))) Date html generated: 2011_10_21-AM-00_02_19 Last ObjectModification: 2011_05_11-PM-04_04_26 Home Index