{ 
[l:IdLnk]. (source(lnk-inv(l)) ~ destination(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,
lsrc: source(l),
lnk-inv: lnk-inv(l),
ldst: destination(l),
pi1: fst(t),
member: t 
T
Lemmas :
Id_wf
\mforall{}[l:IdLnk]. (source(lnk-inv(l)) \msim{} destination(l))
Date html generated:
2011_08_10-AM-07_46_49
Last ObjectModification:
2011_06_18-AM-08_12_21
Home
Index