Lemma 16 (Soundness of the ρ rule)
V((hXi ^ Piii(P))*,a) = V(([hXi ^ Piii(Pk)/Xk],n=ιP)*,a)
Proof. Directly from Lemma 8 and Proposition 10. □
Proposition 17 (Soundness of C) P1 'C P2 ⇒ V(Pι,a) ⊆ V(P2,α)
Proof. The proof proceeds by induction on the length of the derivation of P2
from P1 . □
We now come to a series of five lemmas which are of a more technical nature.
They are needed for the proof of Theorem 23 below. Let us begin with three
simple lemmas of a proof-theoretical nature. Lemma 18 says that a program
P can only derive a sequence P1 ; P2 if P can be split into two parts which
derive P1 and P2 respectively; lemma 20 establishes a useful substitution
property and uses lemma 19 for its proof.
Lemma 18 P 'C P1; P2 iff there are P10 and P22 such that P = P10; P22, P11 'C
Pi and P22 'C P2.
Proof. A straightforward induction on length of derivation. □
Lemma 19 Let i and` range over {1, . . . , n} and let k range over {1, . . . , m},
then
1. [Pk/Xk]k (Q1 ∪ Q2) follows from [Pk/Xk]k Q1 and from [Pk/Xk]k Q2 by
the ∪ rule;
2. [Pk/Xk]k hY ^ Qiii(Q) follows from [Pk/Xk]k [hY ^ Qfii(Qf)/Y']' Q
by the ρ rule.
Proof. The first statement is trivial, so we prove the second. Let Z1, . . . , Zm
be the first variables in some given ordering which do not occur in any of
the Pk, in (Yi ^ Qiii(Q), or in any of the Xk. For any P, abbreviate
[Pk/Yk]k [Z'/Y']' P as P0. We have
[Pk/Xk]k [hYi ^ Qfii(Qf)/Y']' Q =
[Pk/Xk]k [hYi ^ Qiii(Q')/Z']` [Z'/Y']' Q = by Lemma 1
[[Pk/Xk]k Y ^ Qiii(Q')/Z']' Q0 = by Definition 3
[hzi ^ Qiii(Q')/Z']' Q0
This means that [Pk/Xk]k (Yi ^ Qiii(Q), which by definition is (Zi ^
Qiii(Q0), follows from [Pk/Xk]k [hYi ^ Qfii(Q'i/Yf]' Q by the P rule. □
27