{
[i,j,n:Id].
((link(n)
from
i
to
j)
IdLnk)
}
{
Proof
}
Definitions occuring in Statement
:
mk_lnk:
(link(n)
from
i
to
j)
,
IdLnk:
IdLnk
,
Id:
Id
,
uall:
[x:A].
B[x]
,
member:
t
T
Definitions
:
uall:
[x:A].
B[x]
,
member:
t
T
,
IdLnk:
IdLnk
,
mk_lnk:
(link(n)
from
i
to
j)
Lemmas
:
Id_wf
\mforall{}[i,j,n:Id]. ((link(n) from i to j) \mmember{} IdLnk)
Date html generated: 2011_08_10-AM-07_43_33
Last ObjectModification: 2011_06_18-AM-08_10_04
Home
Index
[x:A]. B[x], [i,j,n:Id]. ((link(n) from i to j) 
IdLnk) }[x:A]. B[x], T[x:A]. B[x], T,