On this and the following pages, you will be asked to answer some questions and translate some Nuprl proofs into English. You are encouraged to enter your answers into a text document, keeping track of the question number and/or proof number that you are working on. When you have finished, e-mail this document to Amanda (hollandm@cs.cornell.edu). If this is inconvenient for you, though, you can also answer these questions on paper and deliver them to my mailbox or my office.

To navigate this study, read each page in its entirety, answer all questions to the best of your ability, and then proceed on to the next page. Once you have answered the questions on a page, please do not return to that page or change your answers or translated proof for that page. As mentioned before, you do not need to complete this study all in one sitting. You can send me your responses in batches or wait and send them all at once, but please be sure that your name appears at the top of any document you send me. You are not required to translate all the proofs in order for your participation to be valuable. Please be sure, after you have finished the last proof that you are going to translate, to go to the "Exiting the Study" page (listed in the menu bar at the side and bottom of each page) and answer the questions there.

Most of the theorems you will translate refer to externally defined lemmas and functions. These will be defined for you on the page introducing the proof. The various tactics used in the proof are defined for you on then Tactic Definitions page.

If in the process of translating a proof you get stuck because you cannot understand the Nuprl version, you can indicate this in your translation and leave a hole in the proof. However, please explain where it was that you got stuck and what it was that you could not understand.

Please translate the proof as it appears; by this I mean take the proof tree as it is and work from there. Do not change the way in which the proof was carried out. However, you may traverse the given proof tree in any order that you like and you can omit any information included in the Nuprl proof that you do not think is necessary for the English version. As a guideline, write the proof as you would want it to appear if you were going to have to read it and understand it without having access to the Nuprl proof at all (and, since these are very simple theorems, as if you were just learning these facts about mathematics). In addition, you do not need to translate basic formulas into English, though you may if you think it makes the proof clearer. Something of the form "a = 0" can be used in that way in the proof.

If you have a question about any part of this study, about any of the questions, or about a proof in particular, do not hesitate to contact me. I do ask that you not discuss anything appearing within this study with other people who may be participating.

Continue to next page...