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

At: member upto 1 2 1 1
1. d:
2. 0 < d
3. i,j:. j-i = d-1 (k:. (k upto(i;j)) ik & k < j)
4. i:
5. j:
6. j-i = d
7. k:
8. i < j
9. (k upto(i+1;j)) i+1k & k < j
(k [i / upto(i+1;j)]) ik & k < j
By:
Decide (k = i)
THEN
RWW Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) 0
Generated subgoals:

19. (k upto(i+1;j)) i+1k & k < j
10. (k upto(i+1;j)) (i+1k & k < j)
11. k = i
12. k = i (k upto(i+1;j))
ik		3 steps
 
29. (k upto(i+1;j)) i+1k & k < j
10. (k upto(i+1;j)) (i+1k & k < j)
11. k = i
12. k = i (k upto(i+1;j))
k < j		1 step
 
39. (k upto(i+1;j)) i+1k & k < j
10. (k upto(i+1;j)) (i+1k & k < j)
11. k = i
12. ik
13. k < j
k = i (k upto(i+1;j))		1 step

About:
listconsintnatural_numberaddsubtractless_than
universeequalimpliesandorall

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