{ 
[l1,l2:IdLnk]. [tg1,tg2:Id].
{(l1 = l2) 
(tg1 = tg2)} supposing rcv(l1,tg1) = rcv(l2,tg2) }
{ Proof }
Definitions occuring in Statement :
rcv: rcv(l,tg),
Knd: Knd,
IdLnk: IdLnk,
Id: Id,
uimplies: b supposing a,
uall: [x:A]. B[x],
guard: {T},
and: P Q,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
guard: {T},
and: P Q,
member: t 
T,
prop: 
,
IdLnk: IdLnk,
Id: Id,
pi1: fst(t),
outl: outl(x),
assert: 
b,
isl: isl(x),
all: x:A. B[x],
so_lambda: 
x.t[x],
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
cand: A c B,
pi2: snd(t),
top: Top,
subtype: S 
T,
Knd: Knd,
rcv: rcv(l,tg),
sq_type: SQType(T),
so_apply: x[s],
implies: P 
Q
Lemmas :
Knd_wf,
rcv_wf,
Id_wf,
IdLnk_wf,
member_wf,
outl_wf,
subtype_base_sq,
union_subtype_base,
product_subtype_base,
atom2_subtype_base,
pi1_wf_top,
pi2_wf
\mforall{}[l1,l2:IdLnk]. \mforall{}[tg1,tg2:Id]. \{(l1 = l2) \mwedge{} (tg1 = tg2)\} supposing rcv(l1,tg1) = rcv(l2,tg2)
Date html generated:
2011_08_10-AM-07_45_48
Last ObjectModification:
2011_06_18-AM-08_10_35
Home
Index