At: decidable ex int seg 1 1 1 2 2 2 1
1. i: 
2. j:
3. F: {i..j
}
Prop
4. 
k:{i..j}. Dec(F(k))
5. i
j
6. n: {...j-1}
7. in
8. 
(
k:{(n+1)..j}. F(k))
9. F(n)
10. k: {n..j}
11. F(k)
False
By: Decide (k = n)
Generated subgoals:| 1 | 12. k = n
False |
| 2 | 12. k = n
False |
About:
