(18steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
member
upto
1
2
1.
d:
2.
0 < d
3.
i,j:
. j-i = d-1
(
k:
. (k
upto(i;j))
i
k & k < j)
i,j:
. j-i = d
(
k:
. (k
upto(i;j))
i
k & k < j)
By:
UnivCD
THEN
RecUnfold `upto` 0
THEN
SplitOnConclITE
Generated subgoals:
1
4.
i:
5.
j:
6.
j-i = d
7.
k:
8.
i < j
(k
[i / upto(i+1;j)])
i
k & k < j
7
steps
 
2
4.
i:
5.
j:
6.
j-i = d
7.
k:
8.
j
i
(k
nil)
i
k & k < j
1
step
About:
(18steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc