Nuprl - Proof: spanner-root-exists 1 2 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

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. p : Edge(T) List
18. lpath(p)
19. ||p|| = n-1
20. (

l

p.

f(l))

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

& (

l

p.

f(l))

By:

DVar `p'

Generated subgoals:

1 17. lpath(nil)
18. ||nil|| = n-1
19. (lnil.f(l))
  p:Edge(T) List. lpath(p) & ||p|| = n   & (lp.f(l))
3 steps

2 17. u : Edge(T)
18. v : Edge(T) List
19. lpath([u / v])
20. ||[u / v]|| = n-1
21. (l[u / v].f(l))
  p:Edge(T) List. lpath(p) & ||p|| = n   & (lp.f(l))
13 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