13 - The strong preorder

Summary

In this chapter we fulfil the remaining proof obligations of Chapter 12. Section 13.1 contains a strengthened version of Theorem 4(8), our version of the theorem of Knaster-Tarski. In Section 13.2, we provide the basic set-up, in which we need not yet distinguish between wp and wlp. Section 13.3 contains the construction of the strong preorder and the proofs of rule 12(4) and a variation of rule 12(5). In this way, the proof of the accumulation rule 12(5) is reduced to the verification of two technical conditions: sup-safety (for wp) and inf-safety (for wlp). These conditions comprise the base case of the induction and a continuity property.

In Section 13.4, the base case is reduced to a condition on function abort^⊙. Section 13.5 contains the proof for inf-safety. Section 13.6 contains the definition of the set Lia and the proof for sup-safety. In Sections 13.7 and 13.8 we justify the rules for Lia stated in Section 11.2.

It may seem unsatisfactory that, in the presence of unbounded nondeterminacy, computational induction needs such a complicated theory. The examples in Sections 11.7 and 12.4, however, show that the accumulation rules 11(6) and 12(5) need their complicated conditions. Therefore, corresponding complications must occur in the construction or in the proofs.