# * Efficient Programming by Extract in Nuprl Type Theory - Continued *

## by Aleksey Nogin

1999-2000

### Comment

I am going to continue talking about efficient programming by extract in Nuprl type theory.I will try to explain while the pigeon-hole principle required such uncomputational proof and will present a slightly better proof.

I will also present the efficient proof of decidability of state reachability and explain why writing such a proof could be done in more straghtforward way than the proof of the pigeon-hole principle.