{ 
[l:IdLnk]. (destination(lnk-inv(l)) ~ source(l)) }
{ Proof }
Definitions occuring in Statement :
ldst: destination(l),
lsrc: source(l),
lnk-inv: lnk-inv(l),
IdLnk: IdLnk,
uall: [x:A]. B[x],
sqequal: s ~ t
Definitions :
uall: [x:A]. B[x],
IdLnk: IdLnk,
ldst: destination(l),
lnk-inv: lnk-inv(l),
lsrc: source(l),
pi1: fst(t),
pi2: snd(t),
member: t 
T
Lemmas :
Id_wf
\mforall{}[l:IdLnk]. (destination(lnk-inv(l)) \msim{} source(l))
Date html generated:
2011_08_10-AM-07_46_51
Last ObjectModification:
2011_06_18-AM-08_12_23
Home
Index