|
This proof proves the theorem
 i: . E:{i...}    {u}.
E[i]   (k:{i + 1...}. E[k - 1] E[k]) {k:{i...}. E[k]}
The following lemma is used in this proof:
- int_upper_well_founded
- n:. WellFnd{i}({n...};x,y.x < y)
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?
|
|
