Nuprl Definition : in-all-ordered-state-pairs+
in-all-ordered-state-pairs+{i:l}(es;T;A;l.init[l];t1,t2.Q[t1; t2]) ==
[e1,e2:E(A)].
((((e1 <loc e2) 
(e1 = e2)) 
(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])))
Proof not projected
Definitions occuring in Statement :
es-E-interface: E(X),
es-locl: (e <loc e'),
es-loc: loc(e),
es-E: E,
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
or: P Q,
and: P Q,
apply: f a,
equal: s = t,
bag-member: bag-member(T;x;bs)
Definitions :
uall: [x:A]. B[x],
es-E-interface: E(X),
and: P Q,
or: P Q,
es-locl: (e <loc e'),
equal: s = t,
es-E: E,
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-ordered-state-pairs+
in-all-ordered-state-pairs+\{i:l\}(es;T;A;l.init[l];t1,t2.Q[t1; t2]) ==
\mforall{}[e1,e2:E(A)].
((((e1 <loc e2) \mvee{} (e1 = e2))
{}\mRightarrow{} (\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])))
Date html generated:
2011_10_21-AM-00_02_52
Last ObjectModification:
2011_06_09-PM-04_04_44
Home
Index