(14steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: edge-to 1
1. G : Id
2. to : |G|(IdLnk List)
3. from : |G|(IdLnk List)
4. e : Edge(G)
5. i : |G|
6. bi-graph(G;to;from)
7. (e  to(i))
  destination(e) = i
By: DupHyp -2 THEN Unfold `bi-graph` -1 THEN InstHyp [i] -1 THEN Unfold `l_all` -2
THEN
InstHyp [e] -2
THEN
MaAuto

Generated subgoal:

1 8. i:|G|. 
8. (lto(i).destination(l) = i
8. & G(source(l))
8. & (l  from(source(l)))
8. & (lnk-inv(l)  from(i)))
8. & (lfrom(i).source(l) = i
8. & & G(destination(l))
8. & & (l  to(destination(l)))
8. & & (lnk-inv(l)  to(i)))
9. l:IdLnk. 
9. (l  to(i))
9. 
9. destination(l) = i
9. & G(source(l))
9. & (l  from(source(l)))
9. & (lnk-inv(l)  from(i))
10. (lfrom(i).source(l) = i
10. & G(destination(l))
10. & (l  to(destination(l)))
10. & (lnk-inv(l)  to(i)))
  (e  to(i))
3 steps

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

(14steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc