for each ` ∈ N ∪ {ω}, each m ∈ N and each k (1 ≤ k ≤ n) the relation
R. by setting R0,k = 0 and Rmk+1 = V(Ak, α[Rm√Xι,..., Rmn∕Xn, R'∕ξ])•
Then R0k ⊆ R'k ⊆ ... ⊆ Rnk ⊆ ... for each k and '. Moreover, it
,, ,
is easily proved by induction on m, using the monotonicity of the Ak and
the definition of Rmk that Rmk ⊆ Rm+1,k if ' ∈ N, so that we also have
chains Rmk ⊆ Rmk ⊆ ... ⊆ Rmk ⊆ .... We prove by induction on m that
S' Rmk = Rmk. This is trivial for m = 0. Suppose the statement holds for
m. Then, using the continuity of the Ak and the induction hypothesis, we
find that
R'm,k+1 =
'
[ V(Ak, a[Rm1∕X1,..., Rm/Xn, R'∕ξ]) =
'
V(Ak,a
U Rm1∕X1,... ,∪ Rmn/Xn, U R'∕ξ ) =
' ''
V(Ak, a Rωm,1∕X1,..., Rωm,n∕Xn, Rω ∕ξ ) =
Rωm,+k 1
Since Rωω,k = m ' R'm,k = ' m R'm,k it follows that (*) Rωω,k = 'R'ω,k. Now
we reason as follows, using Lemma 8 twice and using (*) and the continuity
of B in ξ
[V(λr.∀X1 .. .Xn(^n Xi = Ai → B(r)), a[R'∕ξ]) =
' i=1
[ V(B, a[R'ω,1∕X1,..., R'ω,n∕Xn, R'∕ξ]) =
'
V(B, a
R'ω,1∕X1,..., R'ω,n∕Xn, R'∕ξ
)=
' ''
V(B,a Rωω,1∕X1,..., Rωω,n∕Xn, Rω∕ξ ) =
V(λr.∀X1...Xn(^n Xi =Ai → B(r)), a[Rω ∕ξ])
i=1
This concludes the proof □
That translations of programs are continuous is now easily proved. The
proposition will allow us to apply the Knaster-Tarski theorem to those trans-
lations.
21
More intriguing information
1. Cultural Neuroeconomics of Intertemporal Choice2. The name is absent
3. Fiscal Reform and Monetary Union in West Africa
4. References
5. How Offshoring Can Affect the Industries’ Skill Composition
6. sycnoιogιcaι spaces
7. The name is absent
8. Short- and long-term experience in pulmonary vein segmental ostial ablation for paroxysmal atrial fibrillation*
9. Protocol for Past BP: a randomised controlled trial of different blood pressure targets for people with a history of stroke of transient ischaemic attack (TIA) in primary care
10. Unemployment in an Interdependent World