G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|.
  bi-graph(G;to;from)  ((inverse(e)  from(i))  destination(e) = i)

By:	UnivCD THEN RWO Thm* G:(Id), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|. Thm* bi-graph(G;to;from)  ((e  from(i))  source(e) = i) 0 THENA (MaAuto THEN DoSubsume THEN Analyze 0 THEN MaAuto)

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)   source(inverse(e)) = i  destination(e) = i

1 step

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