Nuprl - Proof: dst-edge 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: dst-edge 1

1. T : Id

2. to : {i:Id| T(i) }

(IdLnk List)
3. from : {i:Id| T(i) }

(IdLnk List)
4. u : {l:IdLnk|

i:|T|. (l

from(i)) }
5.

i:|T|.
5. (

to(i).destination(l) = i
5. & T(source(l))
5. & (l

from(source(l)))
5. & (lnk-inv(l)

from(i)))
5. & (

from(i).source(l) = i
5. & & T(destination(l))
5. & & (l

to(destination(l)))
5. & & (lnk-inv(l)

to(i)))

T(destination(u))

By:	Analyze -2 THEN Unhide THEN MaAuto THEN ExRepD THEN InstHyp [i] -1 THEN Unfold `l_all` -1 THEN InstHyp [u] -1

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html