This directory is not related to the soundness and completeness proofs developed for the three strategies. Rather, we exhibit trivial machines, in which we can satisfy Manolios and Moore's characterization of partial correctness. The key is that the machine essentially ignores the program, but sets its state to a certain constant value and then halts. Suppose we now want to prove a routine correct where the routine does not end in a halting state and makes some nontrivial modifications defined by a function modify. Manolios and Moore's notion says that we need to prove the following theorem. (implies (pre s) (= (stepw s) (stepw (modify s)))) But the condition does not guarantee that the machine ever reaches a state (modify s) from s, merely that from s and (modify s) we can reach the same halting state (if one exists, which it does in every case here). So if the machine essentially ignores the program and memory and everything else, and merely halts with a constant value for the state then that condition is satisfied in this case.