Nuprl - Proof: spanner-root-exists 1 2 2 1 2 1 2 1 1

(35steps 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: spanner-root-exists 1 2 2 1 2 1 2 1 1

1. T : Id

2. to : |T|

(IdLnk List)
3. from : |T|

(IdLnk List)
4. f : Edge(T)

5. bi-graph(T;to;from)
6.

i,j:|T|.
6.

p:Edge(T) List.
6. lconnects(p;i;j) & (

q:Edge(T) List. lconnects(q;i;j)

q = p)
7. L : |T| List
8.

i:|T|. (i

L)
9. j : |T|
10. bi-graph(T;to;from)
11. spanner(f;T;to;from)
12.

||to(j)|| = 0
13.

(

i:|T|.

l:Edge(T). (l

to(i))

f(l))
14.

i:|T|. (

l

to(i).

f(l))
15. n :

16. 0<n
17. lpath(nil)
18. ||nil|| = n-1
19. (

l

nil.

f(l))

p:Edge(T) List. lpath(p) & ||p|| = n

& (

l

p.

f(l))

By:	InstHyp [j] -6 THEN Analyze -1 THEN InstConcl [[l]] THEN Reduce 0 THEN MaAuto

Generated subgoals:

1 20. l : Edge(T)
21. (l  to(j))
22. f(l)
  lpath([l])
1 step

2 20. l : Edge(T)
21. (l  to(j))
22. f(l)
  (l[l].f(l))
1 step

About:

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

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