The Union Theorem can now be proved. It was already clear that execution
of some program P must consist in execution of some L such that L 'C P
and, conversely, that execution of any such L amounts to execution of P .
The theorem shows that this squares with the modeltheoretic interpretation
of programs which we have obtained by our translation and in this way
provides a justification for that translation.
Theorem 23 (Union Theorem) VM(Pt, a) = S{VM(Lt,a) | L 'C P} for
all models M and assignments a.
Proof. That S{V (Lt,a) | L 'C P} ⊆ V (Pt, a) follows from Proposition 17.
We prove the reverse, the statement that V (Pt, a) ⊆ S{V (Lt,a) | L 'C P},
by induction on the complexity of P. In case P is atomic the only L such
that L 'C P is P itself, so the statement is trivially true. In case P is P1 ∪ P2
or P is P1 ; P2 and the statement holds for P1 and P2, we can easily derive
the statement for P itself. This leaves it for us to prove that
V((<Xi ^ Pii'=ι(Pn+ι))t, a) ⊆ [{V(Lt,a) | L 'C <Xi ^ Pi)'=ι(P,,+ι)}
under the induction hypothesis (*) that for all k (1 ≤ k ≤ n + 1) V(Pkt, a) ⊆
S{V(Lt, a) | L 'C Pk } for all assignments a. In fact, we shall strengthen the
statement somewhat and use the induction hypothesis to prove that
V((hXi ^ Piii=ι(Pk))t,a) ⊆ [{V(Lt,a) | L 'C <Xi ^ Pi‰(Pk)}
for all k (1 ≤ k ≤ n + 1). To this end, define relations Rkm for all m ∈
N by setting Rf0k = 0 and Rf+1 = V(Pkt,a[Rm/X1,..., Rf∕Xn]). Using a
subinduction on m we prove that Rf ⊆ S{V(Lt, a) | L 'C <Xi ^ Pi}f=1(Pk)}
for all m and k (1 ≤ k ≤ n+ 1). Since this is trivially true for m = 0, suppose
(**) the statement holds for m. The induction hypothesis (*) gives us that
Rkm+1 = V(Pkt, a[R1m/X1,..., Rnm/Xn])
⊆ [{V(L0t, a[R1m/X1,..., Rnm/Xn]) |L0'CPk}
On the other hand, Lemma 22 in combination with the subinduction hypoth-
esis (**) tells us that, for any linear program L0:
V (L0t, a[R1m/X1,..., Rnm/Xn]) ⊆
[{V(Lt,a) | L 'C [<Xi ^ Piin=ι(Pj)/Xj]n=ιL0}
29