{ 
[A,B:
']. [init:Id 
bag(B)]. [trX:Id A B B 
EClass'(A)].
(SM-base(init;trX) 
EClass'(B)) }
{ Proof }
Definitions occuring in Statement :
SM-base: SM-base(init;trX),
Message: Message,
eclass: EClass(A[eo; e]),
Id: Id,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
universe: Type,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
eclass: EClass(A[eo; e]),
member: t T,
SM-base: SM-base(init;trX),
top: Top,
all: x:A. B[x],
subtype: S 
T,
label: ...$L... t,
so_lambda: 
x.t[x],
so_apply: x[s]
Lemmas :
rec-combined-loc-class-opt-1_wf,
lifting-loc-2_wf,
pi1_wf_top,
eclass_wf2,
pi2_wf,
Id_wf,
event-ordering+_wf,
Message_wf,
es-E_wf,
event-ordering+_inc,
bag_wf
\mforall{}[A,B:\mBbbU{}']. \mforall{}[init:Id {}\mrightarrow{} bag(B)]. \mforall{}[trX:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B \mtimes{} EClass'(A)].
(SM-base(init;trX) \mmember{} EClass'(B))
Date html generated:
2011_08_17-PM-06_16_44
Last ObjectModification:
2011_08_15-AM-01_49_09
Home
Index