Lemma 20 If Q 'c Q0 then [Pk/Xk]fe Q 'c [Pk/Xk]fe Q0.
Proof. Let Q1 , . . . , Qn be a derivation of Q0 from Q. It follows immediately
from the previous lemma that, for 1 ≤ i ≤ n, [Pk/Xk]k Qi+1 is an immediate
consequence of [Pk/Xk]k Qi. Hence [Pk/Xk]k Q1, . . . , [Pk/Xk]k Qn is a deriva-
tion of [Pk/Xk]k Q0 from [Pk/Xk]fc Q. □
The next two lemmas establish properties of the union of the denotations of
all linear programs deriving a given program.
Lemma 21 If Ri ⊆ S{V (Lj1 ,α) | Li 'c Qi} and R2 ⊆ S{V (L2,α) | L2 'c
Q2} then Ri ◦ R2 ⊆ S{V(Lt, a) | L 'c Qi; Q2}
Proof. From the assumptions and the translation of Li ; L2 it follows that
Ri ◦ R2 ⊆ [{V(L1,α) ◦V(L1,a) | Li 'c Qi,Li 'c Q2}
= [{V((Li; L2)t, a) | Li 'c Qi, Li 'c Q2}
But since Lemma 18 tells us that L 'c Qi; Q2 iff there are Li and L2 such
that L = Li; L2 while Li 'c Qi and L2 'c Q2, the latter term is equal to
S{V(Lt, a) | L 'c Qi;Q2}. □
Lemma 22 Suppose Rk ⊆ S{V (Lt , a) | L 'c Qk} for all k (1 ≤ k ≤ n).
Then for all linear programs L:
V(Lt,a[Ri/Xi,...,Rn/Xn]) ⊆[{V(L0t,a) | L0 'c [Qi/Xi,..., Qn/Xn]L}
Proof. This follows by induction on the number m of occurrences of the
variables Xi , . . . , Xn in L. If m = 0 the statement reduces to V (Lt , a) ⊆
S{V (L0t, a) | L0 'c L}, which is obviously true. If m > 0 then L has the
form Li ; Xk; L2, with fewer than m occurrences of Xi , . . . , Xn in Li and L2.
Write a0 for a[Ri/Xi , . . . , Rn/Xn]. Then
V(Lt, a0) = V(Li, a0) ◦ Rk ◦ V(l2, a0).
From the induction hypothesis it follows that
V(Lit,a0) ⊆ [{V(L0t,a) | L0 'c [Qi/Xi,..., Qn/Xn]Li}
for i ∈ {1, 2}. This, together with the assumption Rk ⊆ S{V (Lt, a) | L 'c
Qk} and Lemma 21 allows us to draw the desired conclusion that
V(Lt,a0) ⊆ [{V(L0t,a) | L0 'c [Qi/Xi,..., Qn/Xn]Li; Xk; L2}
□
28