j
Dec(
k:{j..j
}. F(k))7. i
n+1 
Dec(k:{(n+1)..j}. F(k))8. i
n Dec(k:{n..j}. F(k))
}
Prop
k:{i..j}. Dec(F(k))j n:{...j}. in Dec(k:{n..j}. F(k))i:, E:({...i}Prop).
E(i) (k:{...i-1}. E(k+1) E(k)) (k:{...i}. E(k))
| 1 | 6. ij Dec(k:{j..j}. F(k)) |
| 2 | 6. n: {...j-1} 7. i n+1 Dec(k:{(n+1)..j}. F(k))8. i n Dec(k:{n..j}. F(k)) |
About:
 |  |  |  |  |  |