equal
deleted
inserted
replaced
32 condition expresses that the size of the argument @{prop"t : set ts"} of any |
32 condition expresses that the size of the argument @{prop"t : set ts"} of any |
33 recursive call of @{term trev} is strictly less than @{term"size(App f ts)"}, |
33 recursive call of @{term trev} is strictly less than @{term"size(App f ts)"}, |
34 which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and |
34 which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and |
35 continue with our definition. Below we return to the question of how |
35 continue with our definition. Below we return to the question of how |
36 \isacommand{recdef} knows about @{term map}. |
36 \isacommand{recdef} knows about @{term map}. |
|
37 |
|
38 The termination condition is easily proved by induction: |
37 *} |
39 *} |
38 |
40 |
39 (*<*) |
41 (*<*) |
40 end |
42 end |
41 (*>*) |
43 (*>*) |