2. to : |G|
(IdLnk List)
3. from : |G|
(IdLnk List)
4. l : IdLnk
5.
i:|G|. (l 
from(i))
6. bi-graph(G;to;from)
i:|G|. (lnk-inv(l) from(i))
(IdLnk List)
(IdLnk List)
i:|G|. (l from(i))
i:|G|. (lnk-inv(l) from(i))| By: |
THEN All (Unfold `l_all`) THEN InstHyp [l] -1 THEN ExRepD THEN InstConcl [destination(l)] THENA MaAuto THEN InstHyp [lnk-inv(l)] -6 THEN MaAuto THEN NthHypEq -2 THEN Analyze THEN Analyze |
| 1 |
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)) |G| | 2 steps |
About:
 |  |  |  |  |  |