Nuprl - Pf decidable__ex_int_seg 1 1 1 2

(14steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: decidable ex int seg 1 1 1 2

1. i:
2. j:
3. F: {i..j}Prop
4. k:{i..j}. Dec(F(k))
5. ij
6. n: {...j-1}
7. in+1 Dec(k:{(n+1)..j}. F(k))
8. in

Dec(k:{n..j}. F(k))

By: Analyze 7 THEN Analyze 8

Generated subgoals:

1 7. in
8. k:{(n+1)..j}. F(k)
Dec(k:{n..j}. F(k))

2 7. in
8. (k:{(n+1)..j}. F(k))
Dec(k:{n..j}. F(k))

About:

(14steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc