(18steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
member
upto
1
2
1
1
1
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.
k = i
(k
upto(i+1;j))
i
k
By:
Assert (i+1
k)
Generated subgoals:
1
i+1
k
1
step
2
13.
i+1
k
i
k
Auto
About:
(18steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
i+1
kk ik
i,j:
. j-i = d-1 
(k:. (k 
upto(i;j)) 
ik & k < j)
upto(i+1;j)) i+1k & k < j
upto(i+1;j)) (i+1k & k < j)
k = i
(k upto(i+1;j))
ik
k)
i+1kk ik
