Global Optimality Theorem

Intuitively, at any given time $p$ should execute some self-modification algorithm (via instruction check()--Item 5 above) only if it is the `best' of all possible self-modifications, given the utility function, which typically depends on available resources, such as storage size and remaining lifetime. At first glance, however, target theorem (2) seems to implicitly talk about just one single modification algorithm, namely, switchprog$(t_1)$ as set by the systematic proof searcher at time $t_1$. Isn't this type of local search greedy? Couldn't it lead to a local optimum instead of a global one? No, it cannot, according to the following global optimality theorem.