2. f : {f | i:{i1:
| i1 (
i,j. i<j) i } 
if i=
0
else {f(i-1)...} fi}
3.
j:{k:| k<i }. f(j) 
4. i
0
5. j :
(f(i-1)
j) Prop
| i1 (i,j. i<j) i } if i=0 else {f(i-1)...} fi}
j:{k:| k<i }. f(j)
0
(f(i-1)j) Prop| By: |
|
| 1 |
f(i-1)  | 1 step |
| 2 |
j | Trivial |
About:
 |  |  |  |  |
 |  |  |  |  |
 |