|
This proof proves the theorem
 a,b: . a -- (a -- b) = imin(a;b)
The following definitions are used in this proof:
- imax (integer maximum)
- imax(a;b) == if a
 z b then b else a fi
- imin (integer minimum)
- imin(a;b) == if a z b then a else b fi
- ndiff
- a -- b == imax(a - b;0)
The following lemmas are used in this proof:
- add_com
- a,b:
 . a + b = b + a
- imin_add_r
- a,b,c:. imin(a;b) + c = imin(a + c;b + c)
- imin_com
- a,b:. imin(a;b) = imin(b;a)
- minus_imax
- a,b:. -imax(a;b) = imin(-a;-b)
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?
|
|
