author | paulson |
Mon, 04 Oct 2004 15:25:28 +0200 | |
changeset 15227 | 804ecdc08cf2 |
parent 13454 | 01e2496dee05 |
child 16218 | ea49a9c7ff7c |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/ex/hoare.ML |
244 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
4 |
Copyright 1993 Technische Universitaet Muenchen |
|
244 | 5 |
*) |
6 |
||
7 |
(* --------- pure HOLCF logic, some little lemmas ------ *) |
|
8 |
||
9265 | 9 |
Goal "b~=TT ==> b=FF | b=UU"; |
10 |
by (rtac (Exh_tr RS disjE) 1); |
|
11 |
by (fast_tac HOL_cs 1); |
|
12 |
by (etac disjE 1); |
|
13 |
by (contr_tac 1); |
|
14 |
by (fast_tac HOL_cs 1); |
|
15 |
qed "hoare_lemma2"; |
|
244 | 16 |
|
10835 | 17 |
Goal " (ALL k. b1$(iterate k g x) = TT) | (EX k. b1$(iterate k g x)~=TT)"; |
9265 | 18 |
by (fast_tac HOL_cs 1); |
19 |
qed "hoare_lemma3"; |
|
244 | 20 |
|
10835 | 21 |
Goal "(EX k. b1$(iterate k g x) ~= TT) ==> \ |
22 |
\ EX k. b1$(iterate k g x) = FF | b1$(iterate k g x) = UU"; |
|
9265 | 23 |
by (etac exE 1); |
24 |
by (rtac exI 1); |
|
25 |
by (rtac hoare_lemma2 1); |
|
26 |
by (atac 1); |
|
27 |
qed "hoare_lemma4"; |
|
244 | 28 |
|
10835 | 29 |
Goal "[|(EX k. b1$(iterate k g x) ~= TT);\ |
30 |
\ k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \ |
|
31 |
\ b1$(iterate k g x)=FF | b1$(iterate k g x)=UU"; |
|
9265 | 32 |
by (hyp_subst_tac 1); |
33 |
by (rtac hoare_lemma2 1); |
|
34 |
by (etac exE 1); |
|
35 |
by (etac LeastI 1); |
|
36 |
qed "hoare_lemma5"; |
|
244 | 37 |
|
9265 | 38 |
Goal "b=UU ==> b~=TT"; |
39 |
by (hyp_subst_tac 1); |
|
40 |
by (resolve_tac dist_eq_tr 1); |
|
41 |
qed "hoare_lemma6"; |
|
42 |
||
43 |
Goal "b=FF ==> b~=TT"; |
|
44 |
by (hyp_subst_tac 1); |
|
45 |
by (resolve_tac dist_eq_tr 1); |
|
46 |
qed "hoare_lemma7"; |
|
244 | 47 |
|
10835 | 48 |
Goal "[|(EX k. b1$(iterate k g x) ~= TT);\ |
49 |
\ k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \ |
|
50 |
\ ALL m. m < k --> b1$(iterate m g x)=TT"; |
|
9265 | 51 |
by (hyp_subst_tac 1); |
52 |
by (etac exE 1); |
|
53 |
by (strip_tac 1); |
|
10835 | 54 |
by (res_inst_tac [("p","b1$(iterate m g x)")] trE 1); |
9265 | 55 |
by (atac 2); |
56 |
by (rtac (le_less_trans RS less_irrefl) 1); |
|
57 |
by (atac 2); |
|
58 |
by (rtac Least_le 1); |
|
59 |
by (etac hoare_lemma6 1); |
|
60 |
by (rtac (le_less_trans RS less_irrefl) 1); |
|
61 |
by (atac 2); |
|
62 |
by (rtac Least_le 1); |
|
63 |
by (etac hoare_lemma7 1); |
|
64 |
qed "hoare_lemma8"; |
|
244 | 65 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
66 |
|
10835 | 67 |
Goal "f$(y::'a)=(UU::tr) ==> f$UU = UU"; |
9265 | 68 |
by (etac (flat_codom RS disjE) 1); |
69 |
by Auto_tac; |
|
70 |
qed "hoare_lemma28"; |
|
244 | 71 |
|
72 |
||
73 |
(* ----- access to definitions ----- *) |
|
74 |
||
10835 | 75 |
Goal "p$x = If b1$x then p$(g$x) else x fi"; |
9265 | 76 |
by (fix_tac3 p_def 1); |
77 |
by (Simp_tac 1); |
|
78 |
qed "p_def3"; |
|
244 | 79 |
|
10835 | 80 |
Goal "q$x = If b1$x orelse b2$x then q$(g$x) else x fi"; |
9265 | 81 |
by (fix_tac3 q_def 1); |
82 |
by (Simp_tac 1); |
|
83 |
qed "q_def3"; |
|
244 | 84 |
|
85 |
(** --------- proves about iterations of p and q ---------- **) |
|
86 |
||
10835 | 87 |
Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\ |
88 |
\ p$(iterate k g x)=p$x"; |
|
13454 | 89 |
by (induct_tac "k" 1); |
9265 | 90 |
by (Simp_tac 1); |
91 |
by (Simp_tac 1); |
|
92 |
by (strip_tac 1); |
|
13454 | 93 |
by (res_inst_tac [("s","p$(iterate n g x)")] trans 1); |
9265 | 94 |
by (rtac trans 1); |
95 |
by (rtac (p_def3 RS sym) 2); |
|
13454 | 96 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1); |
9265 | 97 |
by (rtac mp 1); |
98 |
by (etac spec 1); |
|
99 |
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
|
100 |
by (simp_tac HOLCF_ss 1); |
|
101 |
by (etac mp 1); |
|
102 |
by (strip_tac 1); |
|
103 |
by (rtac mp 1); |
|
104 |
by (etac spec 1); |
|
105 |
by (etac less_trans 1); |
|
106 |
by (Simp_tac 1); |
|
107 |
qed "hoare_lemma9"; |
|
3044
3e3087aa69e7
Updates because nat_ind_tac no longer appends "1" to the ind.var.
nipkow
parents:
2642
diff
changeset
|
108 |
|
10835 | 109 |
Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \ |
110 |
\ q$(iterate k g x)=q$x"; |
|
13454 | 111 |
by (induct_tac "k" 1); |
9265 | 112 |
by (Simp_tac 1); |
113 |
by (simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
|
114 |
by (strip_tac 1); |
|
13454 | 115 |
by (res_inst_tac [("s","q$(iterate n g x)")] trans 1); |
9265 | 116 |
by (rtac trans 1); |
117 |
by (rtac (q_def3 RS sym) 2); |
|
13454 | 118 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate n g x)")] ssubst 1); |
9265 | 119 |
by (fast_tac HOL_cs 1); |
120 |
by (simp_tac HOLCF_ss 1); |
|
121 |
by (etac mp 1); |
|
122 |
by (strip_tac 1); |
|
123 |
by (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1); |
|
124 |
qed "hoare_lemma24"; |
|
244 | 125 |
|
10835 | 126 |
(* -------- results about p for case (EX k. b1$(iterate k g x)~=TT) ------- *) |
244 | 127 |
|
128 |
||
129 |
val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp)); |
|
130 |
(* |
|
10835 | 131 |
val hoare_lemma10 = "[| EX k. b1$(iterate k g ?x1) ~= TT; |
132 |
Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==> |
|
133 |
p$(iterate ?k3 g ?x1) = p$?x1" : thm |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
134 |
|
244 | 135 |
*) |
136 |
||
10835 | 137 |
Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\ |
138 |
\ k=(LEAST n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x)=FF \ |
|
139 |
\ --> p$x = iterate k g x"; |
|
9265 | 140 |
by (case_tac "k" 1); |
141 |
by (hyp_subst_tac 1); |
|
142 |
by (Simp_tac 1); |
|
143 |
by (strip_tac 1); |
|
144 |
by (etac conjE 1); |
|
145 |
by (rtac trans 1); |
|
146 |
by (rtac p_def3 1); |
|
147 |
by (asm_simp_tac HOLCF_ss 1); |
|
148 |
by (hyp_subst_tac 1); |
|
149 |
by (strip_tac 1); |
|
150 |
by (etac conjE 1); |
|
151 |
by (rtac trans 1); |
|
152 |
by (etac (hoare_lemma10 RS sym) 1); |
|
153 |
by (atac 1); |
|
154 |
by (rtac trans 1); |
|
155 |
by (rtac p_def3 1); |
|
10835 | 156 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1); |
9265 | 157 |
by (rtac (hoare_lemma8 RS spec RS mp) 1); |
158 |
by (atac 1); |
|
159 |
by (atac 1); |
|
160 |
by (Simp_tac 1); |
|
161 |
by (simp_tac HOLCF_ss 1); |
|
162 |
by (rtac trans 1); |
|
163 |
by (rtac p_def3 1); |
|
164 |
by (simp_tac (simpset() delsimps [iterate_Suc] addsimps [iterate_Suc RS sym]) 1); |
|
165 |
by (eres_inst_tac [("s","FF")] ssubst 1); |
|
166 |
by (simp_tac HOLCF_ss 1); |
|
167 |
qed "hoare_lemma11"; |
|
244 | 168 |
|
10835 | 169 |
Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\ |
170 |
\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \ |
|
171 |
\ --> p$x = UU"; |
|
9265 | 172 |
by (case_tac "k" 1); |
173 |
by (hyp_subst_tac 1); |
|
174 |
by (Simp_tac 1); |
|
175 |
by (strip_tac 1); |
|
176 |
by (etac conjE 1); |
|
177 |
by (rtac trans 1); |
|
178 |
by (rtac p_def3 1); |
|
179 |
by (asm_simp_tac HOLCF_ss 1); |
|
180 |
by (hyp_subst_tac 1); |
|
181 |
by (Simp_tac 1); |
|
182 |
by (strip_tac 1); |
|
183 |
by (etac conjE 1); |
|
184 |
by (rtac trans 1); |
|
185 |
by (rtac (hoare_lemma10 RS sym) 1); |
|
186 |
by (atac 1); |
|
187 |
by (atac 1); |
|
188 |
by (rtac trans 1); |
|
189 |
by (rtac p_def3 1); |
|
10835 | 190 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1); |
9265 | 191 |
by (rtac (hoare_lemma8 RS spec RS mp) 1); |
192 |
by (atac 1); |
|
193 |
by (atac 1); |
|
194 |
by (Simp_tac 1); |
|
195 |
by (asm_simp_tac HOLCF_ss 1); |
|
196 |
by (rtac trans 1); |
|
197 |
by (rtac p_def3 1); |
|
198 |
by (asm_simp_tac HOLCF_ss 1); |
|
199 |
qed "hoare_lemma12"; |
|
244 | 200 |
|
10835 | 201 |
(* -------- results about p for case (ALL k. b1$(iterate k g x)=TT) ------- *) |
244 | 202 |
|
10835 | 203 |
Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. p$(iterate k g x) = UU"; |
9265 | 204 |
by (rtac (p_def RS def_fix_ind) 1); |
205 |
by (rtac adm_all 1); |
|
206 |
by (rtac allI 1); |
|
207 |
by (rtac adm_eq 1); |
|
208 |
by (cont_tacR 1); |
|
209 |
by (rtac allI 1); |
|
210 |
by (stac strict_Rep_CFun1 1); |
|
211 |
by (rtac refl 1); |
|
212 |
by (Simp_tac 1); |
|
213 |
by (rtac allI 1); |
|
10835 | 214 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); |
9265 | 215 |
by (etac spec 1); |
216 |
by (asm_simp_tac HOLCF_ss 1); |
|
217 |
by (rtac (iterate_Suc RS subst) 1); |
|
218 |
by (etac spec 1); |
|
219 |
qed "fernpass_lemma"; |
|
244 | 220 |
|
10835 | 221 |
Goal "(ALL k. b1$(iterate k g x)=TT) ==> p$x = UU"; |
9265 | 222 |
by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1); |
223 |
by (etac (fernpass_lemma RS spec) 1); |
|
224 |
qed "hoare_lemma16"; |
|
244 | 225 |
|
10835 | 226 |
(* -------- results about q for case (ALL k. b1$(iterate k g x)=TT) ------- *) |
244 | 227 |
|
10835 | 228 |
Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. q$(iterate k g x) = UU"; |
9265 | 229 |
by (rtac (q_def RS def_fix_ind) 1); |
230 |
by (rtac adm_all 1); |
|
231 |
by (rtac allI 1); |
|
232 |
by (rtac adm_eq 1); |
|
233 |
by (cont_tacR 1); |
|
234 |
by (rtac allI 1); |
|
235 |
by (stac strict_Rep_CFun1 1); |
|
236 |
by (rtac refl 1); |
|
237 |
by (rtac allI 1); |
|
238 |
by (Simp_tac 1); |
|
10835 | 239 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1); |
9265 | 240 |
by (etac spec 1); |
241 |
by (asm_simp_tac HOLCF_ss 1); |
|
242 |
by (rtac (iterate_Suc RS subst) 1); |
|
243 |
by (etac spec 1); |
|
244 |
qed "hoare_lemma17"; |
|
244 | 245 |
|
10835 | 246 |
Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$x = UU"; |
9265 | 247 |
by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1); |
248 |
by (etac (hoare_lemma17 RS spec) 1); |
|
249 |
qed "hoare_lemma18"; |
|
250 |
||
10835 | 251 |
Goal "(ALL k. (b1::'a->tr)$(iterate k g x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)"; |
9265 | 252 |
by (rtac (flat_codom) 1); |
253 |
by (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1); |
|
254 |
by (etac spec 1); |
|
255 |
qed "hoare_lemma19"; |
|
244 | 256 |
|
10835 | 257 |
Goal "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k g (x::'a)) = UU"; |
9265 | 258 |
by (rtac (q_def RS def_fix_ind) 1); |
259 |
by (rtac adm_all 1); |
|
260 |
by (rtac allI 1); |
|
261 |
by (rtac adm_eq 1); |
|
262 |
by (cont_tacR 1); |
|
263 |
by (rtac allI 1); |
|
264 |
by (stac strict_Rep_CFun1 1); |
|
265 |
by (rtac refl 1); |
|
266 |
by (rtac allI 1); |
|
267 |
by (Simp_tac 1); |
|
10835 | 268 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1); |
9265 | 269 |
by (etac spec 1); |
270 |
by (asm_simp_tac HOLCF_ss 1); |
|
271 |
by (rtac (iterate_Suc RS subst) 1); |
|
272 |
by (etac spec 1); |
|
273 |
qed "hoare_lemma20"; |
|
244 | 274 |
|
10835 | 275 |
Goal "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU"; |
9265 | 276 |
by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1); |
277 |
by (etac (hoare_lemma20 RS spec) 1); |
|
278 |
qed "hoare_lemma21"; |
|
244 | 279 |
|
10835 | 280 |
Goal "b1$(UU::'a)=UU ==> q$(UU::'a) = UU"; |
9265 | 281 |
by (stac q_def3 1); |
282 |
by (asm_simp_tac HOLCF_ss 1); |
|
283 |
qed "hoare_lemma22"; |
|
244 | 284 |
|
10835 | 285 |
(* -------- results about q for case (EX k. b1$(iterate k g x) ~= TT) ------- *) |
244 | 286 |
|
287 |
val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) ); |
|
288 |
(* |
|
10835 | 289 |
val hoare_lemma25 = "[| EX k. b1$(iterate k g ?x1) ~= TT; |
290 |
Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==> |
|
291 |
q$(iterate ?k3 g ?x1) = q$?x1" : thm |
|
244 | 292 |
*) |
293 |
||
10835 | 294 |
Goal "(EX n. b1$(iterate n g x)~=TT) ==>\ |
295 |
\ k=Least(%n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x) =FF \ |
|
296 |
\ --> q$x = q$(iterate k g x)"; |
|
9265 | 297 |
by (case_tac "k" 1); |
298 |
by (hyp_subst_tac 1); |
|
299 |
by (strip_tac 1); |
|
300 |
by (Simp_tac 1); |
|
301 |
by (hyp_subst_tac 1); |
|
302 |
by (strip_tac 1); |
|
303 |
by (etac conjE 1); |
|
304 |
by (rtac trans 1); |
|
305 |
by (rtac (hoare_lemma25 RS sym) 1); |
|
306 |
by (atac 1); |
|
307 |
by (atac 1); |
|
308 |
by (rtac trans 1); |
|
309 |
by (rtac q_def3 1); |
|
10835 | 310 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1); |
9265 | 311 |
by (rtac (hoare_lemma8 RS spec RS mp) 1); |
312 |
by (atac 1); |
|
313 |
by (atac 1); |
|
314 |
by (Simp_tac 1); |
|
315 |
by (simp_tac HOLCF_ss 1); |
|
316 |
qed "hoare_lemma26"; |
|
244 | 317 |
|
318 |
||
10835 | 319 |
Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\ |
320 |
\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \ |
|
321 |
\ --> q$x = UU"; |
|
9265 | 322 |
by (case_tac "k" 1); |
323 |
by (hyp_subst_tac 1); |
|
324 |
by (Simp_tac 1); |
|
325 |
by (strip_tac 1); |
|
326 |
by (etac conjE 1); |
|
327 |
by (stac q_def3 1); |
|
328 |
by (asm_simp_tac HOLCF_ss 1); |
|
329 |
by (hyp_subst_tac 1); |
|
330 |
by (Simp_tac 1); |
|
331 |
by (strip_tac 1); |
|
332 |
by (etac conjE 1); |
|
333 |
by (rtac trans 1); |
|
334 |
by (rtac (hoare_lemma25 RS sym) 1); |
|
335 |
by (atac 1); |
|
336 |
by (atac 1); |
|
337 |
by (rtac trans 1); |
|
338 |
by (rtac q_def3 1); |
|
10835 | 339 |
by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1); |
9265 | 340 |
by (rtac (hoare_lemma8 RS spec RS mp) 1); |
341 |
by (atac 1); |
|
342 |
by (atac 1); |
|
343 |
by (Simp_tac 1); |
|
344 |
by (asm_simp_tac HOLCF_ss 1); |
|
345 |
by (rtac trans 1); |
|
346 |
by (rtac q_def3 1); |
|
347 |
by (asm_simp_tac HOLCF_ss 1); |
|
348 |
qed "hoare_lemma27"; |
|
244 | 349 |
|
10835 | 350 |
(* ------- (ALL k. b1$(iterate k g x)=TT) ==> q o p = q ----- *) |
244 | 351 |
|
10835 | 352 |
Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$(p$x) = q$x"; |
9265 | 353 |
by (stac hoare_lemma16 1); |
354 |
by (atac 1); |
|
355 |
by (rtac (hoare_lemma19 RS disjE) 1); |
|
356 |
by (atac 1); |
|
357 |
by (stac hoare_lemma18 1); |
|
358 |
by (atac 1); |
|
359 |
by (stac hoare_lemma22 1); |
|
360 |
by (atac 1); |
|
361 |
by (rtac refl 1); |
|
362 |
by (stac hoare_lemma21 1); |
|
363 |
by (atac 1); |
|
364 |
by (stac hoare_lemma21 1); |
|
365 |
by (atac 1); |
|
366 |
by (rtac refl 1); |
|
367 |
qed "hoare_lemma23"; |
|
244 | 368 |
|
9265 | 369 |
(* ------------ EX k. b1~(iterate k g x) ~= TT ==> q o p = q ----- *) |
244 | 370 |
|
10835 | 371 |
Goal "EX k. b1$(iterate k g x) ~= TT ==> q$(p$x) = q$x"; |
9265 | 372 |
by (rtac (hoare_lemma5 RS disjE) 1); |
373 |
by (atac 1); |
|
374 |
by (rtac refl 1); |
|
375 |
by (stac (hoare_lemma11 RS mp) 1); |
|
376 |
by (atac 1); |
|
377 |
by (rtac conjI 1); |
|
378 |
by (rtac refl 1); |
|
379 |
by (atac 1); |
|
380 |
by (rtac (hoare_lemma26 RS mp RS subst) 1); |
|
381 |
by (atac 1); |
|
382 |
by (rtac conjI 1); |
|
383 |
by (rtac refl 1); |
|
384 |
by (atac 1); |
|
385 |
by (rtac refl 1); |
|
386 |
by (stac (hoare_lemma12 RS mp) 1); |
|
387 |
by (atac 1); |
|
388 |
by (rtac conjI 1); |
|
389 |
by (rtac refl 1); |
|
390 |
by (atac 1); |
|
391 |
by (stac hoare_lemma22 1); |
|
392 |
by (stac hoare_lemma28 1); |
|
393 |
by (atac 1); |
|
394 |
by (rtac refl 1); |
|
395 |
by (rtac sym 1); |
|
396 |
by (stac (hoare_lemma27 RS mp) 1); |
|
397 |
by (atac 1); |
|
398 |
by (rtac conjI 1); |
|
399 |
by (rtac refl 1); |
|
400 |
by (atac 1); |
|
401 |
by (rtac refl 1); |
|
402 |
qed "hoare_lemma29"; |
|
244 | 403 |
|
404 |
(* ------ the main prove q o p = q ------ *) |
|
405 |
||
9265 | 406 |
Goal "q oo p = q"; |
407 |
by (rtac ext_cfun 1); |
|
408 |
by (stac cfcomp2 1); |
|
409 |
by (rtac (hoare_lemma3 RS disjE) 1); |
|
410 |
by (etac hoare_lemma23 1); |
|
411 |
by (etac hoare_lemma29 1); |
|
412 |
qed "hoare_main"; |
|
244 | 413 |
|
414 |