Nuprl Definition : in-all-states
in-all-states{i:l}(Info;es;T;A;l.init[l];t.P[t]) ==
[es:EO+(Info)]. [e:E(A)]. (([t:T]. (bag-member(T;t;A es e) 
P[t])) 
P[init[loc(e)]])
Proof not projected
Definitions occuring in Statement :
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),
es-E-interface: E(X),
and: P Q,
uall: [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-states
in-all-states\{i:l\}(Info;es;T;A;l.init[l];t.P[t]) ==
\mforall{}[es:EO+(Info)]. \mforall{}[e:E(A)]. ((\mforall{}[t:T]. (bag-member(T;t;A es e) {}\mRightarrow{} P[t])) \mwedge{} P[init[loc(e)]])
Date html generated:
2011_10_21-AM-00_01_16
Last ObjectModification:
2011_05_11-PM-03_57_40
Home
Index