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

(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 2

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)

(

l

[l; u / v].

f(l))

By:	RWW Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y)) 0

Generated subgoals:

None

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