author  paulson 
Tue, 09 Jul 2002 23:05:26 +0200  
changeset 13328  703de709a64b 
parent 13269  3ba9be497c33 
child 13356  c9cfe1638bf2 
permissions  rwrr 
1478  1 
(* Title: ZF/epsilon.thy 
0  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

6 
*) 

7 

13328  8 
header{*Epsilon Induction and Recursion*} 
9 

13164  10 
theory Epsilon = Nat + mono: 
11 

2469  12 
constdefs 
13164  13 
eclose :: "i=>i" 
2469  14 
"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))" 
0  15 

13164  16 
transrec :: "[i, [i,i]=>i] =>i" 
2469  17 
"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" 
18 

13164  19 
rank :: "i=>i" 
2469  20 
"rank(a) == transrec(a, %x f. UN y:x. succ(f`y))" 
21 

13164  22 
transrec2 :: "[i, i, [i,i]=>i] =>i" 
2469  23 
"transrec2(k, a, b) == 
24 
transrec(k, 

25 
%i r. if(i=0, a, 

26 
if(EX j. i=succ(j), 

27 
b(THE j. i=succ(j), r`(THE j. i=succ(j))), 

28 
UN j<i. r`j)))" 

29 

13164  30 
recursor :: "[i, [i,i]=>i, i]=>i" 
31 
"recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))" 

32 

33 
rec :: "[i, i, [i,i]=>i]=>i" 

34 
"rec(k,a,b) == recursor(a,b,k)" 

35 

36 

37 
(*** Basic closure properties ***) 

38 

39 
lemma arg_subset_eclose: "A <= eclose(A)" 

40 
apply (unfold eclose_def) 

41 
apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans]) 

42 
apply (rule nat_0I [THEN UN_upper]) 

43 
done 

44 

45 
lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard] 

46 

47 
lemma Transset_eclose: "Transset(eclose(A))" 

48 
apply (unfold eclose_def Transset_def) 

49 
apply (rule subsetI [THEN ballI]) 

50 
apply (erule UN_E) 

51 
apply (rule nat_succI [THEN UN_I], assumption) 

52 
apply (erule nat_rec_succ [THEN ssubst]) 

53 
apply (erule UnionI, assumption) 

54 
done 

55 

56 
(* x : eclose(A) ==> x <= eclose(A) *) 

57 
lemmas eclose_subset = 

58 
Transset_eclose [unfolded Transset_def, THEN bspec, standard] 

59 

60 
(* [ A : eclose(B); c : A ] ==> c : eclose(B) *) 

61 
lemmas ecloseD = eclose_subset [THEN subsetD, standard] 

62 

63 
lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD] 

64 
lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard] 

65 

66 
(* This is epsiloninduction for eclose(A); see also eclose_induct_down... 

67 
[ a: eclose(A); !!x. [ x: eclose(A); ALL y:x. P(y) ] ==> P(x) 

68 
] ==> P(a) 

69 
*) 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

70 
lemmas eclose_induct = 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

71 
Transset_induct [OF _ Transset_eclose, induct set: eclose] 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

72 

13164  73 

74 
(*Epsilon induction*) 

75 
lemma eps_induct: 

76 
"[ !!x. ALL y:x. P(y) ==> P(x) ] ==> P(a)" 

77 
by (rule arg_in_eclose_sing [THEN eclose_induct], blast) 

78 

79 

80 
(*** Leastness of eclose ***) 

81 

82 
(** eclose(A) is the least transitive set including A as a subset. **) 

83 

84 
lemma eclose_least_lemma: 

85 
"[ Transset(X); A<=X; n: nat ] ==> nat_rec(n, A, %m r. Union(r)) <= X" 

86 
apply (unfold Transset_def) 

87 
apply (erule nat_induct) 

88 
apply (simp add: nat_rec_0) 

89 
apply (simp add: nat_rec_succ, blast) 

90 
done 

91 

92 
lemma eclose_least: 

