Nuprl - Proof: spanner-root-unique 1 1 1 1 1

(37steps 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-unique 1 1 1 1 1

1. T : Id

2. to : |T|

(IdLnk List)
3. from : |T|

(IdLnk List)
4. f : Edge(T)

5. bi-tree(T;to;from)
6. bi-graph(T;to;from)
7.

i,j:|T|.
7.

p:Edge(T) List.
7. lconnects(p;i;j) & (

q:Edge(T) List. lconnects(q;i;j)

q = p)
8.

L:|T| List.

i:|T|. (i

L)
9. |T|
10. spanner(f;T;to;from)
11. i : |T|
12. j : |T|
13. spanner-root(f;T;to;from;i)
14. spanner-root(f;T;to;from;j)
15. Edge(T) List
16. u : Edge(T)
17. u1 : Edge(T)
18. v1 : Edge(T) List
19. 0<||v1||+1

lpath([u1 / v1])

f(last([u1 / v1]))

(

[u1 / v1].f(l))
20. 0<||v1||+1+1
21. lpath([u1 / v1])
22. f(last([u1 / v1]))
23. destination(u) = source(u1)
24.

u1 = lnk-inv(u)
25. f(u1)
26. (

v1.f(l))

f(u)

By:	DupHyp 10 THEN Unfold `spanner` -1 THEN Analyze -1 THEN InstHyp [u1] -2 THEN InstHyp [source(u1);u;inverse(u1)] -2

Generated subgoals:

1 27. l:Edge(T). f(l) = f(inverse(l))
28. i:|T|, l1,l2:Edge(T).
28. (l1  to(i))  (l2  to(i))  l1 = l2  IdLnk  f(l1)  f(l2)
29. f(u1) = f(inverse(u1))
  source(u1)  |T|
1 step

2 27. l:Edge(T). f(l) = f(inverse(l))
28. i:|T|, l1,l2:Edge(T).
28. (l1  to(i))  (l2  to(i))  l1 = l2  IdLnk  f(l1)  f(l2)
29. f(u1) = f(inverse(u1))
  (u  to(source(u1)))
3 steps

3 27. l:Edge(T). f(l) = f(inverse(l))
28. i:|T|, l1,l2:Edge(T).
28. (l1  to(i))  (l2  to(i))  l1 = l2  IdLnk  f(l1)  f(l2)
29. f(u1) = f(inverse(u1))
  (inverse(u1)  to(source(u1)))
6 steps

4 27. l:Edge(T). f(l) = f(inverse(l))
28. i:|T|, l1,l2:Edge(T).
28. (l1  to(i))  (l2  to(i))  l1 = l2  IdLnk  f(l1)  f(l2)
29. f(u1) = f(inverse(u1))
  u = inverse(u1)  IdLnk
3 steps

5 27. l:Edge(T). f(l) = f(inverse(l))
28. i:|T|, l1,l2:Edge(T).
28. (l1  to(i))  (l2  to(i))  l1 = l2  IdLnk  f(l1)  f(l2)
29. f(u1) = f(inverse(u1))
30. f(u)  f(inverse(u1))
  f(u)
4 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(37steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc

1	27. l:Edge(T). f(l) = f(inverse(l)) 28. i:\|T\|, l1,l2:Edge(T). 28. (l1 to(i)) (l2 to(i)) l1 = l2 IdLnk f(l1) f(l2) 29. f(u1) = f(inverse(u1)) source(u1) \|T\|	1 step
2	27. l:Edge(T). f(l) = f(inverse(l)) 28. i:\|T\|, l1,l2:Edge(T). 28. (l1 to(i)) (l2 to(i)) l1 = l2 IdLnk f(l1) f(l2) 29. f(u1) = f(inverse(u1)) (u to(source(u1)))	3 steps
3	27. l:Edge(T). f(l) = f(inverse(l)) 28. i:\|T\|, l1,l2:Edge(T). 28. (l1 to(i)) (l2 to(i)) l1 = l2 IdLnk f(l1) f(l2) 29. f(u1) = f(inverse(u1)) (inverse(u1) to(source(u1)))	6 steps
4	27. l:Edge(T). f(l) = f(inverse(l)) 28. i:\|T\|, l1,l2:Edge(T). 28. (l1 to(i)) (l2 to(i)) l1 = l2 IdLnk f(l1) f(l2) 29. f(u1) = f(inverse(u1)) u = inverse(u1) IdLnk	3 steps
5	27. l:Edge(T). f(l) = f(inverse(l)) 28. i:\|T\|, l1,l2:Edge(T). 28. (l1 to(i)) (l2 to(i)) l1 = l2 IdLnk f(l1) f(l2) 29. f(u1) = f(inverse(u1)) 30. f(u) f(inverse(u1)) f(u)	4 steps