{ 
[es:EO]. [e,e':E]. (e = e') supposing (e' 
loc e and e loc e' ) }
{ Proof }
Definitions occuring in Statement :
es-le: e loc e' ,
es-E: E,
event_ordering: EO,
uimplies: b supposing a,
uall: [x:A]. B[x],
equal: s = t
Definitions :
isect: 
x:A. B[x],
uall: [x:A]. B[x],
tactic: Error :tactic,
CollapseTHEN: Error :CollapseTHEN,
skip: Error :skip
Lemmas :
es-le-antisymmetric
\mforall{}[es:EO]. \mforall{}[e,e':E]. (e = e') supposing (e' \mleq{}loc e and e \mleq{}loc e' )
Date html generated:
2011_08_16-AM-10_32_58
Last ObjectModification:
2011_06_18-AM-09_14_28
Home
Index