{ 
[Info,A:Type].
I:EClass(A)
[P:es:EO+(Info) 
E 
]
p:es:EO+(Info). e:E. Dec(P[es;e]). es:EO+(Info). e:E.
(
e 
(I|p) 
{(e I) 
P[es;e]}) }
{ Proof }
Definitions occuring in Statement :
es-interface-restrict: (I|p),
in-eclass: e X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
assert: b,
decidable: Dec(P),
uall: [x:A]. B[x],
prop: ,
guard: {T},
so_apply: x[s1;s2],
all: x:A. B[x],
iff: P Q,
and: P Q,
function: x:A B[x],
universe: Type
Definitions :
guard: {T}
Lemmas :
es-is-interface-restrict
\mforall{}[Info,A:Type].
\mforall{}I:EClass(A)
\mforall{}[P:es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}]
\mforall{}p:\mforall{}es:EO+(Info). \mforall{}e:E. Dec(P[es;e]). \mforall{}es:EO+(Info). \mforall{}e:E.
(\muparrow{}e \mmember{}\msubb{} (I|p) \mLeftarrow{}{}\mRightarrow{} \{(\muparrow{}e \mmember{}\msubb{} I) \mwedge{} P[es;e]\})
Date html generated:
2011_08_16-PM-04_26_04
Last ObjectModification:
2011_06_20-AM-00_50_30
Home
Index