1. G : Id
2. to : |G|(IdLnk List)
3. from : |G|(IdLnk List)
4. l : IdLnk
5. i : |G|
6. (l  from(i))
7. i:|G|. 
7. (l:IdLnk. 
7. ((l  to(i))
7. (
7. (destination(l) = i
7. (& G(source(l))
7. (& (l  from(source(l)))
7. (& (lnk-inv(l)  from(i)))
7. & (l:IdLnk. 
7. & ((l  from(i))
7. & (
7. & (source(l) = i
7. & (& G(destination(l))
7. & (& (l  to(destination(l)))
7. & (& (lnk-inv(l)  to(i)))
8. l:IdLnk. 
8. (l  to(i))
8. 
8. destination(l) = i
8. & G(source(l))
8. & (l  from(source(l)))
8. & (lnk-inv(l)  from(i))
9. l:IdLnk. 
9. (l  from(i))
9. 
9. source(l) = i
9. & G(destination(l))
9. & (l  to(destination(l)))
9. & (lnk-inv(l)  to(i))
10. source(l) = i
11. G(destination(l))
12. (l  to(destination(l)))
13. (lnk-inv(l)  to(i))
14. destination(lnk-inv(l)) = i
15. G(source(lnk-inv(l)))
16. (lnk-inv(l)  from(source(lnk-inv(l))))
17. (lnk-inv(lnk-inv(l))  from(i))
  destination(l) = source(lnk-inv(l))

By:	Symmetry THEN BackThru Thm* l:IdLnk. source(lnk-inv(l)) = destination(l)

None

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