93 
"[ Transset(X); A<=X ] ==> eclose(A) <= X" 

94 
apply (unfold eclose_def) 

95 
apply (rule eclose_least_lemma [THEN UN_least], assumption+) 

96 
done 

97 

98 
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*) 

99 
lemma eclose_induct_down: 

100 
"[ a: eclose(b); 

101 
!!y. [ y: b ] ==> P(y); 

102 
!!y z. [ y: eclose(b); P(y); z: y ] ==> P(z) 

103 
] ==> P(a)" 

104 
apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"]) 

105 
prefer 3 apply assumption 

106 
apply (unfold Transset_def) 

107 
apply (blast intro: ecloseD) 

108 
apply (blast intro: arg_subset_eclose [THEN subsetD]) 

109 
done 

110 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

111 
(*fixed up for induct method*) 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

112 
lemmas eclose_induct_down = eclose_induct_down [consumes 1] 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

113 

13164  114 
lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X" 
115 
apply (erule equalityI [OF eclose_least arg_subset_eclose]) 

116 
apply (rule subset_refl) 

117 
done 

118 

119 

120 
(*** Epsilon recursion ***) 

121 

122 
(*Unused...*) 

123 
lemma mem_eclose_trans: "[ A: eclose(B); B: eclose(C) ] ==> A: eclose(C)" 

124 
by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD], 

125 
assumption+) 

126 

127 
(*Variant of the previous lemma in a useable form for the sequel*) 

128 
lemma mem_eclose_sing_trans: 

129 
"[ A: eclose({B}); B: eclose({C}) ] ==> A: eclose({C})" 

130 
by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD], 

131 
assumption+) 

132 

133 
lemma under_Memrel: "[ Transset(i); j:i ] ==> Memrel(i)``{j} = j" 

134 
by (unfold Transset_def, blast) 

135 

13217  136 
lemma lt_Memrel: "j < i ==> Memrel(i) `` {j} = j" 
137 
by (simp add: lt_def Ord_def under_Memrel) 

138 

13164  139 
(* j : eclose(A) ==> Memrel(eclose(A)) `` j = j *) 
140 
lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard] 

141 

142 
lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst] 

143 

144 
lemma wfrec_eclose_eq: 

145 
"[ k:eclose({j}); j:eclose({i}) ] ==> 

146 
wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)" 

147 
apply (erule eclose_induct) 

148 
apply (rule wfrec_ssubst) 

149 
apply (rule wfrec_ssubst) 

150 
apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i]) 

151 
done 

152 

153 
lemma wfrec_eclose_eq2: 

154 
"k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)" 

155 
apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq]) 

156 
apply (erule arg_into_eclose_sing) 

157 
done 

158 

159 
lemma transrec: "transrec(a,H) = H(a, lam x:a. transrec(x,H))" 

160 
apply (unfold transrec_def) 

161 
apply (rule wfrec_ssubst) 

162 
apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose) 

163 
done 

164 

165 
(*Avoids explosions in proofs; resolve it with a metalevel definition.*) 

166 
lemma def_transrec: 

167 
"[ !!x. f(x)==transrec(x,H) ] ==> f(a) = H(a, lam x:a. f(x))" 

168 
apply simp 

169 
apply (rule transrec) 

170 
done 

171 

172 
lemma transrec_type: 

173 
"[ !!x u. [ x:eclose({a}); u: Pi(x,B) ] ==> H(x,u) : B(x) ] 

174 
==> transrec(a,H) : B(a)" 

175 
apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct]) 

176 
apply (subst transrec) 

177 
apply (simp add: lam_type) 

178 
done 

179 

180 
lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) <= succ(i)" 

181 
apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least]) 

182 
apply (rule succI1 [THEN singleton_subsetI]) 

183 
done 

184 

13269  185 
lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})" 
186 
apply (insert arg_subset_eclose [of "{i}"], simp) 

187 
apply (frule eclose_subset, blast) 

188 
done 

189 

190 
lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)" 

191 
apply (rule equalityI) 

