Nuprl - Proof: decidable ex int seg 1 1 2

(9steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable ex int seg 1 1 2

1. i :

2. j :

3. F : {i..j

}

Prop
4.

k:{i..j

}. Dec(F(k))
5. i

j
6. k : {...j-1}
7. i

k
8. Dec(

k:{(k+1)..j

}. F(k))

Dec(

k:{k..j

}. F(k))

By:	Rewrite by Thm* i,j:. Thm* i<j Thm* Thm* (F:({i..j}Prop). (k:{i..j}. F(k)) F(i) (k:{(i+1)..j}. F(k))) THEN BackThru: Thm* Dec(P) Dec(Q) Dec(P Q)

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(9steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc