Nuprl - Proof: spanner-root-exists 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 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. n :

13.

p:Edge(T) List. lpath(p)

||p||

n
14.

||to(j)|| = 0

Dec(

i:|T|. spanner-root(f;T;to;from;i))

By:	Assert ((i:\|T\|. spanner-root(f;T;to;from;i)) (iL.spanner-root(f;T;to;from;i)))

Generated subgoals:

1   (i:|T|. spanner-root(f;T;to;from;i))  (iL.spanner-root(f;T;to;from;i))
1 step

2 15. (i:|T|. spanner-root(f;T;to;from;i))  (iL.spanner-root(f;T;to;from;i))
  Dec(i:|T|. spanner-root(f;T;to;from;i))
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