192 
apply (erule eclose_sing_Ord) 

193 
apply (rule succ_subset_eclose_sing) 

194 
done 

195 

13164  196 
lemma Ord_transrec_type: 
197 
assumes jini: "j: i" 

198 
and ordi: "Ord(i)" 

199 
and minor: " !!x u. [ x: i; u: Pi(x,B) ] ==> H(x,u) : B(x)" 

200 
shows "transrec(j,H) : B(j)" 

201 
apply (rule transrec_type) 

202 
apply (insert jini ordi) 

203 
apply (blast intro!: minor 

204 
intro: Ord_trans 

205 
dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD]) 

206 
done 

207 

208 
(*** Rank ***) 

209 

210 
(*NOT SUITABLE FOR REWRITING  RECURSIVE!*) 

211 
lemma rank: "rank(a) = (UN y:a. succ(rank(y)))" 

212 
by (subst rank_def [THEN def_transrec], simp) 

213 

214 
lemma Ord_rank [simp]: "Ord(rank(a))" 

215 
apply (rule_tac a="a" in eps_induct) 

216 
apply (subst rank) 

217 
apply (rule Ord_succ [THEN Ord_UN]) 

218 
apply (erule bspec, assumption) 

219 
done 

220 

221 
lemma rank_of_Ord: "Ord(i) ==> rank(i) = i" 

222 
apply (erule trans_induct) 

223 
apply (subst rank) 

224 
apply (simp add: Ord_equality) 

225 
done 

226 

227 
lemma rank_lt: "a:b ==> rank(a) < rank(b)" 

228 
apply (rule_tac a1 = "b" in rank [THEN ssubst]) 

229 
apply (erule UN_I [THEN ltI]) 

230 
apply (rule_tac [2] Ord_UN, auto) 

231 
done 

232 

233 
lemma eclose_rank_lt: "a: eclose(b) ==> rank(a) < rank(b)" 

234 
apply (erule eclose_induct_down) 

235 
apply (erule rank_lt) 

236 
apply (erule rank_lt [THEN lt_trans], assumption) 

237 
done 

6070  238 

13164  239 
lemma rank_mono: "a<=b ==> rank(a) le rank(b)" 
240 
apply (rule subset_imp_le) 

241 
apply (subst rank) 

242 
apply (subst rank, auto) 

243 
done 

244 

245 
lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))" 

246 
apply (rule rank [THEN trans]) 

247 
apply (rule le_anti_sym) 

248 
apply (rule_tac [2] UN_upper_le) 

249 
apply (rule UN_least_le) 

250 
apply (auto intro: rank_mono simp add: Ord_UN) 

251 
done 

252 

253 
lemma rank_0 [simp]: "rank(0) = 0" 

254 
by (rule rank [THEN trans], blast) 

255 

256 
lemma rank_succ [simp]: "rank(succ(x)) = succ(rank(x))" 

257 
apply (rule rank [THEN trans]) 

258 
apply (rule equalityI [OF UN_least succI1 [THEN UN_upper]]) 

259 
apply (erule succE, blast) 

260 
apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset]) 

261 
done 

262 

263 
lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))" 

264 
apply (rule equalityI) 

265 
apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least]) 

266 
apply (erule_tac [2] Union_upper) 

267 
apply (subst rank) 

268 
apply (rule UN_least) 

269 
apply (erule UnionE) 

270 
apply (rule subset_trans) 

271 
apply (erule_tac [2] RepFunI [THEN Union_upper]) 

272 
apply (erule rank_lt [THEN succ_leI, THEN le_imp_subset]) 

273 
done 

274 

275 
lemma rank_eclose: "rank(eclose(a)) = rank(a)" 

276 
apply (rule le_anti_sym) 

277 
apply (rule_tac [2] arg_subset_eclose [THEN rank_mono]) 

278 
apply (rule_tac a1 = "eclose (a) " in rank [THEN ssubst]) 

279 
apply (rule Ord_rank [THEN UN_least_le]) 

