Nuprl - Proof: spanner-root-exists 1 2 2 1 2 1 2 1 2 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 2 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. u : Edge(T)
18. v : Edge(T) List
19. lpath([u / v])
20. ||v||+1 = n-1
21.

f(u)
22. (

l

v.

f(l))
23. l : Edge(T)
24. (l

to(source(u)))
25.

f(l)

lpath([l; u / v])

By:	RWO Thm* l:IdLnk, p:IdLnk List. Thm* lpath([l / p]) Thm* Thm* lpath(p) Thm* & (\|\|p\|\| = 0 destination(l) = source(hd(p)) & hd(p) = lnk-inv(l)) 0 THEN MaAuto THEN Reduce 0

Generated subgoals:

1 26. ||[u / v]|| = 0
  destination(l) = source(u)
8 steps

2 26. ||[u / v]|| = 0
  u = lnk-inv(l)  IdLnk
2 steps

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