Exercises identified by number are from the Gries & Schneider text. Of course, in proving a numbered theorem, you may use only lower-numbered theorems.
A1. Supply a proof of Theorem Body Weakening/Strengthening (9.11):
A2. Supply a proof of Theorem Monotonicity of ∀ (9.12):
One approach is to use Shunting (3.65) to rewrite the theorem in a different form, and then to prove that the resulting expression is a theorem.
A3. Supply a proof of Generalized DeMorgan (9.18b):
A4. Supply a proof of Trading (9.19):
A5. Supply a proof of Range weakening (9.25):
A6. Supply a proof (using no theorem numbered higher than (9.18)) of
Provided x does not occur free in Q:
Translate these informal statements into the language of predicate logic. You can define auxiliary functions (including predicates) and make use of them in defining other predicates.
B1. The length of the longest plateau in array b[] is k. (A plateau is an array segment all of whose elements are equal to each other.)
B2. Among all array segments of b[], the sum of the elements in b[low..high) is largest.