{ 
[A:
']. [X:EClass'(A)]. [es:EO']. [e:E]. [L:(A 
E) List].
(classrel-list(es;A;X;L;e) 
') }
{ Proof }
Definitions occuring in Statement :
classrel-list: classrel-list(es;A;X;L;e),
Message: Message,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
uall: [x:A]. B[x],
prop: ,
member: t T,
product: x:A B[x],
list: type List,
universe: Type
Lemmas :
es-E_wf,
Message_wf,
event-ordering+_inc,
es-base-E_wf,
subtype_rel_self,
event-ordering+_wf,
eclass_wf,
eclass_wf3,
eclass_wf2,
bag_wf,
classrel_wf,
l_all_wf,
l_all_wf2,
l_member_wf,
pi2_wf,
pi1_wf_top,
top_wf,
member_wf,
es-locl_wf,
sorted-by_wf,
no_repeats_wf,
map_wf,
es-le_wf,
iff_wf
\mforall{}[A:\mBbbU{}']. \mforall{}[X:EClass'(A)]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[L:(A \mtimes{} E) List]. (classrel-list(es;A;X;L;e) \mmember{} \mBbbP{}')
Date html generated:
2011_08_17-PM-06_25_35
Last ObjectModification:
2011_07_24-PM-04_06_02
Home
Index