{ 
[es:EO]. [T:Type]. [f:T 
E].
LocalOrderPreserving(f) 
supposing T 
r E }
{ Proof }
Definitions occuring in Statement :
es-locl-op: LocalOrderPreserving(f),
es-E: E,
event_ordering: EO,
subtype_rel: A r B,
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
member: t T,
es-locl-op: LocalOrderPreserving(f),
so_lambda: 
x y.t[x; y],
so_apply: x[s1;s2]
Lemmas :
order-preserving_wf,
es-locl_wf,
es-E_wf,
event_ordering_wf
\mforall{}[es:EO]. \mforall{}[T:Type]. \mforall{}[f:T {}\mrightarrow{} E]. LocalOrderPreserving(f) \mmember{} \mBbbP{} supposing T \msubseteq{}r E
Date html generated:
2011_08_16-AM-10_31_14
Last ObjectModification:
2011_06_18-AM-09_13_05
Home
Index