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