Nuprl - Proof: bi-graph-to wf 1 1 1 1 2 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bi-graph-to wf 1 1 1 1 2 2 1 1

1. G : Id

2. to : |G|

(IdLnk List)
3. from : |G|

(IdLnk List)
4. bi-graph(G;to;from)
5. x : |G|
6. IdLnk List
7. u : IdLnk
8. v1 : IdLnk List
9. (u

to(x))
10. (

v1.(l

to(x)))
11. v1

Edge(G) List

i:|G|. (u

from(i))

By:	Unfold `bi-graph` 4 THEN InstHyp [x] 4 THEN Analyze -1 THEN Unfold `l_all` -2 THEN InstHyp [u] -2 THEN InstConcl [source(u)] THEN MaAuto

Generated subgoals:

None

About:

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