280 
apply (erule eclose_rank_lt [THEN succ_leI]) 

281 
done 

282 

283 
lemma rank_pair1: "rank(a) < rank(<a,b>)" 

284 
apply (unfold Pair_def) 

285 
apply (rule consI1 [THEN rank_lt, THEN lt_trans]) 

286 
apply (rule consI1 [THEN consI2, THEN rank_lt]) 

287 
done 

288 

289 
lemma rank_pair2: "rank(b) < rank(<a,b>)" 

290 
apply (unfold Pair_def) 

291 
apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans]) 

292 
apply (rule consI1 [THEN consI2, THEN rank_lt]) 

293 
done 

294 

295 
(*Not clear how to remove the P(a) condition, since the "then" part 

296 
must refer to "a"*) 

297 
lemma the_equality_if: 

298 
"P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)" 

299 
by (simp add: the_0 the_equality2) 

300 

13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

301 
(*The first premise not only fixs i but ensures f~=0. 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

302 
The second premise is now essential. Consider otherwise the relation 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

303 
r = {<0,0>,<0,1>,<0,2>,...}. Then f`0 = Union(f``{0}) = Union(nat) = nat, 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

304 
whose rank equals that of r.*) 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

305 
lemma rank_apply: "[i : domain(f); function(f)] ==> rank(f`i) < rank(f)" 
13269  306 
apply clarify 
307 
apply (simp add: function_apply_equality) 

13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

308 
apply (blast intro: lt_trans rank_lt rank_pair2) 
13164  309 
done 
310 

311 

312 
(*** Corollaries of leastness ***) 

313 

314 
lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)" 

315 
apply (rule Transset_eclose [THEN eclose_least]) 

316 
apply (erule arg_into_eclose [THEN eclose_subset]) 

317 
done 

318 

319 
lemma eclose_mono: "A<=B ==> eclose(A) <= eclose(B)" 

320 
apply (rule Transset_eclose [THEN eclose_least]) 

321 
apply (erule subset_trans) 

322 
apply (rule arg_subset_eclose) 

323 
done 

324 

325 
(** Idempotence of eclose **) 

326 

327 
lemma eclose_idem: "eclose(eclose(A)) = eclose(A)" 

328 
apply (rule equalityI) 

329 
apply (rule eclose_least [OF Transset_eclose subset_refl]) 

330 
apply (rule arg_subset_eclose) 

331 
done 

332 

333 
(** Transfinite recursion for definitions based on the 

334 
three cases of ordinals **) 

335 

336 
lemma transrec2_0 [simp]: "transrec2(0,a,b) = a" 

337 
by (rule transrec2_def [THEN def_transrec, THEN trans], simp) 

338 

339 
lemma transrec2_succ [simp]: "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))" 

340 
apply (rule transrec2_def [THEN def_transrec, THEN trans]) 

341 
apply (simp add: the_equality if_P) 

342 
done 

343 

344 
lemma transrec2_Limit: 

345 
"Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))" 

13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13164
diff
changeset

346 
apply (rule transrec2_def [THEN def_transrec, THEN trans]) 
13269  347 
apply (auto simp add: OUnion_def) 
13164  348 
done 
349 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

350 
lemma def_transrec2: 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

351 
"(!!x. f(x)==transrec2(x,a,b)) 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

352 
==> f(0) = a & 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

353 
f(succ(i)) = b(i, f(i)) & 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

354 
(Limit(K) > f(K) = (UN j<K. f(j)))" 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

355 
by (simp add: transrec2_Limit) 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset

356 

13164  357 

358 
(** recursor  better than nat_rec; the succ case has no type requirement! **) 

359 

360 
(*NOT suitable for rewriting*) 

361 
lemmas recursor_lemma = recursor_def [THEN def_transrec, THEN trans] 

362 

363 
lemma recursor_0: "recursor(a,b,0) = a" 

364 
by (rule nat_case_0 [THEN recursor_lemma]) 

365 

366 
lemma recursor_succ: "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))" 

