|
This proof proves the theorem
 x,y: . |x| = |y|    x =  y
The following definitions are used in this proof:
- absval (absolute value)
- |i| == if 0
 z i then i else -i fi
- pm_equal (equals plus or minus)
- i = j == i = j
 i = -j
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?
|
|
