2. j :
3. F : {i..j
}
Prop
4.
k:{i..j}. Dec(F(k))
5. i
j
Dec(
k:{i..j}. F(k))
}Prop
k:{i..j}. Dec(F(k))
j
Dec(k:{i..j}. F(k))| By: |
Thm* i:, E:({...i}Prop).
Thm* E(i)   (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))
Using:[j | E(n):= i n Dec(k:{n..j}. F(k))] |
| 1 |
j
Dec(k:{j..j}. F(k)) | 2 steps |
| 2 |
7. i k
8. Dec( k:{(k+1)..j}. F(k))
Dec(k:{k..j}. F(k)) | 1 step |
| 3 |
k:{...j}. ik Dec(k:{k..j}. F(k))
Dec(k:{i..j}. F(k)) | 1 step |
About:
 |  |  |  |  |  |
 |  |  |  |
 |