(18steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
member
upto
1
2
1
1
3
1.
d:
2.
0 < d
3.
i,j:
. j-i = d-1
(
k:
. (k
upto(i;j))
i
k & k < j)
4.
i:
5.
j:
6.
j-i = d
7.
k:
8.
i < j
9.
(k
upto(i+1;j))
i+1
k & k < j
10.
(k
upto(i+1;j))
(i+1
k & k < j)
11.
k = i
12.
i
k
13.
k < j
k = i
(k
upto(i+1;j))
By:
Obvious
Generated subgoals:
None
About:
(18steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
i,j:
. j-i = d-1 
(k:. (k 
upto(i;j)) 
i
k & k < j)
upto(i+1;j)) i+1k & k < j
upto(i+1;j)) (i+1k & k < j)
k = i
k
k = i 
(k upto(i+1;j))