This proof proves the theorem
a:. b:. a rem -b = a rem b

The following lemmas are used in this proof:

rem_2_to_1
a:{...0}. n:. a rem n = -(-a rem n)
rem_3_to_1
a:{...0}. n:{...-1}. a rem n = -(-a rem -n)
rem_4_to_1
a:. n:{...-1}. a rem n = a rem -n
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 Six


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