How to access ETPS:

1. Login to an andrew machine with your id.

2. Do "source /afs/andrew/mcs/math/etps/etps.cshrc" at the command
   line. This sets up paths to etps and fontpath so that you can use
   mathematical fonts.  If you are logging into an andrew workstation
   remotely, you will have to copy fonts from the directory
   /afs/andrew.cmu.edu/mcs/math/etps/fonts to a directory on your
   local machine (say ~user/fontdir) and use xset to setup the fonts
   path like so

   xset fp+ ~user/fontdir
   xset fp rehash

   To see if the fonts were actually installed, you can try "xterm -fn
   vtsymbold" and you should see some math symbols in your xterm.

3. Start etps by typing either etps of xetps.
   Now onwards, type the commands in etps window.

4. setflag style <Enter> xterm <Enter>

5. setflag printtypes <Enter> nil <Enter>

6. begin-prfw
   This opens up three new windows containing the full proof, the
   current subproof and proof outline.  Do not type in this windows.
   If you don't want these windows, skip this step.

7. To prove a statement enter
      prove "text of the statement"
   It will ask you for a name of the proof. Enter the name. Then it will
      ask you for line number of the statement, press enter to accept
      the default value, or you can choose your own number. Many
      commands in ETPS are interactive, and it provides very
      reasonable default choices.  You will have to provide the values
      you want to change the defaults or there are no defaults.

8. Keep on introducing hypotheses lines by the command "hyp". It will
   ask you for the line numbers of the statement to be proved and the
   hypothesis. It will also ask you for the statement of the
   hypotheses.

9. type "pall". This prints all the lines of the proof so far and
   updates other windows.  Notice that the theorem line doesn't have
   any hypotheses to its left side.  The lines that are yet unproven
   are displayed as planned lines.

10. Now add hypothesis to the statement to be proved by the command
    "add-hyps".  It will ask you the line number of the hypothesis and
    the line number of the statement to be proven.  Do this for all hypothesis.

11. Refer to full ETPS documentation for the use of various inference
    rules in your proof.  Use the "advice" command for getting an advice if
    you are stuck.

12. If you are running TPS, it can prove theorems for you
    automatically. The command is called "diy".

13. If you have proved the statement, then type "done".

14. If you want to save your proof in the middle, you can say
    "saveproof".  Restore the proof later on by the command
    "restoreproof".

15. Generate a tex file of your proof by the command "texproof". This
    will generate a .tex file. This is *not* a latex file, but a pure
    tex file. Process it using "tex proof.tex". This will generate
    file.dvi.  Get a postscript file by "dvips -o file.ps file.dvi".

16. Finally, exit using "exit".