Nuprl - Proof: bi-tree-diameter 1 1 1 1 1 2 1 2

(31steps 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: bi-tree-diameter 1 1 1 1 1 2 1 2

1. T : Id

2. to : |T|

(IdLnk List)
3. from : |T|

(IdLnk List)
4. bi-graph(T;to;from)
5.

i,j:|T|.
5.

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

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

q = p)
6. L : |T| List
7.

i:|T|. (i

L)
8. |T|
9. p : Edge(T) List
10. lpath(p)
11.

||p||

||L||
12. g : i:|T|

i@0:

i@0<||L|| & i = L[i@0]
13.

(

n:

||p||, m:

n. source(p[m]) = source(p[n]))
14.

h:(

||p||

|T|). Inj(

||p||; |T|; h)

Inj(|T|;

||L||;

i.1of(g(i)))

By:	Unfold `inject` 0 THEN Reduce 0 THEN Analyze 0 THEN Analyze 0 THEN GenConclAtAddr [1;2;1] THEN Analyze -2 THEN Analyze -2 THEN GenConclAtAddr [1;3;1] THEN Analyze -2 THEN Analyze -2 THEN Reduce 0

Generated subgoal:

1 15. a1 : |T|
16. a2 : |T|
17. i@0 :
18. v2 : i@0<||L||
19. v3 : a1 = L[i@0]
20. g(a1) = <i@0,v2,v3>  i@0:i@0<||L|| & a1 = L[i@0]
21. i1 :
22. v5 : i1<||L||
23. v6 : a2 = L[i1]
24. g(a2) = <i1,v5,v6>  i@0:i@0<||L|| & a2 = L[i@0]
25. i@0 = i1  ||L||
  a1 = a2
1 step

About:

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

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