(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 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|. (lto(i).f(l))
15. n : 
16. 0<n
17. u : Edge(T)
18. v : Edge(T) List
19. lpath([u / v])
20. ||v||+1 = n-1
21. f(u)
22. (lv.f(l))
23. l : Edge(T)
24. (l  to(source(u)))
25. f(l)
26. ||[u / v]|| = 0
  destination(l) = source(u)
By: DupHyp 5 THEN Unfold `bi-graph` -1 THEN InstHyp [source(u)] -1 THEN MaAuto

Generated subgoals:

1 27. i:|T|. 
27. (lto(i).destination(l) = i
27. & T(source(l))
27. & (l  from(source(l)))
27. & (lnk-inv(l)  from(i)))
27. & (lfrom(i).source(l) = i
27. & & T(destination(l))
27. & & (l  to(destination(l)))
27. & & (lnk-inv(l)  to(i)))
  source(u)  |T|
1 step
2 27. i:|T|. 
27. (lto(i).destination(l) = i
27. & T(source(l))
27. & (l  from(source(l)))
27. & (lnk-inv(l)  from(i)))
27. & (lfrom(i).source(l) = i
27. & & T(destination(l))
27. & & (l  to(destination(l)))
27. & & (lnk-inv(l)  to(i)))
28. (lto(source(u)).destination(l) = source(u)
28. & T(source(l))
28. & (l  from(source(l)))
28. & (lnk-inv(l)  from(source(u))))
29. (lfrom(source(u)).source(l) = source(u)
29. & T(destination(l))
29. & (l  to(destination(l)))
29. & (lnk-inv(l)  to(source(u))))
  destination(l) = source(u)
6 steps

About:
listconsboolassertintnatural_numberaddsubtractless_thanapply
functionequalmemberimpliesandall
exists
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