367 
by (rule recursor_lemma, simp) 

368 

369 

370 
(** rec: old version for compatibility **) 

371 

372 
lemma rec_0 [simp]: "rec(0,a,b) = a" 

373 
apply (unfold rec_def) 

374 
apply (rule recursor_0) 

375 
done 

376 

377 
lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))" 

378 
apply (unfold rec_def) 

379 
apply (rule recursor_succ) 

380 
done 

381 

382 
lemma rec_type: 

383 
"[ n: nat; 

384 
a: C(0); 

385 
!!m z. [ m: nat; z: C(m) ] ==> b(m,z): C(succ(m)) ] 

386 
==> rec(n,a,b) : C(n)" 

13185  387 
by (erule nat_induct, auto) 
13164  388 

389 
ML 

390 
{* 

391 
val arg_subset_eclose = thm "arg_subset_eclose"; 

392 
val arg_into_eclose = thm "arg_into_eclose"; 

393 
val Transset_eclose = thm "Transset_eclose"; 

394 
val eclose_subset = thm "eclose_subset"; 

395 
val ecloseD = thm "ecloseD"; 

396 
val arg_in_eclose_sing = thm "arg_in_eclose_sing"; 

397 
val arg_into_eclose_sing = thm "arg_into_eclose_sing"; 

398 
val eclose_induct = thm "eclose_induct"; 

399 
val eps_induct = thm "eps_induct"; 

400 
val eclose_least = thm "eclose_least"; 

401 
val eclose_induct_down = thm "eclose_induct_down"; 

402 
val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg"; 

403 
val mem_eclose_trans = thm "mem_eclose_trans"; 

404 
val mem_eclose_sing_trans = thm "mem_eclose_sing_trans"; 

405 
val under_Memrel = thm "under_Memrel"; 

406 
val under_Memrel_eclose = thm "under_Memrel_eclose"; 

407 
val wfrec_ssubst = thm "wfrec_ssubst"; 

408 
val wfrec_eclose_eq = thm "wfrec_eclose_eq"; 

409 
val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2"; 

410 
val transrec = thm "transrec"; 

411 
val def_transrec = thm "def_transrec"; 

412 
val transrec_type = thm "transrec_type"; 

413 
val eclose_sing_Ord = thm "eclose_sing_Ord"; 

414 
val Ord_transrec_type = thm "Ord_transrec_type"; 

415 
val rank = thm "rank"; 

416 
val Ord_rank = thm "Ord_rank"; 

417 
val rank_of_Ord = thm "rank_of_Ord"; 

418 
val rank_lt = thm "rank_lt"; 

419 
val eclose_rank_lt = thm "eclose_rank_lt"; 

420 
val rank_mono = thm "rank_mono"; 

421 
val rank_Pow = thm "rank_Pow"; 

422 
val rank_0 = thm "rank_0"; 

423 
val rank_succ = thm "rank_succ"; 

424 
val rank_Union = thm "rank_Union"; 

425 
val rank_eclose = thm "rank_eclose"; 

426 
val rank_pair1 = thm "rank_pair1"; 

427 
val rank_pair2 = thm "rank_pair2"; 

428 
val the_equality_if = thm "the_equality_if"; 

429 
val rank_apply = thm "rank_apply"; 

430 
val mem_eclose_subset = thm "mem_eclose_subset"; 

431 
val eclose_mono = thm "eclose_mono"; 

432 
val eclose_idem = thm "eclose_idem"; 

433 
val transrec2_0 = thm "transrec2_0"; 

434 
val transrec2_succ = thm "transrec2_succ"; 

435 
val transrec2_Limit = thm "transrec2_Limit"; 

436 
val recursor_0 = thm "recursor_0"; 

437 
val recursor_succ = thm "recursor_succ"; 

438 
val rec_0 = thm "rec_0"; 

439 
val rec_succ = thm "rec_succ"; 

440 
val rec_type = thm "rec_type"; 

441 
*} 

6070  442 

0  443 
end 