The message of this chapter is that properties of non-recursive functions should not be proved by induction.
In a general way, there are the main functions and we prove main theorems about them. These main functions call auxiliary functions, and we write auxiliary lemmas about these auxiliary functions. Just as the main functions call the auxiliary functions, the main theorems are proved as corollaries of the auxiliary lemmas. (Typically the auxiliary functions are recursive and so the auxiliary lemmas are proved by induction.)
In other words, a property about a non-recursive function that calls a recursive function should not be proved by induction. It should be proved as a corollary of a lemma about this recursive function, and this lemma should be proved by induction. This way, the structure of the proofs about programs follows the (control) structure of these programs, which is a reliable guideline.
Trimmed this chapter and made it more explicit with an opening message [20 Aug 2024]
Factored out what is now Chapter Two more goodies to go, and expanded what remains [21 Mar 2024]
Created [16 Feb 2024]