This proof proves the theorem
a,b,c:. imin(a;b) + c = imin(a + c;b + c)

The following definition is used in this proof:

imax (integer maximum)
imax(a;b) == if a z b then b else a fi
Please do the following and record your answers:
  • Translate this proof into English.
  • Was there any part of this proof that you found difficult to translate? If so, why?
  • Do you think that this theorem was proved in a natural or intuitive manner or not? If so, why?

Link to Proof Fourteen


Continue to next page...

Intro to the Study | Introduction to Nuprl | How to Read Nuprl Proofs | Tactic Definitions | Starting the Study | Exiting the Study

In case of questions contact:

Amanda Holland-Minkley
E-mail: hollandm@cs.cornell.edu
Phone: 255-1181
Office: Upson 5141