Nuprl - Proof: member upto

(18steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

i,j,k:. (k upto(i;j)) ik & k < j

By: Assert (d,i,j:. j-i = d (k:. (k upto(i;j)) ik & k < j))

Generated subgoals:

1 d,i,j:. j-i = d (k:. (k upto(i;j)) ik & k < j) 12 steps

2 1. d,i,j:. j-i = d (k:. (k upto(i;j)) ik & k < j)
i,j,k:. (k upto(i;j)) ik & k < j 5 steps

About:

(18steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

1	`d,i,j:. j-i = d (k:. (k upto(i;j)) ik & k < j)`	12 steps

2	1. `d,i,j:. j-i = d (k:. (k upto(i;j)) ik & k < j)` `i,j,k:. (k upto(i;j)) ik & k < j`	5 steps